38 Commits

Author	SHA1	Message	Date
Leonardo Alt	45eba27424	Rename namespace	2020-05-20 12:55:18 +02:00
Leonardo Alt	087605ea02	Create libsmtutil	2020-05-20 12:55:18 +02:00
Leonardo Alt	2435ab938c	Add verification target for empty pop	2020-05-18 16:35:56 +02:00
a3d4	8f68c04358	Add unique IDs to error reporting calls	2020-05-06 13:53:46 +02:00
chriseth	41ef13129b	Merge pull request #8678 from ethereum/smt_remove_redundant_constraints ... [SMTChecker] Remove redundant CHC constraints	2020-04-20 15:44:59 +02:00
Leonardo Alt	45f22e3ff4	Add functional map and fold generic functions	2020-04-16 19:21:36 +02:00
Leonardo Alt	bca43586c6	[SMTChecker] Remove redundant CHC constraints	2020-04-15 18:11:39 +02:00
Leonardo Alt	e3ec22124e	[SMTChecker] Fix ICE in CHC internal calls	2020-04-07 01:09:03 +02:00
Leonardo Alt	d2f65ea8b1	[SMTChecker] Add SortProvider	2020-03-26 14:55:54 +01:00
Leonardo Alt	07368c2e1e	Add support to internal function calls	2020-03-11 16:29:07 +01:00
Leonardo Alt	3bee348525	Change CHC encoding to functions forest instead of explicit CFG	2020-03-03 12:12:26 +01:00
Leonardo Alt	d31a2a8d21	CHC clears indices so that initial is 0 and current is 1	2020-02-12 11:47:58 -03:00
Christian Parpart	6b23412fae	C++ namespace cleanup (except tests).	2020-01-07 15:51:50 +01:00
Leonardo Alt	f4f83690f3	Replace some shared_ptr by unique_ptr or raw pointers	2020-01-06 14:16:49 +01:00
chriseth	f6916a637e	Merge remote-tracking branch 'origin/develop' into develop_060	2019-12-09 17:16:58 +01:00
Leonardo Alt	225041738e	Add SMTCheckerTest for isoltest	2019-12-09 15:32:08 +01:00
chriseth	e061f1e743	Merge remote-tracking branch 'origin/develop' into HEAD	2019-12-05 16:44:26 +01:00
Leonardo Alt	48c3a5c225	[SMTChecker] Create options to choose SMT solver in runtime	2019-12-04 17:31:44 +01:00
chriseth	96d777d7f1	Merge commit 'a7d481fb9' into develop_060	2019-12-03 20:47:30 +01:00
Leonardo Alt	c09da092d2	[SMTChecker] Fix constructors with local vars	2019-11-29 16:59:15 +01:00
Leonardo Alt	a352abe00d	[SMTChecker] Add support to constructors	2019-11-28 14:43:23 +01:00
Leonardo Alt	ddc478e3e4	Add CallbackKind and use it for the SMT solver	2019-11-21 22:10:21 +00:00
chriseth	216e1749f4	Merge remote-tracking branch 'origin/develop' into develop_060	2019-11-14 13:42:46 +01:00
Leonardo Alt	e3652627fd	[SMTChecker] Fix ICE in CHC when function used as argument	2019-11-13 15:11:30 +01:00
chriseth	2e5a42836c	Merge pull request #7681 from ethereum/develop ... Merge develop into develop_060	2019-11-11 16:42:03 +01:00
Leonardo Alt	6b10efff8c	Add CHCSmtLib2Interface	2019-11-07 11:12:11 +01:00
chriseth	21e65076b3	Merge pull request #7650 from ethereum/develop ... Merge develop into develop_060	2019-11-06 21:56:55 +01:00
Leonardo Alt	10e70b8603	[SMTChecker] Support inheritance and resolve overrides	2019-11-06 11:00:06 +01:00
chriseth	4d99bf68f4	Merge pull request #7638 from ethereum/develop ... Merge develop into develop_060	2019-11-05 17:33:54 +01:00
Leonardo Alt	c5e081dc8c	[SMTChecker] Refactor CHC loops and add if blocks	2019-11-05 09:28:59 +01:00
Daniel Kirchner	3321fc56ea	Split fallback function and introduce "fallback()" and "receive()" syntax.	2019-11-04 17:17:58 +01:00
Leonardo Alt	e1c238e25f	[SMTChecker] Add loop support	2019-09-13 12:40:53 +02:00
Leonardo Alt	1a70a46f9b	[CHC] Add function blocks and check asserts	2019-08-15 12:25:15 +02:00
Leonardo Alt	bef6228810	[SMTChecker] Create CHC constructor/interface/error blocks	2019-08-12 12:34:57 +02:00
Leonardo Alt	4214cd1354	[SMTChecker] Fix ICE when reporting cex concerning state vars from different source files	2019-08-10 20:56:52 +02:00
Leonardo Alt	369f8cd97f	[SMTChecker] CHC create function return variables	2019-08-05 12:36:51 +02:00
Leonardo Alt	b204f27047	[SMTChecker] EncodingContext config flag to accumulate assertions	2019-07-19 19:31:25 +02:00
Leonardo Alt	03cc124f32	Add CHC skeleton	2019-07-19 11:52:05 +02:00