Commit Graph
20 Commits
Author SHA1 Message Date
Leonardo Alt 88030c6568 [SMTChecker] Refactor verification targets 2020-07-10 10:28:49 +02:00
Leonardo Alt 3c4e286390 [SMTChecker] Replace wrap mod by slack vars 2020-06-12 14:57:21 +02:00
Leonardo Alt 45eba27424 Rename namespace 2020-05-20 12:55:18 +02:00
chriseth 823a119117 Merge pull request #8570 from aarlt/clang-tidy-apply-modernize-use-emplace
clang-tidy: Apply modernize-use-emplace.
2020-04-07 17:28:50 +02:00
Leonardo Alt 05a85461fe Symbolic state 2020-04-06 12:27:53 +02:00
Alexander Arlt 90bb1d8a7c Apply modernize-use-emplace. 2020-04-02 17:35:48 -05:00
Leonardo Alt d2f65ea8b1 [SMTChecker] Add SortProvider 2020-03-26 14:55:54 +01:00
Christian Parpart 6b23412fae C++ namespace cleanup (except tests). 2020-01-07 15:51:50 +01:00
chriseth 04f298fd0e Merge pull request #7132 from ethereum/smt_acc_solver
[SMTChecker] EncodingContext config flag to accumulate assertions
2019-08-01 13:04:37 +02:00
Leonardo Alt 6bcbeb1d23 [SMTChecker] Reset SSA index to 0 instead of increasing in context reset 2019-07-25 14:16:34 +02:00
Leonardo Alt b204f27047 [SMTChecker] EncodingContext config flag to accumulate assertions 2019-07-19 19:31:25 +02:00
Leonardo Alt 01570bbc8c EncodingContext's solver needs to be set dynamically 2019-07-08 14:40:15 +02:00
Leonardo Alt be663680d4 [SMTChecker] Clear encoding context before engine starts 2019-07-08 11:56:04 +02:00
Leonardo Alt 934e00d235 [SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars 2019-07-03 16:05:56 +02:00
Leonardo Alt ed275fd760 [SMTChecker] Collect assertions in EncodingContext 2019-06-24 15:03:00 +02:00
Leonardo Alt 5493a41842 [SMTChecker] Move global variables and functions to encoding context 2019-05-16 18:11:31 +02:00
Leonardo Alt 4e430ba0ae [SMTChecker] Move expression handling to EncodingContext 2019-05-14 15:56:43 +02:00
Leonardo Alt ebbe03cad6 [SMTChecker] Move variable handling to EncodingContext 2019-05-13 16:59:28 +02:00
Leonardo Alt fc482de695 [SMTChecker] Support address members 2019-04-25 16:24:36 +02:00
Leonardo Alt dd1afeba52 [SMTChecker] Support this as address 2019-04-18 17:56:52 +02:00