Leonardo Alt
|
2f6de12e8c
|
[SMTChecker] Make smt::Sort::operator== virtual
|
2018-11-30 10:41:15 +01:00 |
|
chriseth
|
9e9250c961
|
Fix move bug.
|
2018-11-29 15:32:38 +01:00 |
|
chriseth
|
bb10be789c
|
Inject SMTLIB2 queries and responses via standard-json-io.
|
2018-11-23 09:43:49 +01:00 |
|
chriseth
|
d686807153
|
Style
|
2018-11-22 21:13:02 +01:00 |
|
Leonardo Alt
|
20accf1a90
|
[SMTChecker] Add ArraySort and array operations
|
2018-11-22 14:04:20 +01:00 |
|
Leonardo Alt
|
13a142b039
|
[SMTChecker] Add FunctionSort and refactors the solver interface to create variables
|
2018-11-22 10:04:04 +01:00 |
|
Christian Parpart
|
87821c53c3
|
Isolating files shared between Yul- and Solidity language frontend.
|
2018-11-21 18:58:12 +00:00 |
|
Leonardo Alt
|
01ce43e51b
|
[SMTChecker] Refactor smt::Sort and its usage
|
2018-11-21 15:46:47 +01:00 |
|
Leonardo Alt
|
70bb0eaf95
|
[SMTChecker] Implement uninterpreted functions and use it for blockhash()
|
2018-11-15 09:12:42 +01:00 |
|
Bhargava Shastry
|
67fd3ca4a7
|
Retained move/copy semantics; removed const qualifier from Expression's members name (of type std::string) and arguments (of type std::vector<Expression>)
|
2018-10-17 16:46:18 +02:00 |
|
Bhargava Shastry
|
546b08c158
|
Fix compiler warning: clang-8 warns of explicitly-defined op implicitly deleted for Expression object's copy and move constructors
|
2018-10-17 16:42:51 +02:00 |
|
Leonardo Alt
|
55c1fb60b4
|
[SMTChecker] Add CheckResult::CONFLICTING
|
2018-07-27 16:16:26 +01:00 |
|
Leonardo Alt
|
87a38e1abe
|
[SMTChecker] SMTPortfolio: use all SMT solvers available
|
2018-07-27 16:15:34 +01:00 |
|
Leonardo Alt
|
b356f6a7f9
|
Setting timeout to Z3 and CVC4
|
2018-07-27 16:01:48 +02:00 |
|
Alexander Arlt
|
f94b793472
|
Add virtual destructors on base classes.
|
2018-05-02 13:29:16 +02:00 |
|
Leonardo Alt
|
ae3350ae03
|
[SMTChecker] Integration with CVC4
|
2018-04-17 12:26:58 +01:00 |
|
Leonardo Alt
|
c2d26eb6a2
|
[SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.
|
2018-03-12 20:16:47 +01:00 |
|
Leonardo Alt
|
6a940f0a99
|
[SMTChecker] Support to Bool variables
|
2018-03-12 20:16:47 +01:00 |
|
Leonardo Alt
|
2af4d7c7dd
|
[SMTChecker] Keep track of current path conditions
|
2017-12-13 17:39:10 +01:00 |
|
chriseth
|
19e067465a
|
Unary operators and division.
|
2017-11-30 01:20:21 +01:00 |
|
chriseth
|
0e2a9658d2
|
Explain IntIntFun and merge assertion.
|
2017-11-23 19:02:47 +01:00 |
|
chriseth
|
762d591a47
|
Introduce sorts for smt expressions.
|
2017-11-22 15:20:26 +01:00 |
|
chriseth
|
22c689d516
|
Check for conditions being constant.
|
2017-11-22 02:35:34 +00:00 |
|
chriseth
|
9e63710b8e
|
Remove parameter names for defaulted functions.
|
2017-08-31 12:16:41 +02:00 |
|
chriseth
|
cf5e1d6120
|
Review changes.
|
2017-08-23 17:37:35 +02:00 |
|
chriseth
|
75f09f2a84
|
Partial support for if statements.
|
2017-08-23 17:37:35 +02:00 |
|
chriseth
|
1e05ebe50e
|
Refactor Z3 read callback.
|
2017-08-23 17:37:35 +02:00 |
|
chriseth
|
4cea3d4aa4
|
Insert abstraction layer.
|
2017-08-23 17:37:35 +02:00 |
|