summaryrefslogtreecommitdiff
path: root/Source/VCExpr
diff options
context:
space:
mode:
authorGravatar Valentin Wüstholz <wuestholz@gmail.com>2016-03-03 17:32:31 -0600
committerGravatar Valentin Wüstholz <wuestholz@gmail.com>2016-03-03 17:32:31 -0600
commit502942a53a6db2b3a900d7570807216372d49ad0 (patch)
tree494530d18be4957b05379f3bc4b12d1f83e22e9e /Source/VCExpr
parent8e5a0356cc3122e780fe28300dbad5ade2c13197 (diff)
Improve support for optimization and identifying unnecessary assumes.
Diffstat (limited to 'Source/VCExpr')
-rw-r--r--Source/VCExpr/VCExprAST.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 2fbb102c..a58cfb7f 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -343,6 +343,8 @@ 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);