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

Age	Commit message (Collapse)	Author
2018-06-28	Fix stale reference in MiniSat when generating UC (#2113)	Andres Noetzli
	In MiniSat's analyze(), we were taking a reference of a clause that could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can lead to allocation of clauses which in turn can lead to clauses being reallocated, making the reference stale. The commit encloses the reference in a code block that makes the lifetime of the reference more obvious and removes uses of the potentially stale reference.