Add trace to see inferences in final proof (#7813)

Adds -t im-pf to see which inferences occur in the final proof. Must be used with proofs and --proof-annotate.

diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
index 484f0dd73d0a2c712506c5ca34b96c8253669ed7..4cf3a68f73401caf531aee7585901c5276432675 100644 (file)
--- a/src/smt/proof_final_callback.cpp
+++ b/src/smt/proof_final_callback.cpp
@@ -109,6 +109,12 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
       if (getInferenceId(args[0], id))
       {
         d_annotationRuleIds << id;
+        // Use e.g. `--check-proofs --proof-annotate -t im-pf` to see a list of
+        // inference that appear in the final proof.
+        Trace("im-pf") << "(inference-pf " << id << " " << pn->getResult()
+                       << ")" << std::endl;
+        Trace("im-pf-assert")
+            << "(assert " << pn->getResult() << ") ; " << id << std::endl;
       }
     }
   }