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

Age	Commit message (Collapse)	Author
2020-11-12	Models standard (#5415)	yoni206
	This PR relates to #4987 . Our plan is to: delete the model keyword avoid printing extra declarations by default wrap UF values with as expressions. This PR does step 1, and fixes regressions accordingly.
2020-04-08	Fix dump models and dump proofs (#4230)	Andrew Reynolds
	A recent commit (45e489e) made it so that dump-models did not automatically enable produce-models in the global options object, but instead the SmtEngine enabled produce-models internally. The code for dump-models and dump-proofs was (perhaps out of paranoia) checking produce-models and produce-proofs. This removes this check, which is the correct thing to do since SmtEngine internally ensures produce-models is set.