inherit and reset rlimit counter on children limits

addresses rlimit leak reported by @mtzguido
Z3Prover · Apr 5, 2023 · 84b9204 · 84b9204
1 parent f8242c5
commit 84b9204
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 2 deletions.
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
@@ -2322,6 +2322,14 @@ func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const
     return d;
 }
 
+bool ast_manager::is_parametric_function(func_decl* f, func_decl *& g) const {
+    // is-as-array
+    // is-map
+    // is-transitive-closure
+    return false;
+}
+
+
 sort * ast_manager::mk_fresh_sort(char const * prefix) {
     string_buffer<32> buffer;
     buffer << prefix << "!" << m_fresh_id;

diff --git a/src/ast/ast.h b/src/ast/ast.h
@@ -1924,6 +1924,8 @@ class ast_manager {
         return mk_fresh_func_decl(symbol(prefix), symbol::null, arity, domain, range, skolem);
     }
 
+    bool is_parametric_function(func_decl* f, func_decl *& g) const;
+
     app * mk_fresh_const(char const * prefix, sort * s, bool skolem = true) { 
         return mk_const(mk_fresh_func_decl(prefix, 0, nullptr, s, skolem)); 
     }

diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp
@@ -190,8 +190,8 @@ namespace seq {
             expr_ref digit = m_ax.sk().mk_digit2int(u);
             add_consequence(m_ax.mk_ge(digit, 1));
         }
-	    expr_ref y(seq.str.mk_concat(es, es[0]->get_sort()), m);
-	    ctx.add_solution(seq.str.mk_itos(n), y);
+        expr_ref y(seq.str.mk_concat(es, es[0]->get_sort()), m);
+        ctx.add_solution(seq.str.mk_itos(n), y);
         return true;
     }
 

diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h
@@ -101,6 +101,12 @@ class special_relations_util {
     bool is_to(expr const * e) const { return is_app_of(e, fid(), OP_SPECIAL_RELATION_TO); }
     bool is_tc(expr const * e) const { return is_app_of(e, fid(), OP_SPECIAL_RELATION_TC); }
 
+    bool is_lo(func_decl const * e) const { return is_decl_of(e, fid(), OP_SPECIAL_RELATION_LO); }
+    bool is_po(func_decl const * e) const { return is_decl_of(e, fid(), OP_SPECIAL_RELATION_PO); }
+    bool is_plo(func_decl const * e) const { return is_decl_of(e, fid(), OP_SPECIAL_RELATION_PLO); }
+    bool is_to(func_decl const * e) const { return is_decl_of(e, fid(), OP_SPECIAL_RELATION_TO); }
+    bool is_tc(func_decl const * e) const { return is_decl_of(e, fid(), OP_SPECIAL_RELATION_TC); }
+
     app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( fid(), OP_SPECIAL_RELATION_LO,  arg1, arg2); }
     app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( fid(), OP_SPECIAL_RELATION_PO,  arg1, arg2); }
     app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( fid(), OP_SPECIAL_RELATION_PLO, arg1, arg2); }

diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
@@ -87,6 +87,8 @@ void reslimit::push_child(reslimit* r) {
 
 void reslimit::pop_child() {
     lock_guard lock(*g_rlimit_mux);
+    m_count += m_children.back()->m_count;
+    m_children.back()->m_count = 0;
     m_children.pop_back();    
 }