From c5432dbd88515d4668ad050b089911ac80742d6d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Jan 2021 09:12:09 -0800 Subject: [PATCH] merge Signed-off-by: Nikolaj Bjorner --- src/ast/for_each_expr.cpp | 2 +- src/ast/for_each_expr.h | 2 +- src/ast/static_features.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 2501222b8..75d62161a 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -65,7 +65,7 @@ bool has_skolem_functions(expr * n) { } subterms::subterms(expr_ref_vector const& es): m_es(es) {} -subterms::subterms(const expr_ref& e) : m_es(e.m()) { m_es.push_back(e); } +subterms::subterms(expr_ref const& e) : m_es(e.m()) { m_es.push_back(e); } subterms::iterator subterms::begin() { return iterator(*this, true); } subterms::iterator subterms::end() { return iterator(*this, false); } subterms::iterator::iterator(subterms& f, bool start): m_es(f.m_es) { diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h index 29d11a6e7..5c4f95403 100644 --- a/src/ast/for_each_expr.h +++ b/src/ast/for_each_expr.h @@ -182,7 +182,7 @@ public: bool operator!=(iterator const& other) const; }; subterms(expr_ref_vector const& es); - subterms(const expr_ref& e); + subterms(expr_ref const& e); iterator begin(); iterator end(); }; diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index dd363eb33..c0897d33e 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -405,7 +405,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite return; } if (stack_depth > m_max_stack_depth) { - for (expr* arg : subterms(expr_ref(e, m))) + for (expr* arg : subterms(expr_ref(e, m))) if (get_depth(arg) <= 3 || is_quantifier(arg)) process(arg, form_ctx, or_and_ctx, ite_ctx, stack_depth-10); return;