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 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-02-22 13:57:18 +01:00
parent 73060ecaec 699834261e
commit 72d59ea00a
1 changed files with 14 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast_smt_pp.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include "util/vector.h" #include "util/vector.h"
#include "util/smt2_util.h" #include "util/smt2_util.h"
#include "ast/ast_smt_pp.h" #include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/array_decl_plugin.h" #include "ast/array_decl_plugin.h"
@ -388,10 +389,7 @@ class smt_printer {
m_out << "(_ bv" << val << " " << bv_size << ")"; m_out << "(_ bv" << val << " " << bv_size << ")";
} }
else if (m_futil.is_numeral(n, float_val)) { else if (m_futil.is_numeral(n, float_val)) {
m_out << "((_ to_fp " << m_out << mk_ismt2_pp(n, m_manager);
float_val.get().get_ebits() << " " <<
float_val.get().get_sbits() << ") RTZ " <<
m_futil.fm().to_string(float_val).c_str() << ")";
} }
else if (m_bvutil.is_bit2bool(n)) { else if (m_bvutil.is_bit2bool(n)) {
unsigned bit = n->get_decl()->get_parameter(0).get_int(); unsigned bit = n->get_decl()->get_parameter(0).get_int();