Pawel Gebal
6574c10f25
SMTChecker: Visit the condition in for and while loops after loop is unrolled
2023-08-03 13:36:41 +02:00
Pawel Gebal
db5baebff8
SMTChecker fix: Do not unroll loop after it completes
2023-07-26 16:31:03 +02:00
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
Pawel Gebal
f15b826431
Add optional bounds to unroll loops in BMC model checker
2023-06-02 18:32:38 +02:00
Leo Alt
21c0f78650
Report safe properties in BMC and CHC
2023-03-09 14:59:32 +01:00
feba4de509
Add paris constraints to SMTChecker
...
Co-authored-by: Daniel <daniel@ekpyron.org >
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it >
Co-authored-by: Leo <leo@ethereum.org >
2023-01-31 11:03:04 +01:00
Leo Alt
d660f0cab0
adjust nondeterministic tests
2022-11-24 13:08:06 +01:00
Leo Alt
4fd7de36f1
update smt tests z3 4.8.16
2022-05-03 14:23:27 +02:00
Leo Alt
a9af63187e
Adjust tests for nondeterminism
2021-08-25 21:10:43 +02:00
Leo Alt
85378b1770
Update existing tests
2021-08-25 21:10:08 +02:00
Leo Alt
3c1f555f71
Tests
2021-08-04 13:54:50 +02:00
Leo Alt
20e23171da
Update tests to z3 4.8.12
2021-07-16 14:43:52 +02:00
Leo Alt
d828aeee23
Update test nondet
2021-05-26 22:12:49 +02:00
Alex Beregszaszi
1be07c2b36
Trivial isoltest updates: missing // ---- at the end
2021-04-20 17:38:29 +02:00
Leonardo Alt
0a4afa71bd
Update old tests
2021-04-08 21:03:39 +02:00
Martin Blicha
330fb8f4d0
[SMTChecker] Assignment refactoring
2021-03-31 13:36:50 +02:00
Leonardo Alt
ba97d6ac4e
Add local vars to cex
2021-03-30 17:55:21 +02:00
Leonardo Alt
dbd067d6db
Report out of bounds index access
2021-03-30 10:28:48 +02:00
Leonardo Alt
998346e599
Fix bug in virtual functions called by constructor.
2021-03-12 16:42:28 +01:00
Leonardo Alt
6fd76e830d
Fix CHC cex order
2021-03-11 10:36:40 +01:00
Martin Blicha
deb90d84a6
[SMTChecker] added missing type constraints for Address
2021-01-27 20:39:24 +01:00
Leonardo Alt
a612daa783
Add msgvalue to cex
2021-01-21 19:05:44 +01: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
Martin Blicha
be0a0f4d90
[SMTChecker] Added constraints for block properties
2020-12-29 22:17:44 +01:00
Martin Blicha
41d31fe4d4
updates to the tests
2020-12-28 20:05:52 +01:00
Martin Blicha
77dff222e9
disabling some tests because of nondeterminism in Spacer
2020-12-28 16:24:44 +01:00
Martin Blicha
745466b71f
updates to the tests
2020-12-28 14:32:53 +01:00
Leonardo Alt
50be39fc21
Add and update tests
2020-12-17 14:42:49 +01:00
Martin Blicha
8927015e5a
[SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine
2020-12-11 17:41:50 +01:00
Leonardo Alt
3c142e0e94
Move CHC counterexamples to primary location
2020-12-09 19:55:18 +01:00
Martin Blicha
c1a57ffbfe
[SMTChecker] More precise creation of verification targets.
2020-10-30 19:11:28 +01:00
Leonardo Alt
cf35785328
Add unknown message to all verification targets
2020-10-19 20:54:13 +01:00
Leonardo Alt
54f76e081a
[SMTChecker] Support crypto functions in CHC
2020-10-16 14:57:13 +01:00
Leonardo Alt
88f783bb1e
Remove more tests because current Spacer crashes
2020-10-13 19:27:49 +01:00
Leonardo Alt
3d2e6252f0
Add/update tests
2020-10-12 11:11:52 +01:00
Leonardo Alt
fa7c9a0dc6
Simplify internal function calls
2020-09-28 15:31:15 +02:00
Leonardo Alt
e6bd18525b
[SMTChecker] Add engine prefix to verification target error messages
2020-09-25 19:09:06 +02:00
Leonardo Alt
0223571987
[SMTChecker] Do not report error when rlimit
2020-09-25 18:43:10 +02:00
Leonardo Alt
ebb6f61506
[SMTChecker] Decrease rlimit
2020-09-23 19:28:47 +02:00
Leonardo Alt
28c8e01149
Readd SMTChecker tests
2020-09-14 23:44:13 +02:00
Leonardo Alt
fd6c665548
Update SMTChecker tests with z3 4.8.9
2020-09-14 19:04:13 +02:00
Leonardo Alt
00f6b303b1
[SMTChecker] Change warning message
2020-09-09 16:14:21 +02:00
Leonardo Alt
afcd44e77c
Update current tests
2020-09-03 15:19:03 +02:00
Leonardo Alt
0a160b1ba0
Update remaining tests
2020-08-14 12:58:27 +02:00
Leonardo Alt
ec31d971e6
[SMTChecker] Fix tuple name for arrays
2020-08-07 12:28:10 +02:00
Leonardo Alt
003c9b9a5b
Update tests
2020-07-23 18:49:03 +02:00
Leonardo Alt
9d2a0947e9
Fix 1-tuple chain
2020-07-23 13:46:41 +02:00
Leonardo Alt
5160f89c1b
[SMTChecker] Support to external calls to unknown code
2020-07-01 18:20:33 +02:00
Pawel Gebal
Martin Blicha
Leo Alt
Alex Beregszaszi
Martin Blicha
Martin Blicha