fix #1276 related crashes for re-sumption after cancellation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/maximize_ac_sharing.cpp

@@ -151,11 +151,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) {
 }
 
 void maximize_ac_sharing::reset() {
-    restore_entries(0);
-    m_entries.reset();
     m_cache.reset();
-    m_region.reset();
-    m_scopes.reset();
 }
 
 void maximize_bv_sharing::init_core() {

src/smt/asserted_formulas.cpp

@@ -170,7 +170,7 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
 
 void asserted_formulas::push_scope() {
     SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled());
-    TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout););    
+    TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
     m_scoped_substitution.push();
     m_scopes.push_back(scope());
     scope & s = m_scopes.back();
@@ -181,10 +181,11 @@ void asserted_formulas::push_scope() {
     m_bv_sharing.push_scope();
     m_macro_manager.push_scope();
     commit();
+    TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";);
 }
  
 void asserted_formulas::pop_scope(unsigned num_scopes) {
-    TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout););
+    TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
     m_bv_sharing.pop_scope(num_scopes);
     m_macro_manager.pop_scope(num_scopes);
     unsigned new_lvl    = m_scopes.size() - num_scopes;
@@ -196,7 +197,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
     m_qhead    = s.m_formulas_lim;
     m_scopes.shrink(new_lvl);
     flush_cache();
-    TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout););
+    TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n";);
 }
 
 void asserted_formulas::reset() {

src/smt/smt_context.cpp

@@ -487,6 +487,7 @@ namespace smt {
     */
     void context::add_eq(enode * n1, enode * n2, eq_justification js) {
         unsigned old_trail_size = m_trail_stack.size();
+        scoped_suspend_rlimit _suspend_cancel(m_manager.limit());
 
         try {
             TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
@@ -541,10 +542,14 @@ namespace smt {
                 mark_as_relevant(r1);
             }
 
+            TRACE("add_eq", tout << "to trail\n";);
+
             push_trail(add_eq_trail(r1, n1, r2->get_num_parents()));
 
+            TRACE("add_eq", tout << "qmanager add_eq\n";);
             m_qmanager->add_eq_eh(r1, r2);
 
+            TRACE("add_eq", tout << "merge theory_vars\n";);
             merge_theory_vars(n2, n1, js);
 
             // 'Proof' tree
@@ -577,6 +582,7 @@ namespace smt {
 #endif
 
 
+            TRACE("add_eq", tout << "remove_parents_from_cg_table\n";);
             remove_parents_from_cg_table(r1);
 
             enode * curr = r1;
@@ -588,8 +594,10 @@ namespace smt {
 
             SASSERT(r1->get_root() == r2);
 
+            TRACE("add_eq", tout << "reinsert_parents_into_cg_table\n";);
             reinsert_parents_into_cg_table(r1, r2, n1, n2, js);
 
+            TRACE("add_eq", tout << "propagate_bool_enode_assignment\n";);
             if (n2->is_bool())
                 propagate_bool_enode_assignment(r1, r2, n1, n2);
 
@@ -604,6 +612,7 @@ namespace smt {
         catch (...) {
             // Restore trail size since procedure was interrupted in the middle.
             // If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked.
+            TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m_manager.limit().get_cancel_flag() << "\n";);
             m_trail_stack.shrink(old_trail_size);
             throw;
         }
@@ -972,7 +981,7 @@ namespace smt {
             enode * parent = *it;
             if (parent->is_cgc_enabled()) {
                 TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";);
-                CTRACE("add_eq", !parent->is_cgr(),
+                CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent),
                        tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" <<
                        parent->get_owner_id() << ", parents: \n";
                        for (unsigned i = 0; i < r2->m_parents.size(); i++) {

src/util/rlimit.cpp

@@ -21,6 +21,7 @@ Revision History:
 
 reslimit::reslimit():
     m_cancel(0),
+    m_suspend(false),
     m_count(0),
     m_limit(0) {
 }
@@ -31,12 +32,12 @@ uint64 reslimit::count() const {
 
 bool reslimit::inc() {
     ++m_count;
-    return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
+    return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
 }
 
 bool reslimit::inc(unsigned offset) {
     m_count += offset;
-    return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
+    return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
 }
 
 void reslimit::push(unsigned delta_limit) {

src/util/rlimit.h

@@ -23,12 +23,14 @@ Revision History:
 
 class reslimit {
     volatile unsigned   m_cancel;
+    bool            m_suspend;
     uint64          m_count;
     uint64          m_limit;
     svector<uint64> m_limits;
     ptr_vector<reslimit> m_children;
 
     void set_cancel(unsigned f);
+    friend class scoped_suspend_rlimit;
 
 public:
     reslimit();
@@ -42,7 +44,7 @@ public:
     uint64 count() const;
 
 
-    bool get_cancel_flag() const { return m_cancel > 0; }
+    bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; }
     char const* get_cancel_msg() const;
     void cancel();
     void reset_cancel();
@@ -61,6 +63,17 @@ public:
 
 };
 
+class scoped_suspend_rlimit {
+    reslimit & m_limit;
+public:
+    scoped_suspend_rlimit(reslimit& r): m_limit(r) {
+        r.m_suspend = true;
+    }
+    ~scoped_suspend_rlimit() {
+        m_limit.m_suspend = false;
+    }
+};
+
 struct scoped_limits {
     reslimit&  m_limit;
     unsigned   m_sz;