carefully printing trusted assertions in proofs (#2505)

1 files changed, 6 insertions, 0 deletions

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 89aa66c2d..0342288fe 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -239,6 +239,12 @@ public:
   // for SMT variable names that have spaces and other things
   static std::string sanitize(TNode var);
 
+  // wrap term with (p_app ... ) if the term is printed as a boolean, and print
+  // used for "trust" assertions
+  static void printTrustedTerm(Node term,
+                               std::ostream& os,
+                               ProofLetMap& globalLetMap);
+
   /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/
   void addAssertion(Expr formula);