Merge pull request #560 from smackers/fix-fdiml

Fix the implementation of the `fdiml` function
smackers · Apr 10, 2020 · d05932b · d05932b
2 parents 32f5f91 + 05f0deb
commit d05932b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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);
 }