From 95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 5 Dec 2011 23:07:06 -0800
Subject: Boogie: Added new abstract interpretation harness, which uses native
 Boogie Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain
 (/infer:t), which just detects assume/assert false. Boogie: Added new
 Interval Domain (/infer:j), which is stronger than the /infer:i intervals
 (because the also include preconditions, booleans, and more constraints) and
 may also be more efficient than previous intervals Boogie: Mark all inferred
 conditions with attribute {:inferred}

---
 Source/Basetypes/BigNum.cs | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Source/Basetypes')

diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs
index 73840482..ff676bc6 100644
--- a/Source/Basetypes/BigNum.cs
+++ b/Source/Basetypes/BigNum.cs
@@ -75,6 +75,12 @@ namespace Microsoft.Basetypes {
       }
     }
 
+    public BIM ToBigInteger {
+      get {
+        return val;
+      }
+    }
+
     // Convert to int; assert that no overflows occur
     public int ToIntSafe {
       get {
-- 
cgit v1.2.3