diff options
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 0c3f1f69b..e71f2b157 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -184,7 +184,10 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, uires = mkNegateCTT(ires); if (d_type.isInteger()) { - uval = nm->mkNode(PLUS, val, nm->mkConst(Rational(uires))); + uval = nm->mkNode( + PLUS, + val, + nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); uval = Rewriter::rewrite(uval); } else @@ -249,7 +252,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, if (d_type.isInteger()) { uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER; - uval = nm->mkNode(PLUS, val, nm->mkConst(Rational(uires))); + uval = nm->mkNode( + PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); uval = Rewriter::rewrite(uval); } else |