summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Core/AbsyExpr.cs7
1 files changed, 7 insertions, 0 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 95a11a65..f648cec1 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -209,6 +209,13 @@ namespace Microsoft.Boogie {
return Unary(Token.NoToken, UnaryOperator.Opcode.Not, e1);
}
+
+ public static Expr Neg(Expr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Unary(Token.NoToken, UnaryOperator.Opcode.Neg, e1);
+ }
+
public static NAryExpr Imp(Expr e1, Expr e2) {
Contract.Requires(e2 != null);
Contract.Requires(e1 != null);