From 09be883cb1e27635426a3ca6c296a3557a07f2e0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 10 Sep 2019 17:06:30 -0500 Subject: [PATCH] Fix issue related to enum in cegqi (#3267) --- src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp | 8 ++++++-- 1 file 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 -- 2.30.2