From b29d5f9b5d09a53bef6092a756671586be2a746a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Jun 2020 21:21:01 -0700 Subject: [PATCH] fix #4436 Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 15d7ee825..e2bb32b89 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -216,7 +216,7 @@ public: tout << *m_model << "assumptions: "; for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " "; tout << "\n";); - SASSERT(m_model->is_true(m_asms)); + SASSERT(m_model->is_true(m_asms) || m.limit().is_canceled()); found_optimum(); return l_true; case l_false: