diff --git a/theories/array.why b/theories/array.why
index e8e0f51aef9a9a80fc742af3828be952efd3f4e7..96542c51b9ecc7c04f1ec7138c11a8a5820ce452 100644
--- a/theories/array.why
+++ b/theories/array.why
@@ -165,7 +165,9 @@ theory ArrayRich
   logic sub (map 'a) int int : map 'a
 
   axiom Sub_length : 
-    forall s : map 'a, ofs len : int. length (sub s ofs len) = len
+    forall s : map 'a, ofs len : int.
+    len >= 0 ->
+    length (sub s ofs len) = len
 
   axiom Sub_get :
     forall s : map 'a, ofs len i : int.