Fix assertion failure due to missing clause id (#180)

This commit fixes bug 821. As written in the description of the bug, the issue
is that `id` is not being set on one of the paths in addClause(), specifically
in the case where all but one literal are assigned false and the remaining
literal is assigned true. In that case, we are not actually adding anything and
set the `id` to `ClauseIdUndef`.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 26af5f1467ebf5f240b58c0bafb10f05232e0e0c..0bf5d5d7cea40060e8f13a2cfef72e95c16ea56b 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -428,7 +428,10 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
             }
           }
           return ok;
-        } else return ok;
+        } else {
+          PROOF(id = ClauseIdUndef;);
+          return ok;
+        }
       }
     }
 

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 197f81d63b799c1ec44a87253628aec9ea2afa42..0f250814411cf9f851ca15c8f7072242e387668e 100644 (file)
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -49,7 +49,8 @@ BUG_TESTS = \
   bug765.smt2 \
   bug691.smt2 \
   bug694-Unapply1.scala-0.smt2 \
-  simple_unsat_cores.smt2
+  simple_unsat_cores.smt2 \
+  bug821.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/push-pop/bug821.smt2 b/test/regress/regress0/push-pop/bug821.smt2
new file mode 100644 (file)
index 0000000..b537197
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug821.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+(set-logic UF)
+(push 1)
+(declare-fun _substvar_4_ () Bool)
+(assert _substvar_4_)
+(assert _substvar_4_)
+(check-sat)