From 2f60bcbfcbff5245d2780ab33e4b67468c7068f9 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 19 Aug 2019 14:43:16 +0100
Subject: [PATCH] Clean up NaN return values in Z3_get_numeral_double

---
 src/api/api_numeral.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index f718b1ee6..831b3503d 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -15,6 +15,7 @@ Author:
 Revision History:
 
 --*/
+#include<cmath>
 #include<iostream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
@@ -233,7 +234,7 @@ extern "C" {
         RESET_ERROR_CODE();
         if (!is_expr(a)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0.0/0.0;
+            return NAN;
         }
         expr* e = to_expr(a);
         fpa_util & fu = mk_c(c)->fpautil();
@@ -242,7 +243,7 @@ extern "C" {
             tmp.get().get_ebits() > 11 ||
             tmp.get().get_sbits() > 53) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0.0/0.0;
+            return NAN;
         }
         return fu.fm().to_double(tmp);
     }