diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 1156b2f9e..1d8a59d36 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -1065,6 +1065,7 @@ void normalize (expr *e, expr_ref &out, // equivalence classes expr_equiv_class eq_classes(out.m()); factor_eqs(v, eq_classes); + rewrite_eqs(v, eq_classes); equiv_to_expr(eq_classes, v); }