63 Commits

Author	SHA1	Message	Date
Leonardo Alt	08737e43dc	[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions	2018-12-11 11:28:25 +01:00
Kevin Kelley	fb6fd1b3c2	add a 'readable' format for large hex values	2018-12-05 22:15:02 +01:00
Leonardo Alt	8069bb61da	[SMTChecker] Loops are unrolled once	2018-12-04 12:35:19 +01:00
Leonardo Alt	32fe4768a9	Organize smt tests in subdirectories	2018-11-22 13:33:28 +00:00
Leonardo Alt	4a71080ae5	Remove pragma ABIEncoderV2 from smt test	2018-11-22 13:33:28 +00:00
Alex Beregszaszi	109cfcef69	Drop numbering in front of the SMTChecker tests	2018-11-22 13:33:28 +00:00
Alex Beregszaszi	636da48e82	Move most of SMTChecker tests from C++ to isoltest ... But keep divison in C++ because results differ between different solvers	2018-11-22 13:33:24 +00:00
Leonardo Alt	06c3f0953a	[SMTChecker] Support bound function calls	2018-11-19 15:29:00 +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	e2cf5f6ed9	Add gasleft constraint and use full member access name	2018-10-22 18:19:11 +02:00
Leonardo Alt	b46b827c30	[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash	2018-10-19 15:52:16 +02:00
Leonardo Alt	e4851cf59e	[SMTChecker] Inline calls to internal functions	2018-10-15 15:11:21 +02:00