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
007d39871b
[SMTChecker] Synthesize untrusted functions called externally
2021-01-15 11:56:26 +01:00
Leonardo Alt
b3c3836388
Output internal calls
2021-01-12 14:57:04 +01:00
Martin Blicha
09de54b5eb
tests
2021-01-11 13:36:03 +01:00