From b9bc6975e99ea9b06ca1ee19ed522409cf4076ae Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sat, 16 Nov 2019 16:24:24 +0000
Subject: [PATCH] fix crash in BV internalizer due to unknown bv_neg symbol

---
 src/ast/rewriter/fpa_rewriter.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index d978779aa..f2699915a 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -773,7 +773,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
         if (m_fm.is_nan(v)) {
             if (m_hi_fp_unspecified) {
                 expr * args[4] = { bu.mk_numeral(0, 1),
-                                   bu.mk_bv_neg(bu.mk_numeral(1, x.get_ebits())),
+                                   bu.mk_numeral(rational::minus_one(), x.get_ebits()),
                                    bu.mk_numeral(0, x.get_sbits() - 2),
                                    bu.mk_numeral(1, 1) };
                 result = bu.mk_concat(4, args);