From e52eed325c96b2748734592c3df9ed9b883cadac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Jun 2020 09:22:38 -0700 Subject: [PATCH] close #4450 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 6273e675d..9730334b9 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -963,6 +963,8 @@ private: for (expr * f : m_fmls) { expr_ref tmp(m); eval(f, tmp); + if (m.limit().is_canceled()) + return; CTRACE("sat", !m.is_true(tmp), tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n"; model_smt2_pp(tout, m, *(mdl.get()), 0););