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 f51b9d93425..cb61c2c9713 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();