From b3c863fb15a843627a8144e3ec2936679b4b2b45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Apr 2020 11:05:03 -0700 Subject: [PATCH] fix #3660 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/rewriter_def.h | 14 ++++++-------- src/opt/opt_context.cpp | 2 +- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index ad02ed532..bb46e1d39 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -101,7 +101,7 @@ bool rewriter_tpl::process_const(app * t0) { result_stack().push_back(m_r.get()); if (ProofGen) { SASSERT(rewrites_from(t0, m_pr)); - SASSERT(rewrites_to(t0, m_pr)); + SASSERT(rewrites_to(m_r, m_pr)); if (m_pr) result_pr_stack().push_back(m_pr); else @@ -296,16 +296,14 @@ void rewriter_tpl::process_app(app * t, frame & fr) { SASSERT(rewrites_to(new_t, m_pr)); } } - m_pr2 = nullptr; br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2); - if (st != BR_FAILED && !rewrites_to(m_r, m_pr2)) enable_trace("reduce_app"); CTRACE("reduce_app", st != BR_FAILED, - tout << mk_bounded_pp(t, m()) << "\n"; - tout << "st: " << st; - if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m()); - tout << "\n"; - tout << m_pr2 << "\n"; + tout << mk_bounded_pp(t, m()) << "\n"; + tout << "st: " << st; + if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m()); + tout << "\n"; + if (m_pr2) tout << mk_bounded_pp(m_pr2, m()) << "\n"; ); SASSERT(st == BR_FAILED || rewrites_to(m_r, m_pr2)); SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8f3f91888..21642323d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -374,7 +374,7 @@ namespace opt { void context::set_model(model_ref& m) { m_model = m; opt_params optp(m_params); - if (optp.dump_models()) { + if (optp.dump_models() && m) { model_ref md = m->copy(); fix_model(md); }