20 Commits

Author	SHA1	Message	Date
Martin Blicha	c1a57ffbfe	[SMTChecker] More precise creation of verification targets.	2020-10-30 19:11:28 +01:00
Leonardo Alt	cf35785328	Add unknown message to all verification targets	2020-10-19 20:54:13 +01:00
Leonardo Alt	54f76e081a	[SMTChecker] Support crypto functions in CHC	2020-10-16 14:57:13 +01:00
Leonardo Alt	3d2e6252f0	Add/update tests	2020-10-12 11:11:52 +01:00
Leonardo Alt	e6bd18525b	[SMTChecker] Add engine prefix to verification target error messages	2020-09-25 19:09:06 +02:00
Leonardo Alt	0223571987	[SMTChecker] Do not report error when rlimit	2020-09-25 18:43:10 +02:00
Leonardo Alt	28c8e01149	Readd SMTChecker tests	2020-09-14 23:44:13 +02:00
Leonardo Alt	00f6b303b1	[SMTChecker] Change warning message	2020-09-09 16:14:21 +02:00
Leonardo Alt	9d2a0947e9	Fix 1-tuple chain	2020-07-23 13:46:41 +02:00
Leonardo Alt	5160f89c1b	[SMTChecker] Support to external calls to unknown code	2020-07-01 18:20:33 +02:00
a3d4	e04cedafc5	Added error codes to SyntaxTest expectations (updated tests)	2020-06-22 16:51:47 +02:00
Leonardo Alt	3c4e286390	[SMTChecker] Replace wrap mod by slack vars	2020-06-12 14:57:21 +02:00
Leonardo Alt	07368c2e1e	Add support to internal function calls	2020-03-11 16:29:07 +01:00
Leonardo Alt	beed0f6a27	Set tests that CVC4 can't handle to Z3 only	2019-12-09 15:32:08 +01:00
Leonardo Alt	e1c238e25f	[SMTChecker] Add loop support	2019-09-13 12:40:53 +02:00
Leonardo Alt	a28b84fdc3	[SMTChecker] Add a more general VerificationTarget	2019-06-27 10:31:50 +02:00
Leonardo Alt	48d6729164	[SMTChecker] Remove overflow check for assignments	2019-06-24 17:58:56 +02:00
Leonardo Alt	34470f3549	[SMTChecker] Only check for overflow/underflow in the end of the function	2019-02-18 23:55:58 +01:00
Kevin Kelley	fb6fd1b3c2	add a 'readable' format for large hex values	2018-12-05 22:15:02 +01:00
Leonardo Alt	8069bb61da	[SMTChecker] Loops are unrolled once	2018-12-04 12:35:19 +01:00