diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 6b7ebd1ee..2501222b8 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(expr_ref& e) : m_es(e.m()) { m_es.push_back(e); } +subterms::subterms(const expr_ref& 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 9da46d947..29d11a6e7 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(expr_ref& e); + subterms(const expr_ref& e); iterator begin(); iterator end(); };