14 Commits

Author	SHA1	Message	Date
Leonardo Alt	e1c238e25f	[SMTChecker] Add loop support	2019-09-13 12:40:53 +02:00
Daniel Kirchner	6ed219ebe8	Support multiple sources for syntax tests.	2019-08-19 14:45:26 +02:00
Leonardo Alt	6bcbeb1d23	[SMTChecker] Reset SSA index to 0 instead of increasing in context reset	2019-07-25 14:16:34 +02:00
Leonardo Alt	03cc124f32	Add CHC skeleton	2019-07-19 11:52:05 +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	fb3c85633b	Always create symbolic expression	2019-07-01 16:25:33 +02:00
Leonardo Alt	a28b84fdc3	[SMTChecker] Add a more general VerificationTarget	2019-06-27 10:31:50 +02:00
Leonardo Alt	d9ce9cab99	[SMTChecker] Use smtlib's implies instead of \!a or b	2019-06-04 14:23:44 +02:00
Leonardo Alt	5440a53d4d	[SMTChecker] Support tuples as function calls with multiple return values	2019-05-03 06:10:22 +02:00
Leonardo Alt	0cdb9e48b0	Update SMTChecker JSON tests expectation	2019-04-30 11:08:36 +02:00
Leonardo Alt	fc482de695	[SMTChecker] Support address members	2019-04-25 16:24:36 +02:00
Leonardo Alt	08737e43dc	[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions	2018-12-11 11:28:25 +01:00
Leonardo Alt	0ff4cbe51b	Add SMTChecker tests for standard JSON	2018-11-23 10:51:06 +00:00