From: Andres Nötzli <andres.noetzli@gmail.com>
Date: Fri, 16 Jun 2017 18:16:04 +0000 (-0700)
Subject: Fix segfault by making unit conflict CDMaybe
X-Git-Tag: cvc5-1.0.0~5769
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=38df3307e0503d4b4c69c31e8688da1c03b80bde;p=cvc5.git

Fix segfault by making unit conflict CDMaybe

This commit fixes bug 819 by making d_unitConflictId context dependent and adds a test case.
---

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 5691d1bd2..36de6278a 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -29,6 +29,7 @@
 #include <vector>
 
 #include "context/cdhashmap.h"
+#include "context/cdmaybe.h"
 #include "expr/expr.h"
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
@@ -349,8 +350,7 @@ class TSatProof {
   IdCRefMap d_temp_idClause;
 
   // unit conflict
-  ClauseId d_unitConflictId;
-  bool d_storedUnitConflict;
+  context::CDMaybe<ClauseId> d_unitConflictId;
 
   ClauseId d_trueLit;
   ClauseId d_falseLit;
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index eb4e04d13..6cb10450a 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -218,8 +218,7 @@ TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
       d_nullId(-2),
       d_temp_clauseId(),
       d_temp_idClause(),
-      d_unitConflictId(),
-      d_storedUnitConflict(false),
+      d_unitConflictId(context),
       d_trueLit(ClauseIdUndef),
       d_falseLit(ClauseIdUndef),
       d_name(name),
@@ -867,12 +866,11 @@ template <class Solver>
 ClauseId TSatProof<Solver>::storeUnitConflict(
     typename Solver::TLit conflict_lit, ClauseKind kind) {
   Debug("cores") << "STORE UNIT CONFLICT" << std::endl;
-  Assert(!d_storedUnitConflict);
-  d_unitConflictId = registerUnitClause(conflict_lit, kind);
-  d_storedUnitConflict = true;
-  Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId
+  Assert(!d_unitConflictId.isSet());
+  d_unitConflictId.set(registerUnitClause(conflict_lit, kind));
+  Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId.get()
                               << "\n";
-  return d_unitConflictId;
+  return d_unitConflictId.get();
 }
 
 template <class Solver>
@@ -881,8 +879,8 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
   Assert(conflict_ref != Solver::TCRef_Undef);
   ClauseId conflict_id;
   if (conflict_ref == Solver::TCRef_Lazy) {
-    Assert(d_storedUnitConflict);
-    conflict_id = d_unitConflictId;
+    Assert(d_unitConflictId.isSet());
+    conflict_id = d_unitConflictId.get();
 
     ResChain<Solver>* res = new ResChain<Solver>(conflict_id);
     typename Solver::TLit lit = d_idUnit[conflict_id];
@@ -892,7 +890,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
     return;
 
   } else {
-    Assert(!d_storedUnitConflict);
+    Assert(!d_unitConflictId.isSet());
     conflict_id = registerClause(conflict_ref, LEARNT);  // FIXME
   }
 
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 262132779..197f81d63 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -48,7 +48,8 @@ BUG_TESTS = \
   inc-define.smt2 \
   bug765.smt2 \
   bug691.smt2 \
-  bug694-Unapply1.scala-0.smt2
+  bug694-Unapply1.scala-0.smt2 \
+  simple_unsat_cores.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/push-pop/simple_unsat_cores.smt2 b/test/regress/regress0/push-pop/simple_unsat_cores.smt2
new file mode 100644
index 000000000..e85a546d8
--- /dev/null
+++ b/test/regress/regress0/push-pop/simple_unsat_cores.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic UF)
+(push 1)
+(assert false)
+(check-sat)
+(pop 1)
+(assert false)
+(check-sat)