From c2ddbb00d94253906c1a2a9f3d2abd6a0286698a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 May 2022 16:04:56 -0500 Subject: [PATCH] Fix type of null terminator for ADD/MULT for LFSC (#8762) This fixes many LFSC proof failures that are occurring now because of using 1.0 instead 1 as null terminator for MULT, and 0.0 instead of 0 for ADD. --- src/expr/nary_term_util.cpp | 10 ++++++++-- src/expr/node_converter.cpp | 2 +- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp index 4aa780d7f..03333b9e8 100644 --- a/src/expr/nary_term_util.cpp +++ b/src/expr/nary_term_util.cpp @@ -119,10 +119,16 @@ Node getNullTerminator(Kind k, TypeNode tn) case OR: nullTerm = nm->mkConst(false); break; case AND: case SEP_STAR: nullTerm = nm->mkConst(true); break; - case ADD: nullTerm = nm->mkConstRealOrInt(tn, Rational(0)); break; + case ADD: + // Note that we ignore the type. This is safe since ADD is permissive + // for subtypes. + nullTerm = nm->mkConstInt(Rational(0)); + break; case MULT: case NONLINEAR_MULT: - nullTerm = nm->mkConstRealOrInt(tn, Rational(1)); + // Note that we ignore the type. This is safe since multiplication is + // permissive for subtypes. + nullTerm = nm->mkConstInt(Rational(1)); break; case STRING_CONCAT: // handles strings and sequences diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp index 07dd2c4e8..7c79243c5 100644 --- a/src/expr/node_converter.cpp +++ b/src/expr/node_converter.cpp @@ -119,7 +119,7 @@ Node NodeConverter::convert(Node n) Node cret = postConvert(ret); if (!cret.isNull() && ret != cret) { - AlwaysAssert(cret.getType().isComparableTo(ret.getType())) + AlwaysAssert(cret.getType() == ret.getType()) << "Converting " << ret << " to " << cret << " changes type"; Trace("nconv-debug2") << "..post-rewrite changed " << ret << " into " << cret << std::endl; -- 2.30.2