1 files changed, 17 insertions, 2 deletions
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 3980a3cb3..df0258af7 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -109,9 +109,24 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
 
 void LazyCDProof::addLazyStep(Node expected,
                               ProofGenerator* pg,
-                              bool forceOverwrite)
+                              bool forceOverwrite,
+                              PfRule idNull)
 {
-  Assert(pg != nullptr);
+  if (pg == nullptr)
+  {
+    // null generator, should have given a proof rule
+    if (idNull == PfRule::ASSUME)
+    {
+      Assert(false);
+      return;
+    }
+    Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
+                          << " set (trusted) step " << idNull << "\n";
+    addStep(expected, idNull, {}, {expected});
+    return;
+  }
+  Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
+                        << " set to generator " << pg->identify() << "\n";
   if (!forceOverwrite)
   {
     NodeProofGeneratorMap::const_iterator it = d_gens.find(expected);