From bd974799fccbe702137c70c50423f1482946aab6 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Sat, 20 Apr 2019 17:41:03 +0200 Subject: [PATCH] adding #qvars to [mk-quant] log line --- src/ast/ast.cpp | 2 +- src/ast/datatype_decl_plugin.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 68d24d0a9..e358c5fe1 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2443,7 +2443,7 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector &args) { static void trace_quant(std::ostream& strm, quantifier* q) { strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]") - << " #" << q->get_id() << " " << q->get_qid(); + << " #" << q->get_id() << " " << q->get_qid() << " " << q->get_num_decls(); for (unsigned i = 0; i < q->get_num_patterns(); ++i) { strm << " #" << q->get_pattern(i)->get_id(); } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index e3a1c9ed6..4bc9b5170 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -494,8 +494,8 @@ namespace datatype { out << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i << " " << family_name << "#" << m_id_counter - 1 << "\n"; ++m_id_counter; - out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 - << " " << family_name << "#" << m_id_counter - 1 << "\n"; + out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << num_args << " " << family_name + << "#" << constructor_id + 1 << " " << family_name << "#" << m_id_counter - 1 << "\n"; out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; ++m_id_counter; ++i;