Leonardo Alt
|
08737e43dc
|
[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions
|
2018-12-11 11:28:25 +01:00 |
|
Leonardo Alt
|
ec84a7dc9b
|
[SMTChecker] Refactor setZeroValue and setUnknownValue
|
2018-11-22 16:42:51 +01:00 |
|
Leonardo Alt
|
13a142b039
|
[SMTChecker] Add FunctionSort and refactors the solver interface to create variables
|
2018-11-22 10:04:04 +01: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 |
|
Leonardo Alt
|
d8cbf321da
|
Grouping of symbolic variables in the same file and support to FixedBytes
|
2018-10-25 09:30:48 +02:00 |
|
Leonardo Alt
|
c92d3b537d
|
[SMTChecker] Refactor expressions such that they also use SymbolicVariable
|
2018-10-17 18:36:24 +02:00 |
|
Leonardo Alt
|
afe83cc28b
|
Refactor SymbolicAddressVariable and SymbolicVariable allocation
|
2018-10-17 15:58:13 +02:00 |
|
Leonardo Alt
|
ec39fdcb3c
|
[SMTChecker] Refactoring types
|
2018-10-17 15:58:13 +02:00 |
|