mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

Further rewrite equalities

Browse source
This commit is contained in:
Arie Gurfinkel 2017-11-22 18:29:22 -05:00
parent 6818eb3340
commit 880fc77655
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/muz/spacer/spacer_util.cpp
View file

@ -1065,6 +1065,7 @@ void normalize (expr *e, expr_ref &out,
// equivalence classes // equivalence classes
expr_equiv_class eq_classes(out.m()); expr_equiv_class eq_classes(out.m());
factor_eqs(v, eq_classes); factor_eqs(v, eq_classes);
rewrite_eqs(v, eq_classes);
equiv_to_expr(eq_classes, v); equiv_to_expr(eq_classes, v);
} }