mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-31 12:32:33 -07:00
parent 8d1dfb9f32
commit e2c5e2e39c
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/array_axioms.cpp
View file

@ -197,12 +197,19 @@ namespace array {
expr_ref sel2(a.mk_select(sel2_args), m); expr_ref sel2(a.mk_select(sel2_args), m);
expr_ref sel_eq_e(m.mk_eq(sel1, sel2), m); expr_ref sel_eq_e(m.mk_eq(sel1, sel2), m);
bool new_prop = false;
if (!ctx.get_egraph().find(sel1))
new_prop = true;
if (!ctx.get_egraph().find(sel2))
new_prop = true;
euf::enode* s1 = e_internalize(sel1); euf::enode* s1 = e_internalize(sel1);
euf::enode* s2 = e_internalize(sel2); euf::enode* s2 = e_internalize(sel2);
TRACE("array", TRACE("array",
tout << "select-store " << ctx.bpp(s1) << " " << ctx.bpp(s1->get_root()) << "\n"; tout << "select-store " << ctx.bpp(s1) << " " << ctx.bpp(s1->get_root()) << "\n";
tout << "select-store " << ctx.bpp(s2) << " " << ctx.bpp(s2->get_root()) << "\n";); tout << "select-store " << ctx.bpp(s2) << " " << ctx.bpp(s2->get_root()) << "\n";);
if (s1->get_root() == s2->get_root()) if (s1->get_root() == s2->get_root())
return new_prop; return new_prop;