mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-07-28 19:38:53 +01:00
parent b423418810 24961dc5f1
commit e10f256100
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/ast_smt_pp.cpp
View file

@ -569,8 +569,8 @@ class smt_printer {
m_out << ")"; m_out << ")";
} }
if (m_is_smt2 && q->get_num_patterns() > 0) { if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
m_out << "(!"; m_out << "(! ";
} }
{ {
smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_is_smt2, m_simplify_implies, m_indent, m_num_var_names, m_var_names); smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_is_smt2, m_simplify_implies, m_indent, m_num_var_names, m_var_names);
@ -609,7 +609,11 @@ class smt_printer {
m_out << "}"; m_out << "}";
} }
} }
if (m_is_smt2 && q->get_num_patterns() > 0) {
if (q->get_qid() != symbol::null)
m_out << " :qid " << q->get_qid();
if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
m_out << ")"; m_out << ")";
} }
m_out << ")"; m_out << ")";