From 880fc776559adbccc4ed48cc43c92b289903ccf8 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 22 Nov 2017 18:29:22 -0500
Subject: [PATCH] Further rewrite equalities

---
 src/muz/spacer/spacer_util.cpp | 1 +
 1 file changed, 1 insertion(+)

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