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.

1 files changed, 8 insertions, 1 deletions

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;
 }