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

Age	Commit message (Collapse)	Author
2020-03-31	Rename checkValid/query to checkEntailed. (#4191)	Aina Niemetz
	This renames api::Solver::checkValidAssuming to checkEntailed and removes api::Solver::checkValid. Internally, SmtEngine::query is renamed to SmtEngine::checkEntailed, and these changes are further propagated to the Result class.
2013-11-11	Change exit status to be more consistent with other command-line tools: 0 ↵	Morgan Deters
	success, nonzero error
2011-03-05	adding three features to CVC parser that drastically improve its support for ↵	Morgan Deters
	the language: LET now supported (but not "type-lets" yet), OPTION now supported, and ^ operator (exponentiation) supported for nonnegative integer exponents. The latter simply expands to MULT, and of course fails assertions in arithmetic if a variable is raised to n >= 2. Also other CVC parser clean-up.