Samuel Chassot

I think it would be better to have a separate timeout option for the measure inferences. It is indeed quite impractical in some cases: for example, when running on battery,...

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

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

Includes a renaming of the packages in the mutableMaps project.

Revisiting "unfold" and renaming it to unfolding

7

Solves #1550

`unfolding` should return the return value of the function so that it is a hint for verification, and has the behaviour of the unfolded function at runtime

4

And maybe can be `inline def`