From 83d1156a59af871983aa38f2d193d3b4e8566a54 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 10 Feb 2020 08:31:44 -0800
Subject: [PATCH] fix #2966
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/qe/qe_sat_tactic.cpp | 11 ++++++++---
1 file changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
index 6eb697880..87c146819 100644
--- a/src/qe/qe_sat_tactic.cpp
+++ b/src/qe/qe_sat_tactic.cpp
@@ -631,7 +631,12 @@ namespace qe {
ctx.set_projection_mode(m_projection_mode_param);
m_solvers[idx+1]->push();
while (ctx.get_num_vars() > 0) {
- VERIFY(l_true == m_solvers[idx+1]->check());
+ lbool r = m_solvers[idx+1]->check();
+ SASSERT(r != l_false);
+ if (r == l_undef) {
+ checkpoint();
+ throw tactic_exception("inconclusive solver result");
+ }
ctx.project_var(ctx.get_num_vars()-1);
}
m_solvers[idx+1]->pop(1);
@@ -648,8 +653,8 @@ namespace qe {
m_Ms[idx] = tmp;
m_solvers[idx]->assert_expr(not_fml);
TRACE("qe",
- tout << mk_pp(fml, m) << "\n--->\n";
- tout << mk_pp(tmp, m) << "\n";);
+ tout << fml << "\n--->\n";
+ tout << tmp << "\n";);
}
void checkpoint() {