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

Age	Commit message (Collapse)	Author
2012-07-31	fix some file documentation	Morgan Deters

2012-07-16	Support for having two SmtEngines with the same ExprManager.	Morgan Deters
	Basically, this involves creating a separate StatisticsRegistry for the ExprManager and for the SmtEngine. Otherwise, theories register the same statistic twice. This is a larger problem, though, for creating multiple instances of theories, and that is unaddressed. Still, separating out the expr statistics into a separate registry is probably a good idea, since the expr package is somewhat separate anyway (and in the short term it allows two SmtEngines to co-exist).