inox issues

Inox does not compile on Scala 3.3.1 +

5

Inox is currently on Scala 3.3.0, and fails to compile on 3.3.1 or higher. I noticed this while updated my build to update dependencies generally. The following error is raised:...

sankalpgambhir

Bump to 3.3.3 (does not compile)

2

This PR is to discuss about the bump to Scala 3.3.3. Bumping to this version makes the solver hierarchy for `NativeZ3Opt` not valid anymore, with this error message: ``` [error]...

samuelchassot

CVC4/5 unsupported feature shows an error even though another solver is verifying the VC

2

When using this feature unavailable of CVC4/5, an error message is displayed even though the VC is verified by another available solver. This could be a message displayed only in...

samuelchassot

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...

jad-hamza

bug

soundness

Adding a case for type instantiation

4

Concerns the case `ADTType -> RefinementType`. However, we drop the `prop` part, so maybe this is incorrect?

mario-bucev

Add a minimizing solver for smaller counter-examples

1

This is part of the Formal Verification course project from @mbovel and me, the idea is to add a "minimizing" solver that makes "smaller" counter-examples, such as ints/BVs closer to...

SolalPirelli

Add debug option to dump blocker graph

Adds a debug section `blocker-graph` that dumps the (non-strict) implication graph among all blocking literals. The current graph is dumped at the end of `checkAssumptions` and saved in `blocker-graphs/*file*-*n*.dot`. Nodes...

gsps

Fix RecursiveEvaluator not erasing types (Stainless #1135)

3

Fixes Inox-side issue of Stainless issue 1135 (https://github.com/epfl-lara/stainless/issues/1135). While issues on the Inox side weren't directly observed, we should really be operating on fully-erased values, so that expressions such as...

gsps