diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index 1adca1648..f6b3a22e5 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -73,7 +73,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { } if (m_args.size() == n) { if (arg_differs) { - b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr()); + b = m.mk_app(c->get_decl(), m_args); m_refs.push_back(b); SASSERT(m.get_sort(a) == m.get_sort(b)); } else {