From f7a6f3fa28a3f0cc0b600546205821c8c9c8a913 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Nov 2019 22:40:33 -0800 Subject: [PATCH] fix #2718 Signed-off-by: Nikolaj Bjorner --- src/ast/fpa_decl_plugin.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index daf197806..7b8cde038 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -205,7 +205,9 @@ sort * fpa_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) { m_manager->raise_exception("minimum number of significand bits is 1"); if (ebits < 2) m_manager->raise_exception("minimum number of exponent bits is 2"); - + if (ebits > 63) + m_manager->raise_exception("maximum number of exponent bits is 63"); + parameter p1(ebits), p2(sbits); parameter ps[2] = { p1, p2 }; sort_size sz;