2 files changed, 15 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/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 0a9ba6b3..2c77a252 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -341,6 +341,10 @@ namespace Microsoft.Boogie {
 
     public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);
 
+    public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool);
+    public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool);
+    public static readonly VCExprOp NamedAssumeOp = new VCExprCustomOp("named_assume##dummy", 2, Type.Bool);
+
     public VCExprOp BoogieFunctionOp(Function func) {
       Contract.Requires(func != null);
       Contract.Ensures(Contract.Result<VCExprOp>() != null);
@@ -1565,6 +1569,16 @@ namespace Microsoft.Boogie.VCExprAST {
     }
   }
 
+  public class VCExprSoftOp : VCExprCustomOp
+  {
+    public readonly int Weight;
+
+    public VCExprSoftOp(int weight) : base("soft##dummy", 2, Microsoft.Boogie.Type.Bool)
+    {
+      Weight = weight;
+    }
+  }
+
   public class VCExprCustomOp : VCExprOp {
     public readonly string/*!*/ Name;
     int arity;