From 9ae6866cad0c6af00010940013e1ed272c649e77 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 6 Jan 2014 23:11:49 -0800
Subject: Compile assign-such-that for all integers, not just ones where a
 bound is found

---
 Binaries/DafnyRuntime.cs | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'Binaries/DafnyRuntime.cs')

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index a8faafae..f61163d0 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -581,6 +581,15 @@ namespace Dafny
         yield return true;
       }
     }
+    public static IEnumerable<BigInteger> AllIntegers {
+      get {
+        yield return new BigInteger(0);
+        for (var j = new BigInteger(1);; j++) {
+          yield return j;
+          yield return -j;
+        }
+      }
+    }
     // pre: b != 0
     // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
     public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
-- 
cgit v1.2.3