Jad Hamza

Soundness issue with non-strict positive types and impredicativity of Boolean (or of choose realizability)

9

Stainless is able to derive false in that example adapted from http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/ (original source: Inductively Defined Types (COLOG-88), also discussed in [Coq-Club] Positivity and Elimination Principle: https://sympa.inria.fr/sympa/arc/coq-club/2012-01/msg00087.html) I don't really...

`sbt test` fails with NullPointerException when loading jar

2

Using Java version `openjdk version "1.8.0_242"` on Debian, I get this error: ``` [info] ForComprehension: null java.lang.NullPointerException at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1847) at java.lang.Runtime.loadLibrary0(Runtime.java:871) at java.lang.System.loadLibrary(System.java:1124) at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:110) at z3.Z3Wrapper.(Z3Wrapper.java:49) at z3.scala.Z3Context.(Z3Context.scala:23) at...

Z3 4.8.10

7

I removed `getAbsFunDecl` (and the corresponding test suite) which crashes because the AST kind is `Z3UnknownAST`. Is that ok?

Choose under lamba

13

In this PR https://github.com/epfl-lara/stainless/pull/946, I changed the way VCs are generated in the type-checker, and the following file is now valid: https://github.com/epfl-lara/stainless/blob/965b0ec485e62715003738e73605bd4dbb5da1da/frontends/benchmarks/verification/invalid/Equations1.scala But I was expecting the second equations to...

While copying `ChooseEncoder` to Stainless, I noticed that it doesn't traverse all the trees (for instance bound expressions in lets), so I've added a transformer to make sure that we...

Type error in tip printed from Stainless

2

In a verification condition on the Stainless side, I have a term that contains this: ```scala if (thiss.order.leq(thiss.array((n - 1))._1, elemRef(0)._1)) { Return[(Boolean, SortedArray[K, T], Array[(K, T)]), Unit]((false, thiss, elemRef))...

Using nested recursive calls with Program results in error: Recursive definition is ill-formed

1

#### Description of the problem Hello, I'm having an issue when using `Program` and nested recursive calls. I guess the problem comes from the recursive call to `f` in `f_obligation_2...