removed an unnecessary type checking addition

3 files changed, 30 insertions, 31 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index b980a22b..d3e63922 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2277,7 +2277,6 @@ namespace Microsoft.Boogie {
     private readonly string name;
     private readonly Type type;
     private readonly Type argType;
-    private readonly Type argType2;
     private readonly int hashCode;
 
     public ArithmeticCoercion(IToken tok, CoercionType coercion) {
@@ -2357,9 +2356,9 @@ namespace Microsoft.Boogie {
 
       tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
 
-      if (!(cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType) || cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType2)))
+      if (!cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType))
       {
-        tc.Error(this.tok, "argument type {0} does not match expected type {1} or type {2}", cce.NonNull(args[0]).Type, this.argType, this.argType2);
+        tc.Error(this.tok, "argument type {0} does not match expected type {1}", cce.NonNull(args[0]).Type, this.argType);
       }
 
       return this.type;
diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl
index 34059f80..240c02f3 100644
--- a/Test/floats/float3.bpl
+++ b/Test/floats/float3.bpl
@@ -1,27 +1,27 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-procedure main() returns () {

-	var x : float32;

-	var y : float32;

-	var z : float32;

-	

-	z := x + y;

-	z := x - y;

-	z := x * y;

-	assume(y != fp<8, 24>(0bv32));

-	z := x / y;

-	

-	z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32);

-	assert(z == fp<8, 24>(2bv32));

-	

-	z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32);

-	assert(z == fp<8, 24>(1bv32));

-	

-	z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23);

-	assert(z == fp(false, 127bv8, 0bv23));

-	

-	z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32);

-	assert(z == fp(false, 127bv8, 0bv23));

-	

-	return;

+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+	var x : float32;
+	var y : float32;
+	var z : float32;
+	
+	z := x + y;
+	z := x - y;
+	z := x * y;
+	assume(y != fp<8, 24>(0bv32));
+	z := x / y;
+	
+	z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32);
+	assert(z == fp<8, 24>(2bv32));
+	
+	z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32);
+	assert(z == fp<8, 24>(1bv32));
+	
+	z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23);
+	assert(z == fp(false, 127bv8, 0bv23));
+	
+	z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32);
+	assert(z == fp(false, 127bv8, 0bv23));
+	
+	return;
 }
\ No newline at end of file
diff --git a/Test/test1/IntReal.bpl.expect b/Test/test1/IntReal.bpl.expect
index b532d22a..021a8389 100644
--- a/Test/test1/IntReal.bpl.expect
+++ b/Test/test1/IntReal.bpl.expect
@@ -12,8 +12,8 @@ IntReal.bpl(19,12): Error: invalid argument types (real and int) to binary opera
 IntReal.bpl(25,8): Error: invalid argument types (int and real) to binary operator **
 IntReal.bpl(29,14): Error: invalid argument types (real and int) to binary operator ==
 IntReal.bpl(31,13): Error: invalid argument types (int and real) to binary operator ==
-IntReal.bpl(34,6): Error: argument type int does not match expected type real or type float
-IntReal.bpl(35,6): Error: argument type real does not match expected type int or type float
+IntReal.bpl(34,6): Error: argument type int does not match expected type real
+IntReal.bpl(35,6): Error: argument type real does not match expected type int
 IntReal.bpl(47,8): Error: invalid argument types (real and int) to binary operator div
 IntReal.bpl(48,8): Error: invalid argument types (real and int) to binary operator mod
 18 type checking errors detected in IntReal.bpl