From f501380e89add66b54013996823a88c3822f9d47 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 6 Mar 2020 23:36:04 +0100
Subject: [PATCH] fix #3169 - set cancellation timeout and limit during push.
 Also expose internalization outside of scope that disables cancellation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bit_blaster/bit_blaster.cpp  |  1 +
 .../bit_blaster/bit_blaster_tpl_def.h         |  4 ++--
 src/cmd_context/cmd_context.cpp               | 21 +++++++++++++++----
 src/smt/smt_context.cpp                       |  4 ++--
 src/util/rlimit.h                             |  2 +-
 src/util/timeout.cpp                          |  3 ++-
 6 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.cpp b/src/ast/rewriter/bit_blaster/bit_blaster.cpp
index 6632fe811..e43c99983 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "ast/ast_pp.h"
 #include "ast/bv_decl_plugin.h"
 
+
 bit_blaster_cfg::bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, bool_rewriter& rw):
     m_util(u),
     m_params(p),
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 11be2f72e..6dd1ca403 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -16,10 +16,10 @@ Author:
 Revision History:
 
 --*/
-#include "ast/rewriter/bit_blaster/bit_blaster_tpl.h"
 #include "util/rational.h"
-#include "ast/ast_pp.h"
 #include "util/common_msgs.h"
+#include "ast/rewriter/bit_blaster/bit_blaster_tpl.h"
+#include "ast/ast_pp.h"
 #include "ast/rewriter/rewriter_types.h"
 
 
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index b3d14c8da..6441f1462 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1382,11 +1382,24 @@ void cmd_context::push() {
     s.m_macros_stack_lim       = m_macros_stack.size();
     s.m_aux_pdecls_lim         = m_aux_pdecls.size();
     s.m_assertions_lim         = m_assertions.size();
+    unsigned timeout = m_params.m_timeout;
     m().limit().push(m_params.rlimit());
-    if (m_solver) 
-        m_solver->push();
-    if (m_opt)
-        m_opt->push();
+    cancel_eh<reslimit> eh(m().limit());
+    scoped_ctrl_c ctrlc(eh);
+    scoped_timer timer(timeout, &eh);
+    scoped_rlimit _rlimit(m().limit(), m_params.rlimit());
+    try {
+        if (m_solver) 
+            m_solver->push();
+        if (m_opt)
+            m_opt->push();
+    }
+    catch (z3_error & ex) {
+        throw ex;
+    }
+    catch (z3_exception & ex) {
+        throw cmd_exception(ex.msg());
+    }
 }
 
 void cmd_context::push(unsigned n) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 464a3d78c..3149e360d 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2886,12 +2886,12 @@ namespace smt {
     }
 
     void context::push() {
-        TRACE("unit_subsumption_bug", display(tout << "context::push()\n"););
-        scoped_suspend_rlimit _suspend_cancel(m.limit());
+        TRACE("unit_subsumption_bug", display(tout << "context::push()\n"););        
         pop_to_base_lvl();
         setup_context(false);
         bool was_consistent = !inconsistent();
         internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
+        scoped_suspend_rlimit _suspend_cancel(m.limit());
         propagate();
         if (was_consistent && inconsistent()) {
             // logical context became inconsistent during user PUSH
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
index 7f8f7f67f..6502c0426 100644
--- a/src/util/rlimit.h
+++ b/src/util/rlimit.h
@@ -49,7 +49,7 @@ public:
     bool inc(unsigned offset);
     uint64_t count() const;
 
-
+    bool suspended() const { return m_suspend;  }
     bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; }
     char const* get_cancel_msg() const;
     void cancel();
diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp
index 1a92ae867..e4f6eee39 100644
--- a/src/util/timeout.cpp
+++ b/src/util/timeout.cpp
@@ -33,8 +33,9 @@ namespace {
 class g_timeout_eh : public event_handler {
 public:
     void operator()(event_handler_caller_t caller_id) override {
-        std::cout << "timeout\n";
         m_caller_id = caller_id;
+        std::cout << "timeout\n";
+        std::cout.flush();
         if (g_on_timeout)
             g_on_timeout();
         throw z3_error(ERR_TIMEOUT);