18 Commits

Author	SHA1	Message	Date
Leonardo Alt	88030c6568	[SMTChecker] Refactor verification targets	2020-07-10 10:28:49 +02:00
Leonardo Alt	3c4e286390	[SMTChecker] Replace wrap mod by slack vars	2020-06-12 14:57:21 +02:00
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	05a85461fe	Symbolic state	2020-04-06 12:27:53 +02:00
Leonardo Alt	3bee348525	Change CHC encoding to functions forest instead of explicit CFG	2020-03-03 12:12:26 +01: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
Leonardo Alt	b204f27047	[SMTChecker] EncodingContext config flag to accumulate assertions	2019-07-19 19:31:25 +02:00
Leonardo Alt	01570bbc8c	EncodingContext's solver needs to be set dynamically	2019-07-08 14:40:15 +02:00
Leonardo Alt	be663680d4	[SMTChecker] Clear encoding context before engine starts	2019-07-08 11:56:04 +02:00
Leonardo Alt	934e00d235	[SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars	2019-07-03 16:05:56 +02:00
Leonardo Alt	ed275fd760	[SMTChecker] Collect assertions in EncodingContext	2019-06-24 15:03:00 +02:00
Leonardo Alt	5493a41842	[SMTChecker] Move global variables and functions to encoding context	2019-05-16 18:11:31 +02:00
Leonardo Alt	4e430ba0ae	[SMTChecker] Move expression handling to EncodingContext	2019-05-14 15:56:43 +02:00
Leonardo Alt	ebbe03cad6	[SMTChecker] Move variable handling to EncodingContext	2019-05-13 16:59:28 +02:00
Leonardo Alt	fc482de695	[SMTChecker] Support address members	2019-04-25 16:24:36 +02:00
Leonardo Alt	dd1afeba52	[SMTChecker] Support this as address	2019-04-18 17:56:52 +02:00