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 4ffd88fa6006a1ee1f41c376b488dfc90df8c885..53a9f0c912267f1ed459ee104bccb7bd6e698708 100644 (file)
--- 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 5b79c59d95ee6283ab6dfe5725ebe4afda3c0003..352f1e884088d1e11eb058b5c513b9d4eeb702b1 100644 (file)
--- 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]))