projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e799ab0) | patch
Fix stale reference in MiniSat when generating UC (#2113)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 28 Jun 2018 19:18:47 +0000 (12:18 -0700)
committerGitHub <noreply@github.com>
Thu, 28 Jun 2018 19:18:47 +0000 (12:18 -0700)
commitaa0c64d35814ef892dbcd0cec805d44599009c41
treeba17209644a2d8c2662728c327416ee42b449f8btree
parente799ab0164722e8a4f192ee13223d0eeec6ec004commit | diff
Fix stale reference in MiniSat when generating UC (#2113)

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.
src/prop/minisat/core/Solver.cc diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 [new file with mode: 0644] blob