From 893e60459369e1b781c3d99015c03d2089dd8c5e Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Sat, 11 May 2019 17:34:53 +0200 Subject: [PATCH] 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";