From 893e60459369e1b781c3d99015c03d2089dd8c5e Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Sat, 11 May 2019 17:34:53 +0200 Subject: [PATCH 1/2] generate rewrite proof object early on to avoid logging equality term twice --- src/ast/rewriter/th_rewriter.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 9390e21ee..941437137 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -579,6 +579,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { app_ref tmp(m()); tmp = m().mk_app(f, num, args); m().trace_stream() << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n"; + if (m().proofs_enabled()) + result_pr = m().mk_rewrite(tmp, result); tmp = m().mk_eq(tmp, result); m().trace_stream() << "[instance] " << static_cast(nullptr) << " #" << tmp->get_id() << "\n"; m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; From 1e2fe9e7640acac7e4b131a9858e24b1282a06b7 Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Sat, 11 May 2019 20:13:48 +0200 Subject: [PATCH 2/2] bug fix --- src/ast/rewriter/th_rewriter.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 941437137..3f1f168dd 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -583,6 +583,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { result_pr = m().mk_rewrite(tmp, result); tmp = m().mk_eq(tmp, result); m().trace_stream() << "[instance] " << static_cast(nullptr) << " #" << tmp->get_id() << "\n"; + m().trace_stream() << "[attach-enode] #" << result->get_id() << " 0\n"; m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; m().trace_stream() << "[end-of-instance]\n"; m().trace_stream().flush();