Bug fix in determining whether a type parameter is bounded

When checking whether a type parameter could be determined from the
bound variable types, we mistakenly compare equality between a
TypeVarable and a VCExprVar, instead of between two VCExprVars.

3 files changed, 17 insertions, 1 deletions

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 6077f327..dc9ad10f 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -1115,7 +1115,7 @@ namespace Microsoft.Boogie.TypeErasure
       if (typeVarBindings.Count < node.TypeParameters.Count) {
         foreach (TypeVariable/*!*/ var in node.TypeParameters) {
           Contract.Assert(var != null);
-          if (typeVarBindings.All(b => !b.V.Equals(var)))
+          if (typeVarBindings.All(b => !b.V.Equals(bindings.TypeVariableBindings[var])))
             newBoundVars.Add((VCExprVar)bindings.TypeVariableBindings[var]);
         }
       }
diff --git a/Test/test2/BoundedTypeParameterQuantifier.bpl b/Test/test2/BoundedTypeParameterQuantifier.bpl
new file mode 100644
index 00000000..146ba445
--- /dev/null
+++ b/Test/test2/BoundedTypeParameterQuantifier.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie /proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function Map#Domain<QUN, YAN>(Map QUN YAN): [QUN] bool;
+function Map#Empty<QUN, YAN>(): Map QUN YAN;
+type Map QUN YAN;
+
+axiom (forall<QUN, YAN> u: QUN ::
+        { Map#Domain(Map#Empty(): Map QUN YAN)[u] }
+        !Map#Domain(Map#Empty(): Map QUN YAN)[u]);
+
+procedure P()
+{
+}
diff --git a/Test/test2/BoundedTypeParameterQuantifier.bpl.expect b/Test/test2/BoundedTypeParameterQuantifier.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/test2/BoundedTypeParameterQuantifier.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors