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

@@ -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),

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"
 
 

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

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

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();

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