mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

adding #qvars to [mk-quant] log line

Browse source
This commit is contained in:
nilsbecker 2019-04-20 17:41:03 +02:00
parent 1c24d340d1
commit bd974799fc
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -2443,7 +2443,7 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &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();
}

4
src/ast/datatype_decl_plugin.cpp
View file

@ -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;