diff options
Diffstat (limited to 'src/expr/nary_term_util.cpp')
| -rw-r--r-- | src/expr/nary_term_util.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp index 4071e0d0e..a872c64c7 100644 --- a/src/expr/nary_term_util.cpp +++ b/src/expr/nary_term_util.cpp @@ -119,9 +119,11 @@ 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(Rational(0)); break; + case PLUS: nullTerm = nm->mkConst(CONST_RATIONAL, Rational(0)); break; case MULT: - case NONLINEAR_MULT: nullTerm = nm->mkConst(Rational(1)); break; + case NONLINEAR_MULT: + nullTerm = nm->mkConst(CONST_RATIONAL, Rational(1)); + break; case STRING_CONCAT: // handles strings and sequences nullTerm = theory::strings::Word::mkEmptyWord(tn); |