From 5c82e1dd02c304dd34c72ffcc966840e8b3005ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 15 Dec 2021 09:15:26 -0600 Subject: [PATCH] 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. --- src/smt/proof_final_callback.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp index 484f0dd73..4cf3a68f7 100644 --- a/src/smt/proof_final_callback.cpp +++ b/src/smt/proof_final_callback.cpp @@ -109,6 +109,12 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr 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; } } } -- 2.30.2