cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2016-11-17	Fix Makefiles in test	Andres Notzli
	With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that.
2016-11-08	Add a few options to separation logic and sets. Minor changes to separation ↵	ajreynol
	logic, change syntax for empty heap constraint.
2016-11-03	Add priorities to getNextDecision. Properly handle case for finite types + ↵	ajreynol
	unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-11-02	Add missing regression.	ajreynol

2016-11-02	Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵	ajreynol
	Fix a few more memory leaks.
2016-10-21	Move slow regress0 benchmarks to regress1, increment regress1 through regress3.	ajreynol

2016-09-12	Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry ↵	ajreynol
	breaking in theory sep.
2016-09-09	Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.	ajreynol

2016-09-09	Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵	ajreynol
	allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
2016-08-09	Fixes for sep star rewrite.	ajreynol

2016-07-07	Ensure heap disjointness in sep refinements.	ajreynol

2016-07-05	Refactor last call for theories, only create one model when quantifiers are ↵	ajreynol
	enabled. Fix sep.nil preregistration in TheorySep.
2016-06-17	Support for separation logic. Enable cbqi by default for pure BV.	ajreynol