From: Tim King <tim.king@imag.fr>
Date: Fri, 12 Jun 2015 15:11:29 +0000 (+0200)
Subject: In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or not negBa... 
X-Git-Tag: cvc5-1.0.0~6289
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a76e73bb626983c7b12ea83fed7a6f371011985;p=cvc5.git

In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or not negBack is already in conflict. This is needed as it can be called multiple times on the same constraint.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 2cf313fc2..786499bf0 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2360,8 +2360,15 @@ ConstraintCP TheoryArithPrivate::vectorToIntHoleConflict(const ConstraintCPVec&
   Assert(conflict.size() >= 2);
   ConstraintCPVec exp(conflict.begin(), conflict.end()-1);
   ConstraintCP back = conflict.back();
+  Assert(back->hasProof());
   ConstraintP negBack = back->getNegation();
-  negBack->impliedByIntHole(exp, true);
+  // This can select negBack multiple times so we need to test if negBack has a proof.
+  if(negBack->hasProof()){
+    // back is in conflict already
+  } else {
+    negBack->impliedByIntHole(exp, true);
+  }
+
   return back;
 }