From 2cd4edf1a23a3978851c83338f01d0ea775dabb6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 31 Jul 2014 17:56:18 +0100 Subject: [PATCH] FPA API bugfixes Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.h | 2 +- src/smt/theory_fpa.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 4dedbc2e2..2b6b7fd64 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -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); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index f44447b8f..9c03cb76c 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -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 {