From 0c53c139da18d0804003cbb4b6a841692e50d724 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 15:37:58 -0700 Subject: [PATCH] add to_string method to make it easier to use without << --- src/api/c++/z3++.h | 1 + src/sat/smt/array_axioms.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 97413ae54..c11269b15 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -599,6 +599,7 @@ namespace z3 { iterator begin() const noexcept { return iterator(this, 0); } iterator end() const { return iterator(this, size()); } friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; } + std::string to_string() const { return std::string(Z3_ast_vector_to_string(ctx(), m_vector); } }; diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index ecb1bc470..c34b8ae17 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -451,6 +451,7 @@ namespace array { expr_ref alpha(a.mk_select(args), m); expr_ref beta(alpha); rewrite(beta); + TRACE("array", tout << alpha << " == " << beta << "\n";); return ctx.propagate(e_internalize(alpha), e_internalize(beta), array_axiom()); }