Martin Blicha
cdfc19b503
SMTChecker: Bring back counterexample checks in regression tests
...
Since the default is now to ignore the counterexamples when checking
test output, we bring back counterexample checks in tests where the
counterexample is (mostly) deterministic.
2023-07-25 12:26:21 +02:00
Leo Alt
21c0f78650
Report safe properties in BMC and CHC
2023-03-09 14:59:32 +01:00
Leo Alt
38b0cf7f9c
SMTChecker tests
2021-10-26 11:30:30 +02:00
Leonardo Alt
0a4afa71bd
Update old tests
2021-04-08 21:03:39 +02:00
Leonardo Alt
dbd067d6db
Report out of bounds index access
2021-03-30 10:28:48 +02:00
Leonardo Alt
f1ae24abc7
Remove extra line breaks
2021-01-12 14:00:07 +01:00
Leonardo Alt
b02722ebda
Add contract name to called function in cex
2021-01-04 10:03:16 +01:00
Leonardo Alt
3c142e0e94
Move CHC counterexamples to primary location
2020-12-09 19:55:18 +01:00
Martin Blicha
2ee633f404
[SMTChecker] Added support for public getters through this.
2020-12-02 16:06:48 +01:00