From 3a97451f8cffbd1e7310913b0c7db19566dbd5b4 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 30 May 2018 09:05:05 -0700
Subject: [PATCH] spacer: normalize the cube before creating a lemma

---
 src/muz/spacer/spacer_context.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 491349a4e..5f8951ecb 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -487,8 +487,10 @@ void lemma::mk_expr_core() {
     if (m_pob) {mk_cube_core();}
 
     SASSERT(!m_cube.empty());
-    m_body = ::push_not(::mk_and(m_cube));
+    m_body = ::mk_and(m_cube);
+    // normalize works better with a cube
     normalize(m_body, m_body);
+    m_body = ::push_not(m_body);
 
     if (!m_zks.empty() && has_zk_const(m_body)) {
             app_ref_vector zks(m);