Commit Graph
21 Commits
Author SHA1 Message Date
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 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 e46abd0ca1 Update tests due to nondeterminism 2021-07-19 15:20:11 +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
Martin Blicha 432944d0b4 [SMTChecker] Small refactoring of defining SMT expressions for structs/tuples 2021-03-16 15:34:43 +01:00
Leonardo Alt 6fd76e830d Fix CHC cex order 2021-03-11 10:36:40 +01:00
Martin Blicha a49950cdf3 [SMTChecker] Added transaction constraints also for contract deployment 2021-02-01 16:46:34 +01:00
Martin Blicha deb90d84a6 [SMTChecker] added missing type constraints for Address 2021-01-27 20:39:24 +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
Leonardo Alt b02722ebda Add contract name to called function in cex 2021-01-04 10:03:16 +01:00
Leonardo Alt 50be39fc21 Add and update tests 2020-12-17 14:42:49 +01:00
Leonardo Alt 3c142e0e94 Move CHC counterexamples to primary location 2020-12-09 19:55:18 +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