Commit Graph

14 Commits

Author SHA1 Message Date
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
Leonardo Alt
0a4afa71bd Update old tests 2021-04-08 21:03:39 +02:00
Leonardo Alt
ba97d6ac4e Add local vars to cex 2021-03-30 17:55:21 +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
78d55e6b4a [SMTChecker] Support check/unchecked 2020-12-30 12:14:30 +01:00
Leonardo Alt
3c142e0e94 Move CHC counterexamples to primary location 2020-12-09 19:55:18 +01:00
Djordje Mijovic
9cc37c3fa4 [SMTChecker] Fix ICE when using >>> 2020-10-28 09:25:14 +01:00
Leonardo Alt
e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00
Djordje Mijovic
96bafb9ba3 [SMTChecker] Updating old and adding new tests for compound shift operators. 2020-09-23 11:31:37 +02:00
Leonardo Alt
28c8e01149 Readd SMTChecker tests 2020-09-14 23:44:13 +02:00
Leonardo Alt
3fea11e1a9 Remove problematic test 2020-09-11 22:02:18 +02:00
Leonardo Alt
40197df104 [SMTChecker] Support shifts 2020-09-09 19:47:52 +02:00