From abe73db7028faa08dfcecc50be813344d94d58b5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 25 Apr 2015 15:19:48 +0100 Subject: [PATCH] FP: bugfix for get_some_value which couldn't produce rounding-mode values. --- src/ast/fpa_decl_plugin.cpp | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 48b7adb8b..e559ee179 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -879,12 +879,20 @@ void fpa_decl_plugin::get_sort_names(svector & sort_names, symbol } expr * fpa_decl_plugin::get_some_value(sort * s) { - SASSERT(s->is_sort_of(m_family_id, FLOATING_POINT_SORT)); - mpf tmp; - m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp); - expr * res = this->mk_numeral(tmp); - m_fm.del(tmp); - return res; + if (s->is_sort_of(m_family_id, FLOATING_POINT_SORT)) { + mpf tmp; + m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp); + expr * res = mk_numeral(tmp); + m_fm.del(tmp); + return res; + } + else if (s->is_sort_of(m_family_id, ROUNDING_MODE_SORT)) { + func_decl * f = mk_rm_const_decl(OP_FPA_RM_TOWARD_ZERO, 0, 0, 0, 0, s); + return m_manager->mk_const(f); + } + + UNREACHABLE(); + return 0; } bool fpa_decl_plugin::is_value(app * e) const {