From d9faf4b76212a17148e4d6998752f85e417b359b Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 18 Oct 2024 11:46:04 -0500 Subject: [PATCH] Fixes --- src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp | 9 +++++++-- src/theory/arith/nl/ext/monomial_check.cpp | 2 +- 2 files changed, 8 insertions(+), 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 index be0c8d9d941..0d71a30aace 100644 --- 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()) : 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 index c58439b02a3..fb5351e451a 100644 --- 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