diff options
Diffstat (limited to 'src/expr/nary_term_util.cpp')
| -rw-r--r-- | src/expr/nary_term_util.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp index a872c64c7..03ce637e4 100644 --- a/src/expr/nary_term_util.cpp +++ b/src/expr/nary_term_util.cpp @@ -119,10 +119,10 @@ Node getNullTerminator(Kind k, TypeNode tn) case OR: nullTerm = nm->mkConst(false); break; case AND: case SEP_STAR: nullTerm = nm->mkConst(true); break; - case PLUS: nullTerm = nm->mkConst(CONST_RATIONAL, Rational(0)); break; + case PLUS: nullTerm = nm->mkConstRealOrInt(tn, Rational(0)); break; case MULT: case NONLINEAR_MULT: - nullTerm = nm->mkConst(CONST_RATIONAL, Rational(1)); + nullTerm = nm->mkConstRealOrInt(tn, Rational(1)); break; case STRING_CONCAT: // handles strings and sequences |