From 05f0deb046094f269ae56b1ca5cd05ea449c4e21 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Thu, 9 Apr 2020 16:06:59 -0600
Subject: [PATCH] Fixed the implementation of the `fdiml` function

The type of variable `val` should be `long double`.

Fixes #558
---
 share/smack/lib/math.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/share/smack/lib/math.c b/share/smack/lib/math.c
index 248cf3da7..303a06567 100644
--- a/share/smack/lib/math.c
+++ b/share/smack/lib/math.c
@@ -354,7 +354,7 @@ long double fdiml(long double x, long double y) {
   if (__isnanl(x) || __isnanl(y)) {
     return nanl(0);
   }
-  double val = __VERIFIER_nondet_long_double();
+  long double val = __VERIFIER_nondet_long_double();
   __SMACK_code("@ := $fsub.bvlongdouble($rmode, @, @);", val, x, y);
   return fmaxl(0.0l, val);
 }