From 7bbe3fb2b6e095bc15e5e23e4843049e7846b761 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Sat, 9 Mar 2024 23:13:42 +0000
Subject: [PATCH] fix (get-proof) command to respect option pp.simplify_implies
 (#7157)

---
 src/ast/ast_smt_pp.cpp         | 10 +++++-----
 src/cmd_context/basic_cmds.cpp |  1 +
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index bea669438..0da4f1c12 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -986,7 +986,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     ast_mark sort_mark;
     for (sort* s : decls.get_sorts()) {
         if (!(*m_is_declared)(s)) {
-            smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
+            smt_printer p(strm, m, ql, rn, m_logic, true, m_simplify_implies, 0);
             p.pp_sort_decl(sort_mark, s);
         }
     }
@@ -994,7 +994,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     for (unsigned i = 0; i < decls.get_num_decls(); ++i) {
         func_decl* d = decls.get_func_decls()[i];
         if (!(*m_is_declared)(d)) {
-            smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
+            smt_printer p(strm, m, ql, rn, m_logic, true, m_simplify_implies, 0);
             p(d);
             strm << "\n";
         }
@@ -1003,20 +1003,20 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
 #endif
 
     for (expr* a : m_assumptions) {
-        smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
+        smt_printer p(strm, m, ql, rn, m_logic, false, m_simplify_implies, 1);
         strm << "(assert\n ";
         p(a);
         strm << ")\n";
     }
 
     for (expr* a : m_assumptions_star) {
-        smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
+        smt_printer p(strm, m, ql, rn, m_logic, false, m_simplify_implies, 1);
         strm << "(assert\n ";
         p(a);
         strm << ")\n";
     }
 
-    smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0);
+    smt_printer p(strm, m, ql, rn, m_logic, false, m_simplify_implies, 0);
     if (m.is_bool(n)) {
         if (!m.is_true(n)) {
             strm << "(assert\n ";
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index a2757d955..c93e4432f 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -202,6 +202,7 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
         cmd_is_declared isd(ctx);
         pp.set_is_declared(&isd);
         pp.set_logic(ctx.get_logic());
+        pp.set_simplify_implies(params.simplify_implies());
         pp.display_smt2(ctx.regular_stream(), pr);
         ctx.regular_stream() << std::endl;
     }