87 Commits

Author	SHA1	Message	Date
Leonardo Alt	ba3d16fc58	[SMTChecker] Remove 'information is erase' message for if-else	2018-04-19 09:28:44 +02:00
Leonardo Alt	78ba34608f	[SMTChecker] Using solUnimplementedAssert instead of solAssert when applicable	2018-04-18 13:17:59 +02:00
Leonardo Alt	ae3350ae03	[SMTChecker] Integration with CVC4	2018-04-17 12:26:58 +01:00
Leonardo Alt	8d087d1889	[SMTChecker] Removing usage of UFs to access SSA indices	2018-04-05 12:48:58 +02:00
Leonardo Alt	9b64dc501d	[SMTChecker_Bool] Fix PR review comments: method renaming and solAssert	2018-03-12 20:16:47 +01:00
Leonardo Alt	c2d26eb6a2	[SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.	2018-03-12 20:16:47 +01:00
Leonardo Alt	6a940f0a99	[SMTChecker] Support to Bool variables	2018-03-12 20:16:47 +01:00
Leonardo Alt	5d74b862a3	This z3 option is necessary for good solving performance	2018-03-04 14:42:36 +01:00
Leonardo Alt	8b1b4b78c0	Fix PR comments	2018-02-28 18:31:11 +01:00
Leonardo Alt	cff0836c03	Fix PR comments	2018-02-28 18:05:20 +01:00
Leonardo Alt	21c6b80fc9	Supported types listed in SSAVariable	2018-02-28 18:05:20 +01:00
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	a256983320	Fix expression creation problems.	2017-11-30 01:20:21 +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	0e2a9658d2	Explain IntIntFun and merge assertion.	2017-11-23 19:02:47 +01:00
chriseth	762d591a47	Introduce sorts for smt expressions.	2017-11-22 15:20:26 +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	95a65dc04c	Fix boolean constants.	2017-11-22 02:35:34 +00:00
chriseth	22c689d516	Check for conditions being constant.	2017-11-22 02:35:34 +00:00
chriseth	e5de4a66ed	Tests.	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	7d0e46bf59	Merge pull request #3030 from ethereum/smt-variable-types ... SMT enforce variable types	2017-10-20 16:55:09 +02:00
Alex Beregszaszi	7a4c165518	Remove unused variable in Z3	2017-10-18 23:18:11 +01:00
chriseth	153ae98878	Catch exception in Z3. ... Note: This exception might not be the result of resource limitation, it might also hint towards usage error.	2017-10-17 18:30:10 +01:00
Alex Beregszaszi	a71c6faf0f	Remove duplicate >= in Z3	2017-10-17 18:30:07 +01:00
chriseth	1f97c1ea8f	Rename variables in SMT checker.	2017-10-17 18:29:53 +01:00
Alex Beregszaszi	18ae0c3d78	SMT enforce variable types	2017-10-05 12:29:20 +01:00
Alex Beregszaszi	10529e994f	SMT should not crash on typecast/structs	2017-10-05 11:41:11 +01:00
Alex Beregszaszi	66b188cce9	Merge pull request #3022 from ethereum/assert ... Use solAssert and not assert	2017-10-04 14:11:43 +01:00
Alex Beregszaszi	a9847c9551	Use solAssert and not assert	2017-10-04 13:05:55 +01:00
chriseth	5ee3ceaef7	Remove leftover couts.	2017-09-29 12:44:39 +02:00
Alex Beregszaszi	1c0c5d923a	Mark constructors explicit	2017-09-20 01:23:21 +01:00
chriseth	9e63710b8e	Remove parameter names for defaulted functions.	2017-08-31 12:16:41 +02:00
chriseth	cf5e1d6120	Review changes.	2017-08-23 17:37:35 +02:00
chriseth	c93f0434cd	Use experimental feature pragma for SMT checker.	2017-08-23 17:37:35 +02:00
chriseth	75f09f2a84	Partial support for if statements.	2017-08-23 17:37:35 +02:00
chriseth	5bfd5d98c1	Format numbers more nicely.	2017-08-23 17:37:35 +02:00
chriseth	1e05ebe50e	Refactor Z3 read callback.	2017-08-23 17:37:35 +02:00
chriseth	9ac2ac14c1	Rename read file callback.	2017-08-23 17:37:35 +02:00
chriseth	ab5e3a8f6d	Introduce native Z3 support.	2017-08-23 17:37:35 +02:00
chriseth	4cea3d4aa4	Insert abstraction layer.	2017-08-23 17:37:35 +02:00
chriseth	c9cf24458b	Prepare build system for Z3.	2017-08-23 17:37:35 +02:00