From 30f47ed1880440966e2d433685c05c740dd822c9 Mon Sep 17 00:00:00 2001
From: kroening <kroening@6afb6bc1-c8e4-404c-8f48-9ae832c5b171>
Date: Sat, 9 May 2015 09:45:05 +0000
Subject: [PATCH] make this test work on Windows, another attempt

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5379 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
---
 regression/cbmc/Float-data-dependent-rounding/main.c | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/regression/cbmc/Float-data-dependent-rounding/main.c b/regression/cbmc/Float-data-dependent-rounding/main.c
index 873dc23006..c6a882c9ed 100644
--- a/regression/cbmc/Float-data-dependent-rounding/main.c
+++ b/regression/cbmc/Float-data-dependent-rounding/main.c
@@ -3,7 +3,7 @@
 
 #ifdef _MSC_VER
 #include <float.h>
-int isnanf(float);
+#define isnan(x) ((x)!=(x))
 #else
 #include <fenv.h>
 #endif
@@ -12,8 +12,8 @@ int main (void) {
   float f;
   float g;
 
-  __CPROVER_assume(!isnanf(f));
-  __CPROVER_assume(!isnanf(g));
+  __CPROVER_assume(!isnan(f));
+  __CPROVER_assume(!isnan(g));
 
   if (f > g) {
     #ifdef _MSC_VER