mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix #7331

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-08-06 03:54:25 -07:00
parent 26b8d634a3
commit 3e518b9e8b
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/ast/ast_smt_pp.cpp
View file

@ -31,6 +31,7 @@ Revision History:
#include "ast/datatype_decl_plugin.h" #include "ast/datatype_decl_plugin.h"
#include "ast/seq_decl_plugin.h" #include "ast/seq_decl_plugin.h"
#include "ast/fpa_decl_plugin.h" #include "ast/fpa_decl_plugin.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/for_each_ast.h" #include "ast/for_each_ast.h"
#include "ast/decl_collector.h" #include "ast/decl_collector.h"
#include "math/polynomial/algebraic_numbers.h" #include "math/polynomial/algebraic_numbers.h"
@ -1000,6 +1001,18 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
} }
} }
vector<std::pair<func_decl*, expr*>> recfuns;
recfun::util u(m);
for (auto f : decls.get_rec_decls())
recfuns.push_back({f, u.get_def(f).get_rhs()});
if (!recfuns.empty()) {
smt2_pp_environment_dbg env(m);
ast_smt2_pp_recdefs(strm, recfuns, env);
}
#endif #endif
for (expr* a : m_assumptions) { for (expr* a : m_assumptions) {