Martin Blicha
Martin Blicha
As discussed at TACAS, it would be great if Theta could support CHC front-end. The language is a simple extension of SMT-LIB, format described [here](https://chc-comp.github.io/format.html). At least transition systems (1...
For [this example](https://gist.github.com/blishko/33f40fe69d4ac3c8b75aac69da9c9960) I am getting an error when running Z3 (both Z3 4.8.9 and current master 620204bbb) with the option `fp.xform.inline_eager=false`. The error reported is `(error "line 289 column...
Previously, creating zero value expression for integer type (`solidity::frontend::IntegerType`) did not respect signedness of the type. This led to an assertion violation in methods creating SMT representation of array expressions,...
This is an initial draft for removing specialized solver interfaces (Z3, CVC4) and use only SMTLIB interface for communicating with all solvers. Things to resolve - [x] Check tests results,...
There are two kinds of array literals in Solidity: string literals (arrays of characters/bytes) and proper array literals (e.g., [1,2,3]). While array literals cannot be directly tested for equality in...
This change is in preparation for upgrading to cvc5. Since archlinux is not running SMT tests anyway, we can drop cvc4 from the build immediately.
Instead of compiling `solc` itself with CVC4 support, it is now enough to have `cvc4` executable on PATH when running the compiler. Instead of using API of CVC4, we write...
There is no need to represent predicates using the symbolic variables. These are not variables that correspond to expression in the code. It is sufficient to store the name of...
Hi @NikolajBjorner , @agurfinkel! In SolCMC, we have observed some regressions on our test suite when attempting to upgrade Z3 from 4.12.1 to 4.13.0. I have prepared a simplified example...
This commit introduces the interface class without actually using it. The actual switch will be done later, after all things are set up. This was separated from #15252.