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.

diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp
index 4aa780d7fbeefb4a20a8621d3b0e1113d7759b53..03333b9e8f58d6e0c21c2849330ce741a02c768d 100644 (file)
--- 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 07dd2c4e8f1b9b564d83cedbd45af1ac4f3879e3..7c79243c5bcff06d446f3d13e49149e981999561 100644 (file)
--- 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;