mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

break build again

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-11 14:53:12 -07:00
parent d278a1651d
commit d2ce7b0ea2
2 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sls_euf_plugin.cpp
View file

@ -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));
}
}
}

15
src/qe/qe_mbp.cpp
View file

@ -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<app_const_arr_rewriter>;
template class rewriter_tpl<rd_over_wr_rewriter>;
template class rewriter_tpl<qembp::app_const_arr_rewriter>;
template class rewriter_tpl<qembp::rd_over_wr_rewriter>;
void rewrite_as_const_arr(expr* in, model& mdl, expr_ref& out) {
app_const_arr_rewriter cfg(out.m(), mdl);
rewriter_tpl<app_const_arr_rewriter> rw(out.m(), false, cfg);
qembp::app_const_arr_rewriter cfg(out.m(), mdl);
rewriter_tpl<qembp::app_const_arr_rewriter> 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<rd_over_wr_rewriter> rw(out.m(), false, cfg);
qembp::rd_over_wr_rewriter cfg(out.m(), mdl);
rewriter_tpl<qembp::rd_over_wr_rewriter> rw(out.m(), false, cfg);
rw(in, out);
if (cfg.m_sc.empty()) return;
expr_ref_vector sc(out.m());