From b79d1a6956a6a018280993fc103aea08330cc9bc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Feb 2018 09:22:20 +0900 Subject: [PATCH] fix #1488 for smtlib basic printer Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt_pp.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index ace0de2cc..b7404859f 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -952,6 +952,10 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { strm << "; " << m_attributes.c_str(); } +#if 0 + decls.display_decls(strm); +#else + decls.order_deps(); ast_mark sort_mark; for (unsigned i = 0; i < decls.get_num_sorts(); ++i) { sort* s = decls.get_sorts()[i]; @@ -978,18 +982,19 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { strm << "\n"; } } +#endif - for (unsigned i = 0; i < m_assumptions.size(); ++i) { + for (expr* a : m_assumptions) { smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); strm << "(assert\n "; - p(m_assumptions[i].get()); + p(a); strm << ")\n"; } - for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { + for (expr* a : m_assumptions_star) { smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1); strm << "(assert\n "; - p(m_assumptions_star[i].get()); + p(a); strm << ")\n"; }