30 Commits

Author	SHA1	Message	Date
Leonardo Alt	5bb4e73693	Review 1	2020-07-23 18:49:03 +02:00
Leonardo Alt	003c9b9a5b	Update tests	2020-07-23 18:49:03 +02:00
Leonardo Alt	9d2a0947e9	Fix 1-tuple chain	2020-07-23 13:46:41 +02:00
Leonardo Alt	672633af0a	[SMTChecker] Fix ICE on compound assignment to array index	2020-07-16 17:44:10 +02:00
Leonardo Alt	46653b2d43	Fix ICE when bitwise operator on fixed bytes	2020-07-15 19:32:15 +02:00
a3d4	e04cedafc5	Added error codes to SyntaxTest expectations (updated tests)	2020-06-22 16:51:47 +02:00
Leonardo Alt	e5d25692a5	[SMTChecker] Fix BMC targets with FP	2020-05-29 18:13:13 +02:00
Leonardo Alt	13f32268da	[SMTChecker] Add test that shows that deleting arrays takes the index into account	2020-05-28 13:08:16 +02:00
Leonardo Alt	9e9f0c52e1	[SMTChecker] Support to bitwise	2020-05-27 20:59:00 +02:00
Leonardo Alt	07bb1952a7	Test updates	2020-05-14 23:32:30 +02:00
Leonardo Alt	a0c605aa85	[SMTChecker] Support array length	2020-05-14 23:32:29 +02:00
Daniel Kirchner	0303902173	Update smt test expectations.	2020-05-14 14:12:01 +02:00
Leonardo Alt	059d0bdebb	Revert "Use Spacer option to improve performance of constant arrays" ... This reverts commit 92059fa848.	2020-04-24 11:55:58 +02:00
Leonardo Alt	92059fa848	Use Spacer option to improve performance of constant arrays	2020-04-23 10:45:02 +02:00
Leonardo Alt	cfe3686116	Fix internal error when using array slices	2020-04-22 23:20:10 +02: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	beed0f6a27	Set tests that CVC4 can't handle to Z3 only	2019-12-09 15:32:08 +01:00
Leonardo Alt	77b9416d3e	Extract SMTChecker mod test	2019-12-09 15:32:08 +01:00
Leonardo Alt	02343208ad	Extract SMTChecker compound assignment division tests	2019-12-09 15:32:08 +01:00
Leonardo Alt	ae6cdc3442	Extract more SMTChecker division tests	2019-12-09 15:32:08 +01:00
Leonardo Alt	b870e4ea31	Extract SMTChecker division tests	2019-12-09 15:32:08 +01:00
Leonardo Alt	5dacaf57bc	Fix ICE in FixedBytes IndexAccess	2019-11-08 17:29:40 +01:00
Leonardo Alt	a774b2d905	[SMTChecker] Zero-initialize arrays	2019-09-02 22:37:30 +02:00
Leonardo Alt	d5fb8cf58a	[SMTChecker] Fix ICE compound bitwise op inside branch	2019-08-02 20:02:39 +02:00
Leonardo Alt	fb3c85633b	Always create symbolic expression	2019-07-01 16:25:33 +02:00
Leonardo Alt	2139c20776	[SMTChecker] Support delete	2019-05-06 18:32:10 +02:00
Leonardo Alt	af9f16e014	[SMTChecker] Support mod	2019-04-12 12:39:25 +02:00
Leonardo Alt	aa9b9aa87e	[SMTChecker] Support unary inc/dec for array/mapping access	2019-04-02 16:53:19 +02:00
Leonardo Alt	c7e5468505	Arithmetic compound assignment operators tests	2019-03-28 15:27:52 +01:00