Compile assign-such-that for all integers, not just ones where a bound is found

1 files changed, 9 insertions, 0 deletions

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) {