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

Age	Commit message (Collapse)	Author
2021-06-02	Remove redundant logic ALL_SUPPORTED. (#6664)	Aina Niemetz

2020-11-10	Add proper support for the declare-heap command for separation logic (#5405)	Andrew Reynolds
	This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic. This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred. Fixes #5343, fixes #4926. Work towards CVC4/cvc4-wishues#22.
2017-01-04	Marking regression test files as non-executable.	Tim King

2016-10-21	Move slow regress0 benchmarks to regress1, increment regress1 through regress3.	ajreynol