3 files changed, 7 insertions, 5 deletions
diff --git a/Test/jennisys0/Answer b/Test/jennisys0/Answer
index 609f2fe3..5a3f9e82 100644
--- a/Test/jennisys0/Answer
+++ b/Test/jennisys0/Answer
@@ -1,6 +1,6 @@
 
 -------------------- Prog0.jen --------------------
-Jennisys, Copyright (c) 2011, Microsoft.
+// Jennisys, Copyright (c) 2011, Microsoft.
 ---------- Given Jennisys program ----------
 class C {
   var a: seq[int]
@@ -48,7 +48,7 @@ code C {
 ----------
 
 -------------------- ExtensibleArray.jen --------------------
-Jennisys, Copyright (c) 2011, Microsoft.
+// Jennisys, Copyright (c) 2011, Microsoft.
 ---------- Given Jennisys program ----------
 class ExtensibleArray[T] {
   var Contents: seq[T]
@@ -83,7 +83,8 @@ model ExtensibleArray[T] {
     length <= M + 256
     more != null ==> M < length
     length = |Contents|
-    forall i :: 0 <= i && i < M ==> Contents[i] = more.Contents[i div 256][i mod 256]
+    more != null ==> (forall i :: 0 <= i && i < |more.Contents| ==> more.Contents[i] != null && more.Contents[i].Length = 256)
+    more != null ==> (forall i :: 0 <= i && i < M ==> Contents[i] = more.Contents[i div 256][i mod 256])
     forall i :: M <= i && i < length ==> Contents[i] = elements[i - M]
 }
 ----------
diff --git a/Test/jennisys0/ExtensibleArray.jen b/Test/jennisys0/ExtensibleArray.jen
index e6141ab7..7ef36ce2 100644
--- a/Test/jennisys0/ExtensibleArray.jen
+++ b/Test/jennisys0/ExtensibleArray.jen
@@ -34,6 +34,7 @@ model ExtensibleArray[T] {
     more != null ==> M < length
 
     length = |Contents|
-    forall i :: 0 <= i && i < M ==> Contents[i] = more.Contents[i div 256][i mod 256]
+    more != null ==> forall i :: 0 <= i && i < |more.Contents| ==> more.Contents[i] != null && more.Contents[i].Length = 256
+    more != null ==> forall i :: 0 <= i && i < M ==> Contents[i] = more.Contents[i div 256][i mod 256]
     forall i :: M <= i && i < length ==> Contents[i] = elements[i - M]
 }
diff --git a/Test/jennisys0/runtest.bat b/Test/jennisys0/runtest.bat
index 419c8891..6bae956e 100644
--- a/Test/jennisys0/runtest.bat
+++ b/Test/jennisys0/runtest.bat
@@ -6,5 +6,5 @@ set JENNISYS_EXE=..\..\Jennisys\Jennisys\bin\Debug\Jennisys.exe
 for %%f in (Prog0.jen ExtensibleArray.jen) do (
   echo.
   echo -------------------- %%f --------------------
-  %JENNISYS_EXE% %* /trace %%f
+  %JENNISYS_EXE% %* /trace /noAnalysis %%f
 )