summaryrefslogtreecommitdiff
path: root/Source/Model/Model.cs
diff options
context:
space:
mode:
authorGravatar MichalMoskal <unknown>2010-12-14 23:31:04 +0000
committerGravatar MichalMoskal <unknown>2010-12-14 23:31:04 +0000
commitd16580f98fe091ff59336b978df4705e2a63bcda (patch)
tree93c6702b894f946adf127b5ea05958d20219d051 /Source/Model/Model.cs
parent53e487c93f0c0bbb26ea6cabad175507021a8f8a (diff)
Add information about field being volatile
Diffstat (limited to 'Source/Model/Model.cs')
-rw-r--r--Source/Model/Model.cs9
1 files changed, 9 insertions, 0 deletions
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index c7314ca4..7201aa99 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -208,6 +208,15 @@ namespace Microsoft.Boogie
return r != null && r.Value;
}
+ /// <summary>
+ /// Short for TryEval(args) == (Element)false
+ /// </summary>
+ public bool IsFalse(params Element[] args)
+ {
+ var r = TryEval(args) as Boolean;
+ return r != null && !r.Value;
+ }
+
public void AddApp(Element res, params Element[] args)
{
if (Arity == 0)