From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 May 2022 21:04:56 +0000 (-0500)
Subject: Fix type of null terminator for ADD/MULT for LFSC (#8762)
X-Git-Tag: cvc5-1.0.1~141
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c2ddbb00d94253906c1a2a9f3d2abd6a0286698a;p=cvc5.git

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 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;