Fix issue related to enum in cegqi (#3267)

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 0c3f1f69bf246fb594a7e9d76795272e2cc44e62..e71f2b1572e83a125bbdc18ea7f0d0fc29b7ccc7 100644 (file)
--- 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