From e8e27f0daf572f8e6f7d9bb4bd3a2b5c76117888 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 28 Jun 2018 10:59:28 -0400
Subject: [PATCH] Don't simplify bounds when normalizing a lemma

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

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index b034a8fd5..b6d9f810d 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -538,7 +538,8 @@ void lemma::mk_expr_core() {
     SASSERT(!m_cube.empty());
     m_body = ::mk_and(m_cube);
     // normalize works better with a cube
-    normalize(m_body, m_body);
+    normalize(m_body, m_body, false /* no simplify bounds */, false /* term_graph */);
+
     m_body = ::push_not(m_body);
 
     if (!m_zks.empty() && has_zk_const(m_body)) {