From 09f37e49b05e0d14b29a5e2a5cf390bc66dcc9b4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 26 Oct 2012 14:32:19 -0700 Subject: [PATCH] simplify body Signed-off-by: Nikolaj Bjorner --- src/muz_qe/horn_subsume_model_converter.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/muz_qe/horn_subsume_model_converter.cpp b/src/muz_qe/horn_subsume_model_converter.cpp index 6a150333a..1a6785117 100644 --- a/src/muz_qe/horn_subsume_model_converter.cpp +++ b/src/muz_qe/horn_subsume_model_converter.cpp @@ -186,30 +186,29 @@ void horn_subsume_model_converter::operator()(model_ref& mr) { TRACE("dl_mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";); expr_ref tmp(body); mr->eval(tmp, body); - m_rewrite(body); TRACE("dl_mc", tout << "to:\n" << mk_pp(body, m) << "\n";); if (arity == 0) { expr* e = mr->get_const_interp(h); if (e) { - mr->register_decl(h, m.mk_or(e, body)); - } - else { - mr->register_decl(h, body); + body = m.mk_or(e, body); } + m_rewrite(body); + mr->register_decl(h, m.mk_or(e, body)); } else { func_interp* f = mr->get_func_interp(h); if (f) { expr* e = f->get_else(); - f->set_else(m.mk_or(e, body.get())); + body = m.mk_or(e, body); } else { f = alloc(func_interp, m, arity); - f->set_else(body); mr->register_decl(h, f); } + m_rewrite(body); + f->set_else(body); } } }