From 3bfae100a8b18420a26ae460853cc170fd7952f1 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Fri, 8 Jul 2011 14:18:37 -0700
Subject: Dafny: Dafny now uses the Euclidean definition of division. (Verifier
 and runtime.)

---
 Source/Dafny/Compiler.cs | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 920105a9..d61d653d 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1375,10 +1375,19 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.Mul:
             opString = "*";  break;
           case BinaryExpr.ResolvedOpcode.Div:
-            opString = "/";  break;
+            wr.Write("Dafny.Helpers.EuclideanDivision(");
+            TrParenExpr(e.E0);
+            wr.Write(", ");
+            TrExpr(e.E1);
+            wr.Write(")");
+            break;
           case BinaryExpr.ResolvedOpcode.Mod:
-            opString = "%";  break;
-
+            wr.Write("Dafny.Helpers.EuclideanModulus(");
+            TrParenExpr(e.E0);
+            wr.Write(", ");
+            TrExpr(e.E1);
+            wr.Write(")");
+            break;
           case BinaryExpr.ResolvedOpcode.SetEq:
           case BinaryExpr.ResolvedOpcode.SeqEq:
             callString = "Equals";  break;
-- 
cgit v1.2.3