Add isBvConst and asBvConst accessors to LiteralExpr to match the

others already present for bool, BigNum and BigDec.

1 files changed, 13 insertions, 0 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index d8cb623b..70b445b1 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -604,6 +604,19 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public bool isBvConst {

+      get {

+        return Val is BvConst;

+      }

+    }

+

+    public BvConst asBvConst {

+      get {

+        Contract.Assert(isBvConst);

+        return (BvConst)cce.NonNull(Val);

+      }

+    }

+

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);