mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

FPA API bugfixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-07-31 17:56:18 +01:00
parent c508b66cf7
commit 2cd4edf1a2
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/float_decl_plugin.h
View file

@ -221,7 +221,7 @@ public:
app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
bool is_value(expr * n) { return m_plugin->is_value(n); }
bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }
bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }
bool is_rm_value(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_value(n, v); }
app * mk_pzero(unsigned ebits, unsigned sbits);

4
src/smt/theory_fpa.cpp
View file

@ -122,7 +122,7 @@ namespace smt {
m_rw(term, t);
if (m_converter.is_rm_sort(term_sort)) {
if (m_converter.is_rm(term_sort)) {
SASSERT(is_app(t));
expr_ref bv_rm(m);
proof_ref bv_pr(m);
@ -183,7 +183,7 @@ namespace smt {
m_rw(owner, converted);
m_trans_map.insert(owner, converted, 0);
if (m_converter.is_rm_sort(m.get_sort(owner))) {
if (m_converter.is_rm(m.get_sort(owner))) {
mk_eq_bv_const(converted);
}
else {