From f158ab83957bc42cdc565f0f59b1aa6d14b66fe6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Mar 2020 20:48:31 -0700
Subject: [PATCH] fix #3426

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_mbp.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 01507e517..354d63040 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -231,7 +231,8 @@ class mbp::impl {
             expr_ref tmp(m);
             sub(fml, tmp);
             expr_ref val = eval(tmp);
-            SASSERT(m.is_true(val) || m.is_false(val) || m.canceled());
+            if (!m.is_true(val) && !m.is_false(val))
+                return false;
             fmls.push_back(m.is_true(val) ? tmp : mk_not(m, tmp));
         }
         return found_bool;