In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or not negBa...

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 2cf313fc2f118661537945f688f169e45a33002d..786499bf0f10e874cba450dba92dfb75b336265b 100644 (file)
--- 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;
 }