diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 9d1bab077..6bea4f449 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -95,6 +95,8 @@ protected: m_solver.push(); reduce(fml); m_solver.pop(1); + if (m.canceled()) + return; SASSERT(m_solver.get_scope_level() == 0); TRACE("ctx_solver_simplify_tactic", for (unsigned i = 0; i < fmls.size(); ++i) {