Martin Blicha
Martin Blicha
This is again the problem with BMC not tracking the state of the contract. Since it is doing only a local check, it does not know that the state variable...
This is another false positive due to overapproximations in the encoding. We will investigate if we can make the encoding more precise.
Before we merge this, I wanted to follow up on Rodrigo's suggestion to remove installation of dependencies in `t_archlinux_soltest`, because these are already installed in `b_archlinux`. Except for Z3. That...
> The binary is not completely static. Z3 is actually the one thing we link dynamically and the `z3` package contains that dynamic library. You need it to be installed...
OK, how about we continue with the conversation about Z3 in our CI channel. I think we can merge this PR as is now, no?
I will start investigating on Monday. I remember that some time ago I tried using Z3 4.13 and ran into an issue with SMTChecker tests. It seemed like Z3 ignored...
There are definitely some regressions in our test suite with Z3 4.13.0, so we cannot update right away. I have filed an [issue](https://github.com/Z3Prover/z3/issues/7255) in Z3. Let's see if can get...
Looks like the issue in Z3 is now solved, but we have to wait for the next release.
Z3 has been updated to 4.13.3 (#15558), so I think we can close this issue.
That should not be the case. I will investigate. What exactly have you been trying? What examples?