diff options
Diffstat (limited to 'src/theory/quantifiers/skolemize.cpp')
| -rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 6dcb318f3..4dea0dc22 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -285,10 +285,12 @@ Node Skolemize::mkSkolemizedBody(Node f, } else if (options::intWfInduction() && tn.isInteger()) { - Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0))); - Node iret = ret.substitute(ind_vars[0], - nm->mkNode(MINUS, k, nm->mkConst(Rational(1)))) - .negate(); + Node icond = nm->mkNode(GEQ, k, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node iret = + ret.substitute( + ind_vars[0], + nm->mkNode(MINUS, k, nm->mkConst(CONST_RATIONAL, Rational(1)))) + .negate(); n_str_ind = nm->mkNode(OR, icond.negate(), iret); n_str_ind = nm->mkNode(AND, icond, n_str_ind); } |