diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 15 |
1 files changed, 12 insertions, 3 deletions
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;
|