Initial round of testing works with new syntax. Fixed an error where floating points could not be given as a function argument

1 files changed, 25 insertions, 13 deletions

diff --git a/float_test4.bpl b/float_test4.bpl
index a7aa8c4b..a31aa215 100644
--- a/float_test4.bpl
+++ b/float_test4.bpl
@@ -1,20 +1,32 @@
 //Translation from drift_tenth.c
-//Should Verify
-//FAILS; note that it succeeds when tick == fp(.1)
+//Should Fail
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
 
 procedure main() returns () {
-	var tick : float;
-	var time : float;
+	var tick : float32;
+	var time : float32;
 	var i: int;
 	
-	tick := fp(1)/fp(10);
-	time := fp(0);
+	tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
+	time := TO_FLOAT32_INT(0);
 	
-	i := 0;
-	while (i < 10)
-	{
-		time := time + tick;
-		i := i + 1;
-	}
-	assert(time == fp(1));
+	//i := 0;
+	//while (i < 10)
+	//{
+	//	time := time + tick;
+	//	i := i + 1;
+	//}
+	time := time + tick;//1
+	time := time + tick;//2
+	time := time + tick;//3
+	time := time + tick;//4
+	time := time + tick;//5
+	time := time + tick;//6
+	time := time + tick;//7
+	time := time + tick;//8
+	time := time + tick;//9
+	time := time + tick;//10
+	assert time == TO_FLOAT32_INT(1);
 }
\ No newline at end of file