[proof-new] Have mkScope agnostic to True assumptions (#5086)

1 files changed, 18 insertions, 1 deletions

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 54315ee05..66a8197d8 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -22,7 +22,11 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) {}
+ProofNodeManager::ProofNodeManager(ProofChecker* pc)
+    : d_checker(pc)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+}
 
 std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
     PfRule id,
@@ -88,6 +92,19 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
       acu.insert(a);
       continue;
     }
+    // trivial assumption
+    if (a == d_true)
+    {
+      Trace("pnm-scope") << "- justify trivial True assumption\n";
+      for (std::shared_ptr<ProofNode> pfs : fa.second)
+      {
+        Assert(pfs->getResult() == a);
+        updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a});
+      }
+      Trace("pnm-scope") << "...finished" << std::endl;
+      acu.insert(a);
+      continue;
+    }
     Trace("pnm-scope") << "- try matching free assumption " << a << "\n";
     // otherwise it may be due to symmetry?
     Node aeqSym = CDProof::getSymmFact(a);