diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 470573714..3e2faf7be 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2336,10 +2336,9 @@ namespace smt2 { func_decl_ref_vector decls(m()); vector bindings; vector > ids; - expr_ref_vector bodies(m()); parse_rec_fun_decls(decls, bindings, ids); - for (unsigned i = 0; i < decls.size(); ++i) { - m_ctx.insert(decls[i].get()); + for (func_decl* d : decls) { + m_ctx.insert(d); } parse_rec_fun_bodies(decls, bindings, ids);