Leonardo Alt
|
b46b827c30
|
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
|
2018-10-19 15:52:16 +02:00 |
|
Leonardo Alt
|
afe83cc28b
|
Refactor SymbolicAddressVariable and SymbolicVariable allocation
|
2018-10-17 15:58:13 +02:00 |
|
Leonardo Alt
|
aa23326e06
|
Consistent renaming of 'counters' and 'sequence' to 'index'
|
2018-10-17 15:58:13 +02:00 |
|
Leonardo Alt
|
ec39fdcb3c
|
[SMTChecker] Refactoring types
|
2018-10-17 15:58:13 +02:00 |
|
Leonardo Alt
|
4a4620ac95
|
Refactor SSAVariable such that it only uses Type and not Declaration
|
2018-10-15 14:20:54 +02:00 |
|
Daniel Kirchner
|
87804b6419
|
Split IntegerType into IntegerType and AddressType.
|
2018-09-05 12:19:14 +02:00 |
|
Leonardo Alt
|
8d087d1889
|
[SMTChecker] Removing usage of UFs to access SSA indices
|
2018-04-05 12:48:58 +02: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
|
cff0836c03
|
Fix PR comments
|
2018-02-28 18:05:20 +01:00 |
|
Leonardo Alt
|
3b2851ee41
|
Integer min and max values placed under SymbolicIntVar instead of SMTChecker
|
2018-02-28 18:05:20 +01:00 |
|
Leonardo Alt
|
f41591b3dd
|
[SMTChecker] A little refactoring on SSA vars
|
2018-02-28 18:05:20 +01:00 |
|