Leo Alt
|
cba3d18f66
|
adjust for osx nondeterminism
|
2022-05-04 19:04:54 +02: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 |
|
Leo Alt
|
4c2b661eaa
|
[SMTChecker] Report values for block, msg and tx variables in counterexamples
|
2021-10-05 15:19:10 +02:00 |
|
Leo Alt
|
85378b1770
|
Update existing tests
|
2021-08-25 21:10:08 +02:00 |
|
Leo Alt
|
9ea4576664
|
Update tests
|
2021-08-19 16:34:01 +02:00 |
|
Leo Alt
|
20e23171da
|
Update tests to z3 4.8.12
|
2021-07-16 14:43:52 +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 |
|
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
|
dbd067d6db
|
Report out of bounds index access
|
2021-03-30 10:28:48 +02:00 |
|
Martin Blicha
|
852e877ae7
|
[SMTChecker] Handle InaccessibleDynamicType
|
2021-03-24 11:53:06 +01:00 |
|
Leonardo Alt
|
6fd76e830d
|
Fix CHC cex order
|
2021-03-11 10:36:40 +01:00 |
|
Martin Blicha
|
385a664f3c
|
[SMTChecker] Fix public getter for array of structs.
|
2021-03-08 17:34:20 +01:00 |
|
Martin Blicha
|
a49950cdf3
|
[SMTChecker] Added transaction constraints also for contract deployment
|
2021-02-01 16:46:34 +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
|
41d31fe4d4
|
updates to the tests
|
2020-12-28 20:05:52 +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 |
|
Alex Beregszaszi
|
edbdff8619
|
Update tests
|
2020-12-14 19:32:31 +00:00 |
|
Leonardo Alt
|
3c142e0e94
|
Move CHC counterexamples to primary location
|
2020-12-09 19:55:18 +01:00 |
|
Leonardo Alt
|
7490ffbe13
|
Use nonlinear clauses instead of inlining for base constructors
|
2020-12-04 13:25:56 +01:00 |
|
Martin Blicha
|
2ee633f404
|
[SMTChecker] Added support for public getters through this.
|
2020-12-02 16:06:48 +01:00 |
|