From 0ebea1c298ab38165b60b1744e7e700796601b31 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Oct 2024 11:58:16 -0700 Subject: [PATCH] remove debug out Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 ++ src/cmd_context/pdecl.cpp | 1 - 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5c2a35995..43571167d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1073,6 +1073,8 @@ class ExprRef(AstRef): _z3_assert(is_app(self), "Z3 application expected") return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx) + + def num_args(self): """Return the number of arguments of a Z3 application. diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index de977edd7..4dfb0f8bb 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -773,7 +773,6 @@ bool pdatatypes_decl::commit(pdecl_manager& m) { for (unsigned i = 0; i < d->get_num_params(); ++i) { ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr)); } - verbose_stream() << ps.size() << " " << ps << "\n"; dts.m_buffer.push_back(d->instantiate_decl(m, ps.size(), ps.data())); }