From 8aee7129f69c8852ff1bf70dc29217d874292800 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Jun 2016 21:48:49 -0700 Subject: [PATCH] shortcircuit stats functions on ground terms Signed-off-by: Nikolaj Bjorner --- src/smt/mam.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index ead1ea963..f5b3f34f7 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -879,6 +879,9 @@ namespace smt { */ void get_stats_core(app * n, unsigned & sz, unsigned & num_unbound_vars) { sz++; + if (n->is_ground()) { + return; + } unsigned num_args = n->get_num_args(); for (unsigned i = 0; i < num_args; i++) { expr * arg = n->get_arg(i); @@ -901,7 +904,7 @@ namespace smt { void get_stats(app * n, unsigned & sz, unsigned & num_unbound_vars) { sz = 0; num_unbound_vars = 0; - return get_stats_core(n, sz, num_unbound_vars); + get_stats_core(n, sz, num_unbound_vars); } /** @@ -1032,6 +1035,9 @@ namespace smt { */ unsigned get_num_bound_vars_core(app * n, bool & has_unbound_vars) { unsigned r = 0; + if (n->is_ground()) { + return 0; + } unsigned num_args = n->get_num_args(); for (unsigned i = 0; i < num_args; i++) { expr * arg = n->get_arg(i);