Add support for weights on soft assumes.

2 files changed, 3 insertions, 3 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 6df44c2f..06554fcb 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -281,7 +281,7 @@ namespace Microsoft.Boogie.SMTLib
           Linearise(node[1], options);
           return true;
         }
-        if (node.Op.Equals(VCExpressionGenerator.SoftOp))
+        if (node.Op is VCExprSoftOp)
         {
           Linearise(node[1], options);
           return true;
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 72540c9c..d911ce58 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -210,10 +210,10 @@ void ObjectInvariant()
 
       if (node.Op is VCExprStoreOp) RegisterStore(node);
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);
-      else if (node.Op.Equals(VCExpressionGenerator.SoftOp)) {
+      else if (node.Op is VCExprSoftOp) {
         var exprVar = node[0] as VCExprVar;
         AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
-        AddDeclaration(string.Format("(assert-soft {0} :weight 1)", exprVar.Name));
+        AddDeclaration(string.Format("(assert-soft {0} :weight {1})", exprVar.Name, ((VCExprSoftOp)node.Op).Weight));
       } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) {
         var exprVar = node[0] as VCExprVar;
         AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));