From fc1321f8b3559d0182b55b57ad3df4f9ea2ac11c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Apr 2020 21:02:58 -0700 Subject: [PATCH] fix #4104 Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 5866dfedb..f51b9d934 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1406,6 +1406,21 @@ namespace qe { m_conjs.add_plugin(p); } + bool has_uninterpreted(expr* _e) { + expr_ref e(_e, m); + arith_util au(m); + func_decl_ref f_out(m); + for (expr* arg : subterms(e)) { + if (!is_app(arg)) continue; + app* a = to_app(arg); + func_decl* f = a->get_decl(); + if (m.is_considered_uninterpreted(f)) + return true; + if (au.is_considered_uninterpreted(f, a->get_num_args(), a->get_args(), f_out)) + return true; + } + return false; + } void check(unsigned num_vars, app* const* vars, expr* assumption, expr_ref& fml, bool get_first, @@ -1445,6 +1460,8 @@ 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) {