From d2ce7b0ea283278c59695452fb2539a2f807f98f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Oct 2024 14:53:12 -0700 Subject: [PATCH] break build again --- src/ast/sls/sls_euf_plugin.cpp | 2 +- src/qe/qe_mbp.cpp | 15 ++++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp index aee13acc8..dd0291c4a 100644 --- a/src/ast/sls/sls_euf_plugin.cpp +++ b/src/ast/sls/sls_euf_plugin.cpp @@ -153,7 +153,7 @@ namespace sls { euf::enode* args[2] = { g.find(a), g.find(b) }; c = g.mk(eq, 0, 2, args); } - g.merge(c, g.find(m.mk_false()), to_ptr(lit)); + g.merge(g.find(m.mk_false()), to_ptr(lit)); } } } diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 96ae5e85a..5f5752187 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -42,7 +42,8 @@ Revision History: using namespace qe; -namespace { +namespace qembp { + // rewrite select(store(a, i, k), j) into k if m \models i = j and select(a, j) if m \models i != j struct rd_over_wr_rewriter : public default_rewriter_cfg { ast_manager &m; @@ -124,19 +125,19 @@ namespace { }; } -template class rewriter_tpl; -template class rewriter_tpl; +template class rewriter_tpl; +template class rewriter_tpl; void rewrite_as_const_arr(expr* in, model& mdl, expr_ref& out) { - app_const_arr_rewriter cfg(out.m(), mdl); - rewriter_tpl rw(out.m(), false, cfg); + qembp::app_const_arr_rewriter cfg(out.m(), mdl); + rewriter_tpl rw(out.m(), false, cfg); rw(in, out); } void rewrite_read_over_write(expr *in, model &mdl, expr_ref &out) { - rd_over_wr_rewriter cfg(out.m(), mdl); - rewriter_tpl rw(out.m(), false, cfg); + qembp::rd_over_wr_rewriter cfg(out.m(), mdl); + rewriter_tpl rw(out.m(), false, cfg); rw(in, out); if (cfg.m_sc.empty()) return; expr_ref_vector sc(out.m());