120 Commits

Author	SHA1	Message	Date
Leonardo Alt	d818746e0c	[SMTChecker] Fix ICE in abi.decode	2019-11-18 13:15:10 +01:00
chriseth	7c258873bd	Add some more abstract keywords in test to make sure the correct property is tested.	2019-11-04 17:26:38 +01:00
Alexander Arlt	cd3ad73b5a	Update tests.	2019-11-01 14:54:47 -05:00
Leonardo Alt	360f868836	[SMTChecker] Fix literal string type mismatch	2019-08-10 21:51:46 +02:00
Leonardo Alt	6606a13ed2	[SMTChecker] Remove unsound assertion (too strong)	2019-07-01 16:16:39 +02:00
Leonardo Alt	a28b84fdc3	[SMTChecker] Add a more general VerificationTarget	2019-06-27 10:31:50 +02:00
Leonardo Alt	60a4f03d3d	[SMTChecker] Fix ice in unsupported functions with multi return values	2019-05-16 18:23:42 +02:00
Leonardo Alt	ef32bf185f	[SMTChecker] Inline external function calls to this.	2019-05-09 16:53:30 +02:00
Leonardo Alt	3d52a6ca68	[SMTChecker] Fix ICE in branch-inline function call-modify local variable	2019-05-09 09:15:11 +02:00
Leonardo Alt	6c7527ac90	[SMTChecker] Support tuple type declaration	2019-05-02 12:05:21 +02:00
Leonardo Alt	a6db37ac9c	[SMTChecker] Fix bad cast in base constructor modifier.	2019-04-30 18:48:13 +02:00
Leonardo Alt	dd1afeba52	[SMTChecker] Support this as address	2019-04-18 17:56:52 +02:00
Leonardo Alt	ecd89393ee	[SMTChecker] Support contract type	2019-04-17 16:30:11 +02:00
Leonardo Alt	79d8a4e13a	[SMTChecker] Refactor VariableUsage	2019-04-05 11:38:37 +02:00
Leonardo Alt	2764d2f525	Tests that used to give false negatives	2019-03-28 14:32:47 +01:00
Leonardo Alt	7f8ceaadab	[SMTChecker] Clear state knowledge after external function calls	2019-01-21 12:58:40 +01:00
Leonardo Alt	08737e43dc	[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions	2018-12-11 11:28:25 +01:00
Leonardo Alt	32fe4768a9	Organize smt tests in subdirectories	2018-11-22 13:33:28 +00:00
Leonardo Alt	06c3f0953a	[SMTChecker] Support bound function calls	2018-11-19 15:29:00 +01:00
Leonardo Alt	e4851cf59e	[SMTChecker] Inline calls to internal functions	2018-10-15 15:11:21 +02:00