diff --git a/src/api/api_context.h b/src/api/api_context.h
index 882974005..3d5f0c2bf 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -117,6 +117,7 @@ namespace api {
         bool produce_unsat_cores() const { return m_params.m_unsat_core; }
         bool use_auto_config() const { return m_params.m_auto_config; }
         unsigned get_timeout() const { return m_params.m_timeout; }
+        unsigned get_rlimit() const { return m_params.m_rlimit; }
         arith_util & autil() { return m_arith_util; }
         bv_util & bvutil() { return m_bv_util; }
         datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 9ed82191b..c3fdeb94b 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -287,9 +287,11 @@ extern "C" {
         lbool r = l_undef;
         cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
         unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit  = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
         api::context::set_interruptable si(*(mk_c(c)), eh);        
         {
             scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
                 r = to_fixedpoint_ref(d)->ctx().query(to_expr(q));
             }
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 50b0c6e22..4daf3956f 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -254,6 +254,7 @@ extern "C" {
         }
         expr * const * _assumptions = to_exprs(assumptions);
         unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
         bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
         cancel_eh<solver> eh(*to_solver_ref(s));
         api::context::set_interruptable si(*(mk_c(c)), eh);
@@ -261,6 +262,7 @@ extern "C" {
         {
             scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
                 result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions);
             }
@@ -356,6 +358,7 @@ extern "C" {
         Z3_stats_ref * st = alloc(Z3_stats_ref);
         to_solver_ref(s)->collect_statistics(st->m_stats);
         get_memory_statistics(st->m_stats);
+        get_rlimit_statistics(mk_c(c)->m().limit(), st->m_stats);
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
         RETURN_Z3(r);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index c1ee603c7..deddd3cad 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -44,6 +44,7 @@ Revision History:
 #include"chashtable.h"
 #include"z3_exception.h"
 #include"dependency.h"
+#include"rlimit.h"
 
 #define RECYCLE_FREE_AST_INDICES
 
@@ -1424,6 +1425,7 @@ public:
     void show_id_gen();
 
 protected:
+    reslimit                  m_limit;
     small_object_allocator    m_alloc;
     family_manager            m_family_manager;
     expr_array_manager        m_expr_array_manager;
@@ -1519,6 +1521,8 @@ public:
             fid == m_user_sort_family_id; 
     }
 
+    reslimit& limit() { return m_limit; }
+
     void register_plugin(symbol const & s, decl_plugin * plugin);
     
     void register_plugin(family_id id, decl_plugin * plugin);
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index be3bfbd0a..505197f33 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -578,6 +578,8 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
     while (!frame_stack().empty()) {
         if (m_cancel)
             throw rewriter_exception(Z3_CANCELED_MSG);
+        if (!m().limit().inc()) 
+            throw rewriter_exception(Z3_CANCELED_MSG);
         SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
         frame & fr = frame_stack().back();
         expr * t   = fr.m_curr;
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 8fda13289..8648775ee 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1390,6 +1390,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     TRACE("before_check_sat", dump_assertions(tout););
     init_manager();
     unsigned timeout = m_params.m_timeout;
+    unsigned rlimit  = m_params.m_rlimit;
     scoped_watch sw(*this);
     lbool r;
 
@@ -1399,6 +1400,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         cancel_eh<opt_wrapper> eh(*get_opt());
         scoped_ctrl_c ctrlc(eh);
         scoped_timer timer(timeout, &eh);
+        scoped_rlimit _rlimit(m().limit(), rlimit);
         ptr_vector<expr> cnstr(m_assertions);
         cnstr.append(num_assumptions, assumptions);
         get_opt()->set_hard_constraints(cnstr);
@@ -1436,6 +1438,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         cancel_eh<solver> eh(*m_solver);
         scoped_ctrl_c ctrlc(eh);
         scoped_timer timer(timeout, &eh);
+        scoped_rlimit _rlimit(m().limit(), rlimit);
         try {
             r = m_solver->check_sat(num_assumptions, assumptions);
         }
@@ -1646,6 +1649,7 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
         st.update("total time", total_time);
     st.update("time", get_seconds());
     get_memory_statistics(st);
+    get_rlimit_statistics(m().limit(), st);
     if (m_check_sat_result) {
         m_check_sat_result->collect_statistics(st);
     }
diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index 5a9b1a4f3..add1b5b3d 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -35,6 +35,7 @@ context_params::context_params() {
     m_smtlib2_compliant = false;
     m_well_sorted_check = false;
     m_timeout = UINT_MAX;
+    m_rlimit  = UINT_MAX;
     updt_params();
 }
 
@@ -65,6 +66,10 @@ void context_params::set(char const * param, char const * value) {
         long val = strtol(value, 0, 10);
         m_timeout = static_cast<unsigned>(val);
     }
+    if (p == "rlimit") {
+        long val = strtol(value, 0, 10);
+        m_rlimit = static_cast<unsigned>(val);
+    }
     else if (p == "type_check" || p == "well_sorted_check") {
         set_bool(m_well_sorted_check, param, value);
     }
@@ -115,6 +120,7 @@ void context_params::updt_params() {
 
 void context_params::updt_params(params_ref const & p) {
     m_timeout           = p.get_uint("timeout", m_timeout);
+    m_rlimit            = p.get_uint("rlimit", m_rlimit);
     m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", m_well_sorted_check));
     m_auto_config       = p.get_bool("auto_config", m_auto_config);
     m_proof             = p.get_bool("proof", m_proof);
@@ -130,6 +136,7 @@ void context_params::updt_params(params_ref const & p) {
 
 void context_params::collect_param_descrs(param_descrs & d) {
     d.insert("timeout", CPK_UINT, "default timeout (in milliseconds) used for solvers", "4294967295");
+    d.insert("rlimit", CPK_UINT, "default resource limit used for solvers", "4294967295");
     d.insert("well_sorted_check", CPK_BOOL, "type checker", "false");
     d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
     d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h
index bdd77fb1c..2c75b5743 100644
--- a/src/cmd_context/context_params.h
+++ b/src/cmd_context/context_params.h
@@ -40,6 +40,7 @@ public:
     bool        m_unsat_core;
     bool        m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager.
     unsigned    m_timeout;
+    unsigned    m_rlimit;
 
     context_params();
     void set(char const * param, char const * value);
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 9d4c18262..ab2ad3922 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -158,6 +158,7 @@ public:
     void display_statistics(cmd_context & ctx, tactic * t) {
         statistics stats;
         get_memory_statistics(stats);
+        get_rlimit_statistics(ctx.m().limit(), stats);
         stats.update("time", ctx.get_seconds());
         t->collect_statistics(stats);
         stats.display_smt2(ctx.regular_stream());
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 60de96e1d..c2db15e3a 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -948,6 +948,7 @@ namespace datalog {
             m_engine->collect_statistics(st);
         }
         get_memory_statistics(st);
+        get_rlimit_statistics(m.limit(), st);
     }
 
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 0264ea70f..dda38e566 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1258,6 +1258,7 @@ namespace opt {
             it->m_value->collect_statistics(stats);
         }        
         get_memory_statistics(stats);
+        get_rlimit_statistics(m.limit(), stats);
     }
 
     void context::collect_param_descrs(param_descrs & r) {
diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp
index 179749dac..a194cdfd8 100644
--- a/src/sat/sat_bceq.cpp
+++ b/src/sat/sat_bceq.cpp
@@ -497,7 +497,7 @@ namespace sat {
         flet<unsigned> _bound_maxc(m_solver.m_config.m_max_conflicts, 1500);
 
         use_list     ul;        
-        solver       s(m_solver.m_params, 0);
+        solver       s(m_solver.m_params, m_solver.rlimit(), 0);
         s.m_config.m_bcd            = false;
         s.m_config.m_minimize_core  = false;
         s.m_config.m_optimize_model = false;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0ecda2808..008ba8a18 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -31,8 +31,9 @@ Revision History:
 
 namespace sat {
 
-    solver::solver(params_ref const & p, extension * ext):
+    solver::solver(params_ref const & p, reslimit& l, extension * ext):
         m_cancel(false),
+        m_rlimit(l),
         m_config(p),
         m_ext(ext),
         m_cleaner(*this),
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 97a27502d..23033d940 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -38,6 +38,7 @@ Revision History:
 #include"statistics.h"
 #include"stopwatch.h"
 #include"trace.h"
+#include"rlimit.h"
 
 namespace sat {
 
@@ -71,6 +72,7 @@ namespace sat {
         struct abort_solver {};
     protected:
         volatile bool           m_cancel;
+        reslimit&               m_rlimit;
         config                  m_config;
         stats                   m_stats;
         extension *             m_ext;
@@ -145,7 +147,7 @@ namespace sat {
         friend class bceq;
         friend struct mk_stat;
     public:
-        solver(params_ref const & p, extension * ext);
+        solver(params_ref const & p, reslimit& l, extension * ext);
         ~solver();
 
         // -----------------------
@@ -238,6 +240,7 @@ namespace sat {
         clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
         void checkpoint() {
             if (m_cancel) throw solver_exception(Z3_CANCELED_MSG);
+            if (!m_rlimit.inc()) { m_cancel = true; throw solver_exception(Z3_CANCELED_MSG); }
             ++m_num_checkpoints;
             if (m_num_checkpoints < 10) return;
             m_num_checkpoints = 0;
@@ -415,6 +418,7 @@ namespace sat {
         void user_push();
         void user_pop(unsigned num_scopes);
         void pop_to_base_level();
+        reslimit& rlimit() { return m_rlimit; }
         // -----------------------
         //
         // Simplification
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index a64be2075..fd1f4cfd0 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -63,7 +63,7 @@ class inc_sat_solver : public solver {
     typedef obj_map<expr, sat::literal> dep2asm_t;
 public:
     inc_sat_solver(ast_manager& m, params_ref const& p):
-        m(m), m_solver(p,0), 
+        m(m), m_solver(p, m.limit(), 0), 
         m_params(p), m_optimize_model(false), 
         m_fmls(m), 
         m_asmsf(m),
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index e4d5e6df5..f04100ca2 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -34,7 +34,7 @@ class sat_tactic : public tactic {
         
         imp(ast_manager & _m, params_ref const & p):
             m(_m),
-            m_solver(p, 0),
+            m_solver(p, m.limit(), 0),
             m_params(p) {
             SASSERT(!m.proofs_enabled());
         }
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index abaa2eace..54e78ac8f 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include<time.h>
 #include<signal.h>
 #include"timeout.h"
+#include"rlimit.h"
 #include"dimacs.h"
 #include"sat_solver.h"
 #include"gparams.h"
@@ -132,7 +133,8 @@ unsigned read_dimacs(char const * file_name) {
     signal(SIGINT, on_ctrl_c);
     params_ref p = gparams::get_module("sat");
     p.set_bool("produce_models", true);
-    sat::solver solver(p, 0);
+    reslimit limit;
+    sat::solver solver(p, limit, 0);
     g_solver = &solver;
 
     if (file_name) {
@@ -150,7 +152,7 @@ unsigned read_dimacs(char const * file_name) {
     
     lbool r;
     vector<sat::literal_vector> tracking_clauses;
-    sat::solver solver2(p, 0);
+    sat::solver solver2(p, limit, 0);
     if (p.get_bool("dimacs.core", false)) {
         g_solver = &solver2;        
         sat::literal_vector assumptions;
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 2ef9a0d54..c31b2fb6d 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -35,6 +35,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
     m_timeout = p.timeout();
+    m_rlimit  = p.rlimit();
     m_max_conflicts = p.max_conflicts();
     m_core_validate = p.core_validate();
     model_params mp(_p);
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index e67591d0e..2c1ac13c5 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -206,6 +206,7 @@ struct smt_params : public preprocessor_params,
     bool                m_user_theory_preprocess_axioms;
     bool                m_user_theory_persist_axioms;
     unsigned            m_timeout;
+    unsigned            m_rlimit;
     bool                m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
     bool                m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.    
     bool                m_dump_goal_as_smt;
@@ -275,6 +276,7 @@ struct smt_params : public preprocessor_params,
         m_user_theory_preprocess_axioms(false),
         m_user_theory_persist_axioms(false),
         m_timeout(0),
+        m_rlimit(0),
         m_at_labels_cex(false),
         m_check_at_labels(false),
         m_dump_goal_as_smt(false),
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index fa73f9725..e84f3654c 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -16,6 +16,7 @@ def_module_params(module_name='smt',
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
                           ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
                           ('timeout', UINT, 0, 'timeout (0 means no timeout)'),
+	                  ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
                           ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index b0abc0de0..e19ee34dd 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -199,7 +199,7 @@ namespace smt {
     bool context::bcp() {
         SASSERT(!inconsistent());
         while (m_qhead < m_assigned_literals.size()) {
-            if (m_cancel_flag) {
+            if (get_cancel_flag()) {
                 return true;
             }
             literal l      = m_assigned_literals[m_qhead];
@@ -1616,7 +1616,7 @@ namespace smt {
             unsigned qhead = m_qhead;
             if (!bcp())
                 return false;
-            if (m_cancel_flag) 
+            if (get_cancel_flag()) 
                 return true;
             SASSERT(!inconsistent());
             propagate_relevancy(qhead);
@@ -2773,7 +2773,7 @@ namespace smt {
     }
 
     void context::assert_expr_core(expr * e, proof * pr) {
-        if (m_cancel_flag) return;
+        if (get_cancel_flag()) return;
         SASSERT(is_well_sorted(m_manager, e));
         TRACE("begin_assert_expr", tout << mk_pp(e, m_manager) << "\n";);
         TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m_manager) << "\n";);
@@ -2803,7 +2803,7 @@ namespace smt {
     }
 
     void context::internalize_assertions() {
-        if (m_cancel_flag) return;
+        if (get_cancel_flag()) return;
         TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
         timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
         reduce_assertions();
@@ -3311,6 +3311,9 @@ namespace smt {
                 if (!inconsistent()) {
                     if (resource_limits_exceeded())
                         return l_undef;
+
+                    if (!m_manager.limit().inc())
+                        return l_undef;
                     
                     if (m_num_conflicts_since_restart > m_restart_threshold && m_scope_lvl - m_base_lvl > 2) {
                         TRACE("search_bug", tout << "bounded-search return undef, inconsistent: " << inconsistent() << "\n";);
@@ -3337,9 +3340,11 @@ namespace smt {
                 return l_undef;
             }
 
+            if (!m_manager.limit().inc())
+                return l_undef;
+
             if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses)
                 simplify_clauses();
-
             
             if (!decide()) {
                 final_check_status fcs = final_check();
@@ -3381,7 +3386,7 @@ namespace smt {
             }
         }
             
-        if (m_cancel_flag) {
+        if (get_cancel_flag()) {
             m_last_search_failure = CANCELED;
             return true;
         }
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 231b73fe3..fc7f076f1 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -235,7 +235,7 @@ namespace smt {
 
         virtual void set_cancel_flag(bool f = true);
 
-        bool get_cancel_flag() { return m_cancel_flag; }
+        bool get_cancel_flag() { return m_cancel_flag || !m_manager.limit().inc(); }
 
         region & get_region() {
             return m_region;
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
new file mode 100644
index 000000000..338bd5582
--- /dev/null
+++ b/src/util/rlimit.cpp
@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    rlimit.cpp
+
+Abstract:
+
+    Resource limit container.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-09-28
+
+Revision History:
+
+--*/
+#include "rlimit.h"
+
+reslimit::reslimit():
+    m_count(0),
+    m_limit(UINT_MAX) {
+}
+
+unsigned reslimit::count() const {
+    return m_count;
+}
+
+bool reslimit::inc() {
+    ++m_count;
+    return m_count <= m_limit;
+}
+
+bool reslimit::inc(unsigned offset) {
+    m_count += offset;
+    return m_count <= m_limit;
+}
+
+void reslimit::push(unsigned delta_limit) {
+    unsigned new_limit = UINT_MAX;
+    if (delta_limit > 0 && delta_limit + m_count > m_count) {
+        new_limit = delta_limit + m_count;
+    }
+    m_limits.push_back(m_limit);
+    m_limit = std::min(new_limit, m_limit);
+}
+
+void reslimit::pop() {
+    if (m_count > m_limit) {
+        m_count = m_limit;
+    }
+    m_limit = m_limits.back();
+    m_limits.pop_back();
+}
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
new file mode 100644
index 000000000..36912de40
--- /dev/null
+++ b/src/util/rlimit.h
@@ -0,0 +1,47 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    rlimit.h
+
+Abstract:
+
+    Resource limit container.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-09-28
+
+Revision History:
+
+--*/
+#ifndef RLIMIT_H_
+#define RLIMIT_H_
+
+#include "vector.h"
+
+class reslimit {
+    unsigned        m_count;
+    unsigned        m_limit;
+    unsigned_vector m_limits;
+public:    
+    reslimit();
+    bool inc();
+    bool inc(unsigned offset);
+    void push(unsigned delta_limit);
+    void pop();
+    unsigned count() const; 
+};
+
+class scoped_rlimit {
+    reslimit& m_limit;
+public:
+    scoped_rlimit(reslimit& r, unsigned l): m_limit(r) {
+        r.push(l);
+    }
+    ~scoped_rlimit() { m_limit.pop(); }
+
+};
+
+#endif
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 6e50fd4a8..e1a0928fe 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -236,3 +236,7 @@ void get_memory_statistics(statistics& st) {
     st.update("memory",      static_cast<double>(mem)/100.0);
     st.update("num allocs",  static_cast<double>(memory::get_allocation_count()));
 }
+
+void get_rlimit_statistics(reslimit& l, statistics& st) {
+    st.update("rlimit-count",     l.count());
+}
diff --git a/src/util/statistics.h b/src/util/statistics.h
index 258ffbe29..041c2cf99 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -21,6 +21,7 @@ Notes:
 
 #include<iostream>
 #include"vector.h"
+#include"rlimit.h"
 
 class statistics {
     typedef std::pair<char const *, unsigned> key_val_pair;
@@ -43,5 +44,6 @@ public:
 };
 
 void get_memory_statistics(statistics& st);
+void get_rlimit_statistics(reslimit& l, statistics& st);
 
 #endif