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 |
|