diff options
author | Tim King <tim.king@imag.fr> | 2015-06-12 17:11:29 +0200 |
---|---|---|
committer | Tim King <tim.king@imag.fr> | 2015-06-12 17:11:29 +0200 |
commit | 2a76e73bb626983c7b12ea83fed7a6f371011985 (patch) | |
tree | a2a43674375f2247e6d898ec378b438d1aa3f94b /src | |
parent | 61415ee2c5659893055f71d84a38eab8701dc47a (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 9 |
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; } |