19 Commits

Author	SHA1	Message	Date
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	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
Leonardo Alt	e3652627fd	[SMTChecker] Fix ICE in CHC when function used as argument	2019-11-13 15:11:30 +01:00
Leonardo Alt	6b10efff8c	Add CHCSmtLib2Interface	2019-11-07 11:12:11 +01:00
Leonardo Alt	c5e081dc8c	[SMTChecker] Refactor CHC loops and add if blocks	2019-11-05 09:28:59 +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	03cc124f32	Add CHC skeleton	2019-07-19 11:52:05 +02:00