Added .Trunc field to real-based types

Changed semantics of real-to-int conversions--these now have a precondition that the number converted is already an integer

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/dafny0/RealCompare.dfy b/Test/dafny0/RealCompare.dfy
index b1dae47d..f5256d6f 100644
--- a/Test/dafny0/RealCompare.dfy
+++ b/Test/dafny0/RealCompare.dfy
@@ -145,7 +145,7 @@ method Test_AbsInt1()
 {

   var a, i := 0.3, 0.0;

   while i < 10.0

-    invariant i <= 10.0 && i == real(int(i));

+    invariant i <= 10.0 && i == real(i.Trunc);

     invariant a == 0.3 + 0.5 * i;

   {

     a, i := a + 0.5, i + 1.0;