diff --git a/bench/Main.hs b/bench/Main.hs
--- a/bench/Main.hs
+++ b/bench/Main.hs
@@ -58,21 +58,27 @@
 
 testResultRecords :: TestResult -> [NamedRecord]
 testResultRecords (TestResult name l s ls lss _)
-  = [ namedRecord $ [ "Benchmark" .= B8.pack name
-                    , "Tool"      .= B8.pack "Target" ]
-                 ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d l ]
-    , namedRecord $ [ "Benchmark" .= B8.pack name
-                    , "Tool"      .= B8.pack "SmallCheck" ]
-                 ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d s ]
-    , namedRecord $ [ "Benchmark" .= B8.pack name
-                    , "Tool"      .= B8.pack "Lazy-SmallCheck" ]
-                 ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d ls ]
+  = [ namedRecord [ "Depth" .= bshow d
+                  , "Target" .= uncurry toResult (lookup3 d l)
+                  , "SmallCheck" .= uncurry toResult (lookup3 d s)
+                  , "Lazy-SmallCheck" .= uncurry toResult (lookup3 d ls)
+                  ]
+      <> maybe (namedRecord []) (\ss ->
+          namedRecord [ "Lazy-SmallCheck-slow" .= uncurry toResult (lookup3 d ss)])
+         lss
+    | d <- [2..20]
     ]
-   ++ maybe [] (\ss ->
-    [ namedRecord $ [ "Benchmark" .= B8.pack name
-                    , "Tool"      .= B8.pack "Lazy-SmallCheck-slow" ]
-                 ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d ss ]
-    ]) lss
+  -- = [ namedRecord $ [ "Tool"      .= B8.pack "Target" ]
+  --                ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d l ]
+  --   , namedRecord $ [ "Tool"      .= B8.pack "SmallCheck" ]
+  --                ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d s ]
+  --   , namedRecord $ [ "Tool"      .= B8.pack "Lazy-SmallCheck" ]
+  --                ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d ls ]
+  --   ]
+  --  ++ maybe [] (\ss ->
+  --   [ namedRecord $ [ "Tool"      .= B8.pack "Lazy-SmallCheck-slow" ]
+  --                ++ [ bshow d .= toResult t o | d <- [2..20], let (t,o) = lookup3 d ss ]
+  --   ]) lss
 
 bshow :: Show a => a -> B.ByteString
 bshow = B8.pack . show
@@ -83,14 +89,17 @@
                  Just (i,d,o) -> (d,o)
 
 toResult :: Double -> Outcome -> B.ByteString
-toResult d TimeOut      = "X"
+toResult d TimeOut      = "nan"
 toResult d (Complete i) = bshow d
 
-header :: V.Vector B.ByteString
-header = V.fromList $ ["Benchmark", "Tool"] ++ [bshow d | d <- [2..20]]
+-- header :: V.Vector B.ByteString
+-- header = V.fromList $ ["Tool"] ++ [bshow d | d <- [2..20]]
+header (TestResult name l s ls lss _)
+  = V.fromList $ [ "Depth", "Target", "SmallCheck", "Lazy-SmallCheck"]
+              ++ maybe [] (const ["Lazy-SmallCheck-slow"]) lss
 
 logCsv f r = withFile f WriteMode $ \h -> do
-  LB.hPutStr h $ encodeByName header $ testResultRecords r
+  LB.hPutStr h $ encodeByName (header r) $ testResultRecords r
   return r
 
 main :: IO ()
@@ -170,7 +179,7 @@
 checkTarget f n m = checkMany (show n++"/Target")
                               (\d max -> resultPassed <$>
                                          targetResultWith f n m (mkOpts d max))
-  where mkOpts d max = defaultOpts { depth = d, maxSuccess = Just max, scDepth = True }
+  where mkOpts d max = defaultOpts { logging = False, depth = d, maxSuccess = Just max, scDepth = True }
 
 checkSmall p n = checkMany (show n++"/SmallCheck")
                            (\d n -> fromIntegral.fst.fst <$> runTestWithStats d n (p d))
diff --git a/src/Test/Target.hs b/src/Test/Target.hs
--- a/src/Test/Target.hs
+++ b/src/Test/Target.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE ViewPatterns #-}
 module Test.Target
-  ( target, targetResult, targetWith, targetResultWith
+  ( target, targetResult, targetWith, targetResultWith, targetResultWithStr
   -- , targetTH
   , Result(..), Testable
   , TargetOpts(..), defaultOpts
@@ -57,7 +57,10 @@
 
 -- | Like 'targetWith', but returns the 'Result' instead of printing to standard out.
 targetResultWith :: Testable f => f -> TH.Name -> FilePath -> TargetOpts -> IO Result
-targetResultWith f (show -> name) path opts
+targetResultWith f (show -> name) path opts = targetResultWithStr f name path opts
+
+targetResultWithStr :: Testable f => f -> String -> FilePath -> TargetOpts -> IO Result
+targetResultWithStr f name path opts
   = do when (verbose opts) $
          printf "Testing %s\n" name
        sp  <- getSpec path
diff --git a/src/Test/Target/Testable.hs b/src/Test/Target/Testable.hs
--- a/src/Test/Target/Testable.hs
+++ b/src/Test/Target/Testable.hs
@@ -75,7 +75,12 @@
           | Just (_ :: AsyncException) <- fromException e -> throwM e
           | Just (SmtError _) <- fromException e -> throwM e
           | Just (ExpectedValues _) <- fromException e -> throwM e
-          | otherwise -> mbKeepGoing xs n
+          | otherwise -> do
+              real <- gets realized
+              modify $ \s@(TargetState {..}) -> s { realized = [] }
+              _ <- io $ command ctx $ Assert Nothing $ PNot $ pAnd
+                    [ ESym (SL $ symbolText x) `eq` ESym (SL v) | (x,v) <- real ]
+              mbKeepGoing xs n'
         Right r -> do
           real <- gets realized
           modify $ \s@(TargetState {..}) -> s { realized = [] }
@@ -89,16 +94,17 @@
           -- causing us to return a spurious error
           _ <- io $ command ctx $ Assert Nothing $ PNot $ pAnd
                 [ ESym (SL $ symbolText x) `eq` ESym (SL v) | (x,v) <- real ]
-          -- let env = map (second (`app` [])) cts ++ mkExprs f (map fst xts) xs
-          -- sat <- evalType (M.fromList env) to (toExpr r)
+
           case sat of
             False -> mbKeepGoing xs n'
-            True ->
+            True -> do
               asks maxSuccess >>= \case
                 Nothing -> go n' =<< io (command ctx CheckSat)
                 Just m | m == n' -> return $ Passed m
                        | otherwise -> go n' =<< io (command ctx CheckSat)
+
     go _ r = error $ "go _ " ++ show r
+
     mbKeepGoing xs n = do
       kg <- asks keepGoing
       if kg
@@ -118,8 +124,10 @@
   mkExprs    :: f -> [Symbol] -> HList (Args f) -> [(Symbol,Expr)]
 
 instance (Show a, Targetable a, Testable b) => Testable (a -> b) where
-  queryArgs f d (stripQuals -> (RFun _ i o _))
-    = liftM2 (:) (query (Proxy :: Proxy a) d i) (queryArgs (f undefined) d o)
+  queryArgs f d (stripQuals -> (RFun x i o _))
+    = do v  <- query (Proxy :: Proxy a) d i
+         vs <- queryArgs (f undefined) d (subst (mkSubst [(x,var v)]) o)
+         return (v:vs)
   queryArgs _ _ t = error $ "queryArgs called with non-function type: " ++ show t
   decodeArgs f (v:vs) (t:ts)
     = liftM2 (:::) (decode v t) (decodeArgs (f undefined) vs ts)
diff --git a/src/Test/Target/Util.hs b/src/Test/Target/Util.hs
--- a/src/Test/Target/Util.hs
+++ b/src/Test/Target/Util.hs
@@ -120,7 +120,7 @@
                           , GHC.hscTarget = GHC.HscNothing --GHC.HscInterpreted
                           -- , GHC.optLevel  = 0 --2
                           , GHC.log_action = \_ _ _ _ _ -> return ()
-                          , GHC.importPaths = GHC.importPaths df
+                          , GHC.importPaths = "bench" : GHC.importPaths df
                           } `GHC.gopt_set` GHC.Opt_ImplicitImportQualified
                             `GHC.xopt_set` GHC.Opt_MagicHash
              _ <- GHC.setSessionDynFlags df'
diff --git a/target.cabal b/target.cabal
--- a/target.cabal
+++ b/target.cabal
@@ -1,5 +1,5 @@
 name:                target
-version:             0.1.0.0
+version:             0.1.1.0
 synopsis:            Generate test-suites from refinement types.
 
 description:         Target is a library for testing Haskell functions based on