From c06d33bd3dc6bf88f6424f75c3055b219e830713 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 19 Dec 2024 16:05:11 -0600
Subject: [PATCH] Fixes

---
 src/proof/conv_proof_generator.cpp     |  4 ----
 src/theory/arith/arith_proof_rcons.cpp |  9 +++++----
 src/theory/quantifiers/bv_inverter.cpp | 16 +++++++++-------
 3 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp
index 6c66381e93a..91a8511fe6d 100644
--- a/src/proof/conv_proof_generator.cpp
+++ b/src/proof/conv_proof_generator.cpp
@@ -199,8 +199,6 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
   if (f[0] == f[1])
   {
     // assertion failure in debug
-    Assert(false) << "TConvProofGenerator::getProofFor: " << identify()
-                  << ": don't ask for trivial proofs";
     lpf.addStep(f, ProofRule::REFL, {}, {f[0]});
   }
   else
@@ -255,8 +253,6 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
   if (conc[1] == n)
   {
     // assertion failure in debug
-    Assert(false) << "TConvProofGenerator::getProofForRewriting: " << identify()
-                  << ": don't ask for trivial proofs";
     lpf.addStep(conc, ProofRule::REFL, {}, {n});
   }
   std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
diff --git a/src/theory/arith/arith_proof_rcons.cpp b/src/theory/arith/arith_proof_rcons.cpp
index 6cd6d45b66d..752fbc9dd52 100644
--- a/src/theory/arith/arith_proof_rcons.cpp
+++ b/src/theory/arith/arith_proof_rcons.cpp
@@ -18,6 +18,7 @@
 #include "expr/term_context.h"
 #include "proof/conv_proof_generator.h"
 #include "proof/proof.h"
+#include "proof/proof_node.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_subs.h"
 
@@ -80,7 +81,7 @@ std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
     ArithSubsTermContext astc;
     TConvProofGenerator tcnv(d_env,
                              nullptr,
-                             TConvPolicy::FIXPOINT,
+                             TConvPolicy::ONCE,
                              TConvCachePolicy::NEVER,
                              "ArithRConsTConv",
                              &astc);
@@ -105,7 +106,7 @@ std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
         if (a != as)
         {
           std::shared_ptr<ProofNode> pfn = tcnv.getProofForRewriting(a);
-          Assert(pfn.getResult()[1] == as);
+          Assert(pfn->getResult()[1] == as);
           cdp.addProof(pfn);
           cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {});
         }
@@ -136,7 +137,7 @@ std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
             if (a != as)
             {
               std::shared_ptr<ProofNode> pfn = tcnv.getProofForRewriting(a);
-              Assert(pfn.getResult()[1] == as);
+              Assert(pfn->getResult()[1] == as);
               cdp.addProof(pfn);
               cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {});
             }
@@ -172,7 +173,7 @@ std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
         if (a != as)
         {
           std::shared_ptr<ProofNode> pfn = tcnv.getProofForRewriting(a);
-          Assert(pfn.getResult()[1] == as);
+          Assert(pfn->getResult()[1] == as);
           cdp.addProof(pfn);
           cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {});
         }
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 725feb8b36c..5b4128e5399 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -66,16 +66,18 @@ Node BvInverter::mkWitness(const Node& annot) const
       d_nm, ProofRule::MACRO_EXISTS_INV_CONDITION, {annot});
   Trace("bv-invert-witness")
       << "...returned " << w << " for " << annot << std::endl;
-  Assert(!w.isNull());
-  if (d_rewriter != nullptr)
+  if (!w.isNull())
   {
-    Node neww = d_rewriter->rewrite(w);
-    if (neww != w)
+    if (d_rewriter != nullptr)
     {
-      Trace("bv-invert-witness")
-          << "Witness " << w << " was rewritten to " << neww << std::endl;
+      Node neww = d_rewriter->rewrite(w);
+      if (neww != w)
+      {
+        Trace("bv-invert-witness")
+            << "Witness " << w << " was rewritten to " << neww << std::endl;
+      }
+      w = neww;
     }
-    w = neww;
   }
   return w;
 }