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

Age	Commit message (Collapse)	Author
2017-10-03	Add regression from #50 regarding "as" parsing in smt2 (#1188)	Andrew Reynolds
	* Add regression from pull request #50, which was fixed separately in pull request #1162. * Improve comment in regression
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.
2015-01-14	sygus input language and benchmark	Morgan Deters

2015-01-11	adjusted to both v2.0 and v2.5 string literals	Tianyi Liang

2015-01-09	blocked unprintable characters in string literals;	Tianyi Liang
	disabled string literal test case for smtlib v2.5
2014-10-23	Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.	Morgan Deters
	* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.)
2014-06-08	test for prvs commit (tokenize emptyset)	Kshitij Bansal
	9978c259f30b1f4b2c70c04589a309033a6eb1f6