diff --git a/ivory-quickcheck.cabal b/ivory-quickcheck.cabal
--- a/ivory-quickcheck.cabal
+++ b/ivory-quickcheck.cabal
@@ -1,5 +1,5 @@
 name:                ivory-quickcheck
-version:             0.2.0.3
+version:             0.2.0.4
 author:              Galois, Inc.
 copyright:           2013 Galois, Inc.
 maintainer:          leepike@galois.com
@@ -14,11 +14,11 @@
 source-repository    this
   type:     git
   location: https://github.com/GaloisInc/ivory
-  tag:      hackage-qc-0103
+  tag:      hackage-0.1.0.4
 
 library
   exposed-modules:      Ivory.QuickCheck
-  build-depends:        base >= 4.6 && < 5,
+  build-depends:        base >= 4.7 && < 5,
                         base-compat,
                         monadLib,
                         random,
diff --git a/src/Ivory/QuickCheck.hs b/src/Ivory/QuickCheck.hs
--- a/src/Ivory/QuickCheck.hs
+++ b/src/Ivory/QuickCheck.hs
@@ -1,15 +1,15 @@
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE DataKinds       #-}
+{-# LANGUAGE ImplicitParams  #-}
 {-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeOperators   #-}
 
 {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
 
 -- | Check properties of Ivory programs using random inputs.
 --
 -- Example usage:
--- 
+--
 -- > [ivory|
 -- > struct foo
 -- >   { foo_a :: Stored IFloat
@@ -43,18 +43,19 @@
 
 module Ivory.QuickCheck (check, checkWith, contract) where
 
-import           Prelude ()
+import           Prelude                         ()
 import           Prelude.Compat
 
-import           Control.Monad (replicateM,forM)
-import           Data.IORef (IORef,newIORef,readIORef,writeIORef)
-import           Data.List (transpose,find)
+import           Control.Monad                   (forM, replicateM)
+import           Data.IORef                      (IORef, newIORef, readIORef,
+                                                  writeIORef)
+import           Data.List                       (find, transpose)
 import           Ivory.Compile.C.CmdlineFrontend
 import qualified Ivory.Eval                      as E
 import           Ivory.Language
 import           Ivory.Language.Proc
 import qualified Ivory.Language.Syntax           as I
-import           System.IO.Unsafe (unsafeInterleaveIO)
+import           System.IO.Unsafe                (unsafeInterleaveIO)
 
 import qualified Test.QuickCheck.Arbitrary       as A
 import qualified Test.QuickCheck.Gen             as G
@@ -192,10 +193,10 @@
     -> sampleArray m len ty
   I.TyStruct ty
     -> sampleStruct m ty
-  I.TyProc _ _ -> err 
-  I.TyVoid     -> err 
-  I.TyPtr _    -> err 
-  I.TyCArray _ -> err 
+  I.TyProc _ _ -> err
+  I.TyVoid     -> err
+  I.TyPtr _    -> err
+  I.TyCArray _ -> err
   I.TyOpaque   -> err
   where
   err = error $ "I don't know how to make values of type '" ++ show t ++ "'!"
@@ -292,7 +293,7 @@
 sampleArray m len ty = repeatIO $ do
   (vars, blcks) <- unzip <$> replicateM len (head <$> sampleType m ty)
   let init = [ I.InitExpr ty (I.ExpVar v) | v <- vars ]
-  (v, blck) <- mkLocal (I.TyArr len ty) (I.InitArray init)
+  (v, blck) <- mkLocal (I.TyArr len ty) (I.InitArray init True)
   return (v, concat blcks ++ blck)
 
 repeatIO :: IO a -> IO [a]
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -182,13 +182,15 @@
 
 m10 :: Module
 m10 = package "foo10" (incl foo10)
-    
+
 -----------------------
 
 foo11 :: Def ('[Ix 10] ':-> ())
-foo11 = L.proc "foo11" $ \n -> body $ do
+foo11 = L.proc "foo11" $ \n ->
+          requires (n >=? 0)
+        $ body $ do
           x <- local (ival (0 :: Sint8))
-          for n $ \i -> do
+          0 `upTo` n $ \i -> do
             x' <- deref x
             store x $ x' + safeCast i
 
@@ -198,7 +200,7 @@
 -----------------------
 
 foo12 :: Def ('[Uint8] ':-> Uint8)
-foo12 = L.proc "foo12" $ \n -> 
+foo12 = L.proc "foo12" $ \n ->
         ensures (\r -> r ==? n)
       $ body $ do
           ifte_ (n ==? 0)
@@ -212,7 +214,7 @@
 -----------------------
 
 foo13 :: Def ('[Uint8, Uint8] ':-> Uint8)
-foo13 = L.proc "foo13" $ \x y -> 
+foo13 = L.proc "foo13" $ \x y ->
         requires (x <=? 15)
       $ requires (y <=? 15)
       $ body $ ret (x * y)
@@ -233,10 +235,11 @@
 -----------------------
 
 foo15 :: Def ('[Ix 10] ':-> Uint8)
-foo15 = L.proc "foo15" $ \n -> 
-  ensures (\r -> r <=? 5) $
-  body $ do
-    n `times` \i -> do
+foo15 = L.proc "foo15" $ \n ->
+    requires (n >=? 0)
+  $ ensures (\r -> r <=? 5)
+  $ body $ do
+    n `downTo` 0 $ \i -> do
       ifte_ (i >? 5) (ret 5) (ret $ safeCast i)
     ret 4 -- FIXME: Ivory.Opts.TypeCheck doesn't see above `ret`s
 
@@ -258,7 +261,7 @@
 -----------------------
 
 foo18 :: Def ('[Ref s ('L.Struct "foo2")] ':-> Ref s ('L.Struct "foo2"))
-foo18 = L.proc "foo18" $ \f -> 
+foo18 = L.proc "foo18" $ \f ->
     requires (checkStored (f ~> aFoo) (\a -> a >? 0))
   $ requires (checkStored (f ~> aFoo) (\a -> a <? 10))
   $ ensures (\r -> checkStored (r ~> aFoo) (\a -> a >? 1))