diff --git a/src/muz/spacer/spacer_term_graph.cpp b/src/muz/spacer/spacer_term_graph.cpp index 61f7fb369..7c2b64a50 100644 --- a/src/muz/spacer/spacer_term_graph.cpp +++ b/src/muz/spacer/spacer_term_graph.cpp @@ -292,7 +292,7 @@ app* term_graph::mk_app_core (app *a) { kids.push_back (mk_app(::to_app(a->get_arg(i)))); } - app* res = m.mk_app(a->get_decl(), kids.c_ptr()); + app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.c_ptr()); m_pinned.push_back(res); return res;