Jad Hamza

I tried on Windows on PowerShell and got an error as well. I had other issues like colors not being displayed correctly (known issue for PowerShell). For this issue, it...

I tried in VSCode and emacs to enter a tab (of length 8), and the column numbers in the bottom of the screen are shown as 9 (VSCode) and 8...

Thanks for the report! That's right, Stainless uses the file timestamp to decide if it has to rerun: https://github.com/epfl-lara/stainless/blob/5b7b3a0c01c23486fea44abb2255f0963a242708/core/src/main/scala/stainless/utils/FileWatcher.scala We could use the file content instead, what do other people...

Such conversions are not supported because it's not clear how to translate them for verification in the underlying solvers. If you don't want verification for function involving those conversions, you...

When this is fixed, we should unignore these benchmarks: https://github.com/epfl-lara/stainless/blob/729aa8b1666f101f82d918f6caeccd18115ec7f8/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala#L96 https://github.com/epfl-lara/stainless/blob/729aa8b1666f101f82d918f6caeccd18115ec7f8/frontends/scalac/src/it/scala/stainless/verification/VerificationSuite.scala#L121

It's with `--feeling-lucky` (I don't really know how this works, but the description is: "Use evaluator to find counter-examples early"), so maybe it's even before that. (Also there shouldn't be...

Opened an issue here: https://github.com/Z3Prover/z3/issues/5103

Hmm, the Z3 issue was closed because it's not a bug. On our end we can simplify the `FunctionClosure` transformation (but I'm not sure that'll scale for large examples). We...

@samarion I'm trying out the `Option` encoding here: https://github.com/epfl-lara/stainless/compare/master...jad-hamza:cvc4-arrays?expand=1#diff-833e151d83b173d8c6f1ca01ad436463073344e02d8ea181f475f887775b9ca3 (I had to change `OptionSort` to be able to use it for target Inox trees). The encoding error is still there:...

We also want to force the models to use `Some` and not `None`. For instance, `a1 == a2` should be valid for two arrays `Array[Unit]` of length 1.