From 46fb0d928a4585ab9fc3eae3d945f70c576cad08 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 27 Dec 2017 13:01:54 -0500
Subject: [PATCH] Fix in spacer_term_graph

---
 src/muz/spacer/spacer_term_graph.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/muz/spacer/spacer_term_graph.cpp b/src/muz/spacer/spacer_term_graph.cpp
index 5cd531870..0dc29a7c5 100644
--- a/src/muz/spacer/spacer_term_graph.cpp
+++ b/src/muz/spacer/spacer_term_graph.cpp
@@ -157,7 +157,7 @@ public:
             result = mk_le_zero(arg1);
             return true;
         }
-        else if (m_arith.is_numeral(arg2, n)) {
+        else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n < 0) {
             // t <= n ==> t < n + 1 ==> ! (t >= n + 1)
             result = m.mk_not(m_arith.mk_ge(arg1, m_arith.mk_numeral(n+1, true)));
             return true;
@@ -182,7 +182,7 @@ public:
             result = mk_ge_zero(arg1);
             return true;
         }
-        else if (m_arith.is_numeral(arg2, n)) {
+        else if (m_arith.is_int(arg1) && m_arith.is_numeral(arg2, n) && n > 0) {
             // t >= n ==> t > n - 1 ==> ! (t <= n - 1)
             result = m.mk_not(m_arith.mk_le(arg1, m_arith.mk_numeral(n-1, true)));
             return true;