From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Sep 2019 22:06:30 +0000 (-0500)
Subject: Fix issue related to enum in cegqi (#3267)
X-Git-Tag: cvc5-1.0.0~3969
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09be883cb1e27635426a3ca6c296a3557a07f2e0;p=cvc5.git

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