diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-10 17:06:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-10 17:06:30 -0500 |
| commit | 09be883cb1e27635426a3ca6c296a3557a07f2e0 (patch) | |
| tree | 1d476a0a140644ba847a7ee499f1ac08244720ab /src/theory | |
| parent | b99e0654867bdc40d9c3d30779c0f800d410ea54 (diff) | |
Fix issue related to enum in cegqi (#3267)
Diffstat (limited to 'src/theory')
| -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 |