20 Commits

Author	SHA1	Message	Date
Leonardo Alt	3b2851ee41	Integer min and max values placed under SymbolicIntVar instead of SMTChecker	2018-02-28 18:05:20 +01:00
Leonardo Alt	f41591b3dd	[SMTChecker] A little refactoring on SSA vars	2018-02-28 18:05:20 +01:00
Leonardo Alt	d0abc5359b	[SMTChecker] Variables are merged after branches (ite variables)	2018-01-04 18:20:12 +01:00
Leonardo Alt	b588134840	[SMTChecker] Fix typo in the code (satisifable->satisfiable)	2017-12-18 17:31:27 +01:00
Leonardo Alt	a1e296e392	[SMTChecker] Helper functions to add an expression to the solver conjoined with or implied by the current path conditions	2017-12-13 17:59:36 +01:00
Leonardo Alt	2af4d7c7dd	[SMTChecker] Keep track of current path conditions	2017-12-13 17:39:10 +01:00
chriseth	d160ec8595	Fix signed division.	2017-11-30 01:20:21 +01:00
chriseth	19e067465a	Unary operators and division.	2017-11-30 01:20:21 +01:00
chriseth	8538a25f8d	Fix problem with non-value-typed variables.	2017-11-22 02:35:34 +00:00
chriseth	19d5c42429	For loop.	2017-11-22 02:35:34 +00:00
chriseth	22c689d516	Check for conditions being constant.	2017-11-22 02:35:34 +00:00
chriseth	b37377641d	Track usage of variables.	2017-11-22 02:35:34 +00:00
chriseth	f62caf587e	Handle branches.	2017-11-22 02:35:34 +00:00
chriseth	1f97c1ea8f	Rename variables in SMT checker.	2017-10-17 18:29:53 +01:00
chriseth	cf5e1d6120	Review changes.	2017-08-23 17:37:35 +02:00
chriseth	75f09f2a84	Partial support for if statements.	2017-08-23 17:37:35 +02:00
chriseth	9ac2ac14c1	Rename read file callback.	2017-08-23 17:37:35 +02:00
chriseth	4cea3d4aa4	Insert abstraction layer.	2017-08-23 17:37:35 +02:00
chriseth	b3f8ed457a	Cleanup.	2017-08-23 14:24:30 +02:00
chriseth	1ece7bf443	z3 conditions	2017-08-23 14:24:04 +02:00