From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 24 May 2022 19:13:29 +0000 (-0500)
Subject: Fix subtype issues in proofs for nonlinear solver (#8782)
X-Git-Tag: cvc5-1.0.1~100
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=675c1b118102395503a060675081f4c11e7c9583;p=cvc5.git

Fix subtype issues in proofs for nonlinear solver (#8782)

Causes a debug proof failure on proof-new.
---

diff --git a/src/theory/arith/nl/coverings/proof_generator.cpp b/src/theory/arith/nl/coverings/proof_generator.cpp
index 4ffd88fa6..53a9f0c91 100644
--- a/src/theory/arith/nl/coverings/proof_generator.cpp
+++ b/src/theory/arith/nl/coverings/proof_generator.cpp
@@ -18,6 +18,7 @@
 #ifdef CVC5_POLY_IMP
 
 #include "proof/lazy_tree_proof_generator.h"
+#include "theory/arith/arith_utilities.h"
 #include "theory/arith/nl/poly_conversion.h"
 #include "util/indexed_root_predicate.h"
 
@@ -155,7 +156,8 @@ void CoveringsProofGenerator::addDirect(Node var,
     // Excludes a single point only
     auto ids = getRootIDs(roots, get_lower(interval));
     Assert(ids.first == ids.second);
-    res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
+    res.emplace_back(
+        mkIRP(var, Kind::EQUAL, mkZero(var.getType()), ids.first, poly, vm));
   }
   else
   {
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 5b79c59d9..352f1e884 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -372,11 +372,11 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
                 proof->addStep(exp[1][0],
                                PfRule::AND_ELIM,
                                {exp[1]},
-                               {nm->mkConstReal(Rational(0))});
+                               {nm->mkConstInt(Rational(0))});
                 proof->addStep(exp[1][1],
                                PfRule::AND_ELIM,
                                {exp[1]},
-                               {nm->mkConstReal(Rational(1))});
+                               {nm->mkConstInt(Rational(1))});
                 Node lb = nm->mkNode(Kind::GEQ, simpleeq[0], simpleeq[1]);
                 Node rb = nm->mkNode(Kind::LEQ, simpleeq[0], simpleeq[1]);
                 if (rew->rewrite(lb) == rew->rewrite(exp[1][0]))