Add support for weights on soft assumes.

1 files changed, 10 insertions, 1 deletions

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index a58cfb7f..2c77a252 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -344,7 +344,6 @@ namespace Microsoft.Boogie {
     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 static readonly VCExprOp SoftOp = new VCExprCustomOp("soft##dummy", 2, Type.Bool);
 
     public VCExprOp BoogieFunctionOp(Function func) {
       Contract.Requires(func != null);
@@ -1570,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;