From 84b92046163239331fc6f20ac2951ff67a640ee1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 5 Apr 2023 16:39:10 -0700
Subject: [PATCH] inherit and reset rlimit counter on children limits

addresses rlimit leak reported by @mtzguido
---
 src/ast/ast.cpp                         | 8 ++++++++
 src/ast/ast.h                           | 2 ++
 src/ast/rewriter/seq_eq_solver.cpp      | 4 ++--
 src/ast/special_relations_decl_plugin.h | 6 ++++++
 src/util/rlimit.cpp                     | 2 ++
 5 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 0a34d3e12d8..7f9542fe48a 100644
--- 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
index 3e2f0288dfa..e0ae7b92f21 100644
--- 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
index 6d8734bc936..c6778c45e36 100644
--- 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
index 75b5cb134d2..0c437786421 100644
--- 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
index f71d2764a7c..ecc527681a1 100644
--- 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();    
 }