From 2a76e73bb626983c7b12ea83fed7a6f371011985 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 12 Jun 2015 17:11:29 +0200 Subject: [PATCH] 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. --- src/theory/arith/theory_arith_private.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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; } -- 2.30.2