From 0324757fb1a12d76861a51be988690bf8de75f64 Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Wed, 14 Oct 2015 12:57:50 -0600
Subject: Modified translation so that z3 runs with type checking for simple
 binary operations

---
 Source/Core/AbsyExpr.cs | 1 -
 1 file changed, 1 deletion(-)

(limited to 'Source/Core')

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index cf6fb922..ad537288 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1642,7 +1642,6 @@ namespace Microsoft.Boogie {
           case Opcode.Div:
           case Opcode.Mod:
           case Opcode.RealDiv:
-          case Opcode.FloatDiv:
           case Opcode.Pow:
           case Opcode.Neq:  // Neq is allowed, but not Eq
           case Opcode.Subtype:
-- 
cgit v1.2.3