240 Commits

Author	SHA1	Message	Date
Leonardo Alt	8eba66daf9	Extract boost smt and remove unused tests	2020-09-23 17:55:55 +02:00
Đorđe Mijović	858b4507e2	Merge pull request #9854 from ethereum/bitwiseSmt ... [SMTChecker] Support compound shifts and bitwise and, or, and xor	2020-09-23 12:35:48 +02:00
Djordje Mijovic	96bafb9ba3	[SMTChecker] Updating old and adding new tests for compound shift operators.	2020-09-23 11:31:37 +02:00
Djordje Mijovic	0193952106	[SMTChecker] Updating old and adding new tests for compound bitwise xor operator.	2020-09-23 11:31:37 +02:00
Djordje Mijovic	e2e0b33ee7	[SMTChecker] Updating old and adding new tests for compound bitwise or operator.	2020-09-23 11:31:41 +02:00
Djordje Mijovic	69df163dcb	[SMTChecker] Updating old and adding new tests for compound bitwise and operator.	2020-09-23 11:31:37 +02:00
Leonardo Alt	f4ee4cd479	Update tests	2020-09-22 20:51:28 +02:00
Alex Beregszaszi	709d25bd3d	[SMTChecker] Support address type conversion with literals	2020-09-22 18:49:11 +01:00
Alex Beregszaszi	c8c17b693b	[SMTChecker] Support events and low-level logs	2020-09-16 11:50:39 +02:00
Alex Beregszaszi	783d66c1a4	[SMTChecker] Support revert()	2020-09-15 11:46:33 +01:00
Alex Beregszaszi	8f36408ef9	Add test case for revert() in SMTChecker	2020-09-15 11:46:16 +01:00
Daniel Kirchner	e93d74398b	Merge pull request #9807 from ethereum/smt_readd_tests ... Readd SMTChecker tests	2020-09-15 02:57:42 +02:00
Leonardo Alt	28c8e01149	Readd SMTChecker tests	2020-09-14 23:44:13 +02:00
Alex Beregszaszi	83934254ea	[SMTChecker] Support type(I).interfaceId	2020-09-14 20:34:52 +01:00
Leonardo Alt	fd6c665548	Update SMTChecker tests with z3 4.8.9	2020-09-14 19:04:13 +02:00
Leonardo	31b5102aa0	Merge pull request #9731 from ethereum/smt_import ... [SMTChecker] Fix CHC encoding	2020-09-12 00:56:04 +02:00
Alex Beregszaszi	961a199cf5	[SMTChecker] Support type(T).min and type(T).max	2020-09-11 21:37:51 +01:00
Leonardo Alt	3fea11e1a9	Remove problematic test	2020-09-11 22:02:18 +02:00
Leonardo Alt	23ee011c56	[SMTChecker] Fix imports	2020-09-11 13:34:46 +02:00
Leonardo Alt	84c707cd2a	Adjust problematic SMTChecker tests	2020-09-10 19:32:17 +02:00
Leonardo Alt	40197df104	[SMTChecker] Support shifts	2020-09-09 19:47:52 +02:00
Leonardo Alt	00f6b303b1	[SMTChecker] Change warning message	2020-09-09 16:14:21 +02:00
Leonardo Alt	69a7808838	Add new tests	2020-09-03 15:19:33 +02:00
Leonardo Alt	afcd44e77c	Update current tests	2020-09-03 15:19:03 +02:00
Leonardo	0d83977d5a	Merge pull request #9648 from ethereum/smt_refactor_predicates ... [SMTChecker] Refactor CHC predicates	2020-09-01 20:38:47 +02:00
Leonardo Alt	49d3804de4	[SMTChecker] Fix rational number short circuit	2020-09-01 17:21:13 +02:00
Leonardo Alt	e23d96464b	Adjust test	2020-09-01 16:10:12 +02:00
Leonardo Alt	016b9b83a8	Refactor predicates	2020-09-01 16:09:56 +02:00
Leonardo Alt	238b8a929e	[SMTChecker] Fix ICE on tuples of one element that actually have tuple type	2020-09-01 08:31:57 +02:00
Leonardo Alt	5cafbeebec	[SMTChecker] Fix ICE on tuple assignment	2020-09-01 08:29:01 +02:00
Leonardo Alt	50e0ada77d	[SMTChecker] Fix unary operator on lvalue tuple	2020-09-01 08:25:06 +02:00
Leonardo Alt	8c05db88c0	[SMTChecker] Fix soundness of array pop	2020-08-31 12:11:33 +02:00
Djordje Mijovic	11a7763f49	[SMTChecker] Support bitwise or, xor and not.	2020-08-26 11:06:56 +02:00
Djordje Mijovic	00e765f478	Fix tests for conditional operator on latest develop.	2020-08-22 07:52:55 +02:00
Đorđe Mijović	4dd25f7302	Merge pull request #9639 from ethereum/smtConditionalSupport ... [SMTChecker] Supporting conditional operator	2020-08-21 14:25:47 +02:00
Djordje Mijovic	3f97a1012a	[SMTChecker] Supporting conditional operator	2020-08-20 21:39:35 +02:00
Leonardo Alt	5afd1219f5	Add test with unused error id	2020-08-14 12:58:27 +02:00
Leonardo Alt	0a160b1ba0	Update remaining tests	2020-08-14 12:58:27 +02:00
Leonardo Alt	80ab56dbc6	Update overflow tests	2020-08-14 12:58:27 +02:00
Leonardo Alt	8a06041bbe	[SMTChecker] Add underflow/overflow target to CHC	2020-08-14 12:58:27 +02:00
Leonardo Alt	ec31d971e6	[SMTChecker] Fix tuple name for arrays	2020-08-07 12:28:10 +02:00
chriseth	3a409c39e4	Merge pull request #9518 from ethereum/smt_fix_bmc_function_inlining ... [SMTChecker] Fix ICE in BMC function inlining	2020-08-06 00:50:04 +02:00
Leonardo Alt	8df8c6e14f	[SMTChecker] Fix ICE in BMC function inlining	2020-08-05 11:47:25 +02:00
Leonardo Alt	55624d6416	Add test from Aon blog post	2020-08-04 09:31:48 +02:00
Leonardo Alt	ad1798b000	[SMTChecker] Fix ICE on fixed bytes access	2020-07-28 17:59:42 +02:00
Leonardo Alt	a6df232fa3	Fix SMT tests	2020-07-28 11:24:25 +02:00
chriseth	9605b85c21	Merge pull request #9352 from ethereum/smt_cex ... [SMTChecker] CHC counterexamples	2020-07-27 19:21:04 +02:00
Leonardo Alt	b207222af7	Fix extra parens	2020-07-27 17:14:59 +02:00
Leonardo Alt	de4ae301c4	[SMTChecker] Fix ICE when tuples have extra effectless parens	2020-07-27 13:03:27 +02:00
Leonardo Alt	95484d9969	Fix tests after rebase	2020-07-23 18:49:03 +02:00