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) {