16 Commits

Author	SHA1	Message	Date
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