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
678461e828
Fix encoding of side-effects inside if and conditional statements in the BMC engine
2023-05-11 16:44:09 +02:00
Leo Alt
21c0f78650
Report safe properties in BMC and CHC
2023-03-09 14:59:32 +01:00
Leo Alt
d660f0cab0
adjust nondeterministic tests
2022-11-24 13:08:06 +01:00
Leo Alt
504b70b6af
update smt 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
9f171c0f06
update smtchecker tests for new z3
2022-01-12 15:13:34 +01:00
Leo Alt
fb8c138b8b
Do not analyze unecessary contracts
2021-12-24 19:36:32 +01:00
Leo Alt
a2588533e5
macos nondeterminism
2021-11-24 20:41:22 +01:00
Leo Alt
ff5c842d67
update smtchecker tests
2021-11-24 20:41:22 +01:00
Leo Alt
38b0cf7f9c
SMTChecker tests
2021-10-26 11:30:30 +02:00
Alex Beregszaszi
1be07c2b36
Trivial isoltest updates: missing // ---- at the end
2021-04-20 17:38:29 +02:00
Alex Beregszaszi
84c05d35f3
Trivial isoltest updates: normalized whitespace
2021-04-20 17:38:29 +02:00
Alex Beregszaszi
45c6bbe02b
Trivial isoltest updates: directives sorted alphabetically
2021-04-20 17:21:56 +02: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
25b31111df
Merge pull request #11040 from ethereum/smt_fix_virtual_one_more_time
...
[SMTChecker] Fix bug in virtual functions called by constructor
2021-03-17 16:54:36 +01:00
Martin Blicha
2f52affcc2
[SMTChecker] Correctly resolve current scope contract in VariableUsage.
2021-03-15 13:55:14 +01: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
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
Leonardo Alt
f1ae24abc7
Remove extra line breaks
2021-01-12 14:00:07 +01:00
Martin Blicha
09de54b5eb
tests
2021-01-11 13:36:03 +01:00
Leonardo Alt
b02722ebda
Add contract name to called function in cex
2021-01-04 10:03:16 +01:00
Martin Blicha
be0a0f4d90
[SMTChecker] Added constraints for block properties
2020-12-29 22:17:44 +01:00
Martin Blicha
d90b9da4f0
[SMTChecker] Refactoring
2020-12-22 13:10:48 +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
Leonardo Alt
b7ac207391
[SMTChecker] Support return in CHC
2020-12-07 18:17:33 +01:00
Leonardo Alt
1dbd8f8d67
Fix CHC false positives when using branches inside modifiers
2020-11-04 21:47:07 +00:00
Leonardo Alt
daf859c15b
[SMTChecker] report SMTEncoder warnings also via CHC
2020-11-03 16:06:17 +00:00
Mathias Baumann
32b4f18023
Print warning for unnamed return parameters and no return statement
2020-10-13 13:11:29 +02:00
Leonardo Alt
e6bd18525b
[SMTChecker] Add engine prefix to verification target error messages
2020-09-25 19:09:06 +02:00
Leonardo Alt
f4ee4cd479
Update tests
2020-09-22 20:51:28 +02:00
Alex Beregszaszi
783d66c1a4
[SMTChecker] Support revert()
2020-09-15 11:46:33 +01:00
Alex Beregszaszi
8f36408ef9
Add test case for revert() in SMTChecker
2020-09-15 11:46:16 +01:00
Leonardo Alt
00f6b303b1
[SMTChecker] Change warning message
2020-09-09 16:14:21 +02:00
Leonardo Alt
0a160b1ba0
Update remaining tests
2020-08-14 12:58:27 +02:00
Leonardo Alt
003c9b9a5b
Update tests
2020-07-23 18:49:03 +02:00
a3d4
e04cedafc5
Added error codes to SyntaxTest expectations (updated tests)
2020-06-22 16:51:47 +02:00
Leonardo Alt
10162016ae
[SMTChecker] Fix internal error on try/catch
2020-06-02 16:51:53 +02:00
Leonardo Alt
07368c2e1e
Add support to internal function calls
2020-03-11 16:29:07 +01:00
Leonardo Alt
3d52a6ca68
[SMTChecker] Fix ICE in branch-inline function call-modify local variable
2019-05-09 09:15:11 +02:00
Leonardo Alt
80712f44cb
Fix short circuit with assignments
2019-05-06 11:04:43 +02:00
Leonardo Alt
dadafed022
Short circuit tests
2019-03-28 16:08:30 +01:00
Leonardo Alt
a7e826a224
[SMTChecker] Implement short circuit
2019-03-28 16:08:30 +01:00
Leonardo Alt
2ae778bf0a
[SMTChecker] Add buggy short circuit test
2019-03-21 18:47:14 +01:00
Leonardo Alt
32fe4768a9
Organize smt tests in subdirectories
2018-11-22 13:33:28 +00:00