From bbcfd79bf699f0bfe509ed3a1d3731c516e01c12 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Mar 2020 08:13:05 +0100
Subject: [PATCH] fix #3129

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/tactic/ctx_solver_simplify_tactic.cpp | 2 ++
 1 file changed, 2 insertions(+)

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) {