From f67346d16e6abe41d5a0e2b664103914a1be1d74 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 4 Sep 2018 21:48:07 -0400
Subject: [PATCH] Fix is_infty_level to treat 2^16-1 as infinity

---
 src/muz/spacer/spacer_prop_solver.cpp | 1 +
 src/muz/spacer/spacer_util.h          | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index 004ea6754..4899ad692 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -94,6 +94,7 @@ void prop_solver::add_level()
 
 void prop_solver::ensure_level(unsigned lvl)
 {
+    if (is_infty_level(lvl)) return;
     while (lvl >= level_cnt()) {
         add_level();
     }
diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h
index 8da574d0e..0328d8640 100644
--- a/src/muz/spacer/spacer_util.h
+++ b/src/muz/spacer/spacer_util.h
@@ -48,7 +48,8 @@ namespace spacer {
     }
 
     inline bool is_infty_level(unsigned lvl) {
-        return lvl == infty_level ();
+        // XXX: level is 16 bits in class pob
+        return lvl >= 65535;
     }
 
     inline unsigned next_level(unsigned lvl) {