Fixes

ajreynol · Oct 18, 2024 · d9faf4b · d9faf4b
1 parent 35cbd66
commit d9faf4b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp
@@ -100,6 +100,11 @@ std::string ArithNlCompareProofGenerator::identify() const
   return "ArithNlCompareProofGenerator";
 }
 
+Node ensureReal(NodeManager * nm, const Node& n)
+{
+  return n.isConst() ? nm->mkConstReal(n.getConst<Rational>()) : nm->mkNode(Kind::TO_REAL, n);
+}
+
 Node ArithNlCompareProofGenerator::mkLit(
     NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute)
 {
@@ -110,11 +115,11 @@ Node ArithNlCompareProofGenerator::mkLit(
     // must resolve subtype issues here
     if (au.getType().isInteger())
     {
-      au = nm->mkNode(Kind::TO_REAL, au);
+      au = ensureReal(nm, au);
     }
     else
     {
-      bu = nm->mkNode(Kind::TO_REAL, bu);
+      bu = ensureReal(nm, bu);
     }
   }
   // add absolute value

diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -434,7 +434,7 @@ bool MonomialCheck::compareMonomial(
       {
         cob = mkOne(oa.getType());
       }
-      Node conc = mkAndNotifyLit(oa, ob, status, true);
+      Node conc = mkAndNotifyLit(oa, cob, status, true);
       Node clem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc);
       Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl;
       // use dedicated proof generator d_ancPfGen