From 6d4bd37e15214803192a380dc5af46576d9a1eb5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Apr 2020 21:04:04 -0700
Subject: [PATCH] fix #4104
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/qe/qe.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index f51b9d934..cb61c2c97 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1460,10 +1460,10 @@ namespace qe {
if (assumption) m_solver.assert_expr(assumption);
bool is_sat = false;
lbool res = l_true;
- if (has_uninterpreted(m_fml))
- res = l_undef;
while (res == l_true) {
res = m_solver.check();
+ if (res == l_true && has_uninterpreted(m_fml))
+ res = l_undef;
if (res == l_true) {
is_sat = true;
final_check();