diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-28 12:18:47 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-28 12:18:47 -0700 |
| commit | aa0c64d35814ef892dbcd0cec805d44599009c41 (patch) | |
| tree | ba17209644a2d8c2662728c327416ee42b449f8b /test/regress/Makefile.tests | |
| parent | e799ab0164722e8a4f192ee13223d0eeec6ec004 (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.
Diffstat (limited to 'test/regress/Makefile.tests')
| -rw-r--r-- | test/regress/Makefile.tests | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 939b52128..83f1c0714 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1600,6 +1600,7 @@ REG2_TESTS = \ regress2/ooo.rf6.smt2 \ regress2/ooo.tag10.smt2 \ regress2/piVC_5581bd.smt2 \ + regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 \ regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \ regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \ regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \ |