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

Age	Commit message (Collapse)	Author
2021-06-09	Reorder ITE rewrites (#6723)	Andres Noetzli
	Fixes #6717. Commit 11c1fba added some new rewrites for ITE. Due to the new rewrites taking precedence over existing rewrites, it could happen that some of the previous rewrites did not apply anymore even though they would have further simplified the ITE. In the example from the issue, (ite c c true) was rewritten to (or (not T) T) instead of (ite T true true) and then true. The commit fixes the issue by moving rewrites resulting in conjunctions/disjunctions to the end.
2020-12-08	Add regression from #1978. (#5552)	Gereon Kremer
	This PR adds a regression from #1978 that has been fixed in the meantime. Closes #1978 .