From f999c14a1ec97032738b7bde50eb50d301726453 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 4 Jun 2020 01:33:28 -0700
Subject: [PATCH] close #4429

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/spacer/spacer_util.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 68974fb56..09d712dff 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -383,7 +383,7 @@ namespace {
             expr_ref res(m), v(m);
             v = m_model(e);
             // the literal must have a value
-            SASSERT(m.is_true(v) || m.is_false(v));
+            SASSERT(m.limit().is_canceled() || m.is_true(v) || m.is_false(v));
 
             res = m.is_false(v) ? m.mk_not(e) : e;