diff --git a/Examples/Test.hs b/Examples/Test.hs
new file mode 100644
--- /dev/null
+++ b/Examples/Test.hs
@@ -0,0 +1,121 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | A test suite to check for basic functionality.
+
+module Main where
+
+import System.Directory ( removeDirectoryRecursive
+                        , doesDirectoryExist
+                        , doesFileExist
+                        , removeFile )
+import qualified Copilot.Compile.C99 as C99
+import qualified Copilot.Compile.SBV as SBV
+import qualified Copilot.Tools.CBMC as M
+import Control.Monad (when)
+
+import AddMult
+import Array
+--import BadExtVars
+import Cast
+import ClockExamples
+import EngineExample
+import Examples
+import Examples2
+import ExtFuns
+import Local
+import LTLExamples
+import PTLTLExamples
+import Random
+import RegExpExamples
+import StackExamples
+import StatExamples
+import VotingExamples
+
+
+--------------------------------------------------------------------------------
+
+main :: IO ()
+main = do
+  cleanup
+  putStrLn "Testing addMult ..."
+  addMult         >> cleanup
+  putStrLn ""
+  putStrLn "Testing array ..."
+  array           >> cleanup
+  putStrLn ""
+--  putStrLn "Testing badExtVars ..."
+--  badExtVars      >> cleanup
+  putStrLn ""
+  putStrLn "Testing castEx ..."
+  castEx          >> cleanup
+  putStrLn ""
+  putStrLn "Testing clockExamples ..."
+  clockExamples   >> cleanup
+  putStrLn ""
+  putStrLn "Testing engineExample ..."
+  engineExample   >> cleanup
+  putStrLn ""
+  putStrLn "Testing examples ..."
+  examples        >> cleanup
+  putStrLn ""
+  putStrLn "Testing examples2 ..."
+  examples2       >> cleanup
+  putStrLn ""
+  putStrLn "Testing extFuns ..."
+  extFuns         >> cleanup
+  putStrLn ""
+  putStrLn "Testing localEx ..."
+  localEx         >> cleanup
+  putStrLn ""
+  putStrLn "Testing ltlExamples ..."
+  ltlExamples     >> cleanup
+  putStrLn ""
+  putStrLn "Testing ptltlExamples ..."
+  ptltlExamples   >> cleanup
+  putStrLn ""
+  putStrLn "Testing randomEx ..."
+  randomEx        >> cleanup
+  putStrLn ""
+  putStrLn "Testing regExpExamples ..."
+  regExpExamples  >> cleanup
+  putStrLn ""
+  putStrLn "Testing stackExamples ..."
+  stackExamples   >> cleanup
+  putStrLn ""
+  putStrLn "Testing statExamples ..."
+  statExamples    >> cleanup
+  putStrLn ""
+  putStrLn "Testing votingExamples ..."
+  votingExamples  >> cleanup
+  putStrLn ""
+  putStrLn ""
+  putStrLn "************************************"
+  putStrLn " Ok, the basic tests passed.  Enjoy!"
+  putStrLn "************************************"
+
+--------------------------------------------------------------------------------
+
+cleanup :: IO ()
+cleanup = do
+
+  b0 <- doesDirectoryExist SBV.sbvDirName
+  when b0 (removeDirectoryRecursive SBV.sbvDirName)
+
+  b1 <- doesDirectoryExist C99.c99DirName
+  when b1 (removeDirectoryRecursive C99.c99DirName)
+
+  let cbmc = "cbmc_driver.c"
+  b2 <- doesFileExist cbmc
+  when b2 (removeFile cbmc)
+
+  let atomCBMC = M.appendPrefix M.atomPrefix C99.c99DirName
+  b3 <- doesDirectoryExist atomCBMC
+  when b3 (removeDirectoryRecursive atomCBMC)
+
+  let sbvCBMC = M.appendPrefix M.sbvPrefix SBV.sbvDirName
+  b4 <- doesDirectoryExist sbvCBMC
+  when b4 (removeDirectoryRecursive sbvCBMC)
+
+--------------------------------------------------------------------------------
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -27,7 +27,7 @@
   Currently, this includes the C99 back-end and the SBV back-end.
 
 * [copilot-c99](http://hackage.haskell.org/package/copilot-c99) A back-end that
-  translates to [Atom](http://hackage.haskell.org/package/copilot-cbmc) to
+  translates to [Atom](http://hackage.haskell.org/package/atom) to
   generate hard real-time C code.
 
 Optionally, you may which also to install
diff --git a/Tests/Test.hs b/Tests/Test.hs
deleted file mode 100644
--- a/Tests/Test.hs
+++ /dev/null
@@ -1,127 +0,0 @@
---------------------------------------------------------------------------------
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
-
--- | A very small test suite to check for basic functionality.
-
-{-# LANGUAGE RebindableSyntax #-}
-
-module Main where
-
-import qualified Prelude as P
-import Language.Copilot hiding (even, odd)
-import Copilot.Compile.C99
-
-import System.Directory (removeFile)
---------------------------------------------------------------------------------
-
---
--- Some utility functions:
---
-
-flipflop :: Stream Bool -> Stream Bool
-flipflop x = y
-  where
-    y = [False] ++ if x then not y else y
-
-nats :: Stream Word64
-nats = [0] ++ nats + 1
-
-even :: (P.Integral a, Typed a) => Stream a -> Stream Bool
-even x = x `mod` 2 == 0
-
-odd :: (P.Integral a, Typed a) => Stream a -> Stream Bool
-odd = not . even
-
-counter :: (Num a, Typed a) => Stream Bool -> Stream a
-counter reset = y
-  where
-    zy = [0] ++ y
-    y  = if reset then 0 else zy + 1
-
-booleans :: Stream Bool
-booleans = [True, True, False] ++ booleans
-
-fib :: Stream Word64
-fib = [1, 1] ++ fib + drop 1 fib
-
-bitWise :: Stream Word8
-bitWise = ( let a = [ 1, 1, 0 ] ++ a in a )
-          .^.
-          ( let b = [ 0, 1, 1 ] ++ b in b )
-
-sumExterns :: Stream Word64
-sumExterns =
-  let
-    ex1 = extern "e1"
-    ex2 = extern "e2"
-  in
-    ex1 + ex2
-
---------------------------------------------------------------------------------
-
---
--- An example of a complete copilot specification.
-
-
--- A specification:
-spec :: Spec 
-spec =
-  do
-    -- A trigger with four arguments:
-    trigger "e" booleans
-      [ arg fib, arg nats, arg sumExterns, arg bitWise ]
-
-    -- A trigger with two arguments:
-    trigger "f" booleans
-      [ arg fib, arg sumExterns ]
-
-    -- A trigger with a single argument:
-    trigger "g" (flipflop booleans)
-      [ arg (sumExterns + counter false + 25) ]
-
-    -- A trigger with a single argument (should never fire):
-    trigger "h" (extern "e3" /= fib)
-      [ arg (0 :: Stream Int8) ]
-
-    observer "i" (odd nats)
-
---- Some infinite lists for simulating external variables:
-e1, e2, e3 :: [Word64]
-e1 = [0..]
-e2 = 5 : 4 : e2
-e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3)
-
-main :: IO ()
-main = do
-  putStrLn "PrettyPrinter:"
-  putStrLn ""
-  prettyPrint spec
-  putStrLn ""
-  putStrLn ""
-  putStrLn "Interpreter:"
-  putStrLn ""
-  interpret 10 [var "e1" e1, var "e2" e2, var "e3" e3] spec
-  putStrLn ""
-  putStrLn ""
-  putStrLn "Atom compilation:"
-  reify spec >>= compile defaultParams 
-  cleanUp 
-  putStrLn "*********************************"
-  putStrLn " Ok, things seem to work.  Enjoy!"
-  putStrLn "*********************************"
-
-  -- Don't assume SBV is installed.
-  -- putStrLn "Check equivalence:"
-  -- putStrLn ""
-  -- putStrLn ""
-  -- reify spec >>= 
-  --   C.genCBMC C.defaultParams {C.numIterations = 20}
-
---------------------------------------------------------------------------------
-
-cleanUp :: IO ()
-cleanUp = do
-  removeFile "copilot.c"
-  removeFile "copilot.h"
-  return ()
diff --git a/copilot.cabal b/copilot.cabal
--- a/copilot.cabal
+++ b/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             2.0.1
+version:             2.0.2
 cabal-version:       >= 1.10
 license:             BSD3
 license-file:        LICENSE
@@ -37,7 +37,7 @@
 
 executable copilot-regression
   default-language        : Haskell2010
-  hs-source-dirs          : Tests, src
+  hs-source-dirs          : Examples, src
   ghc-options             : -Wall -fwarn-tabs
   main-is                 : Test.hs
   build-depends:
@@ -45,5 +45,8 @@
                    , copilot-core
                    , copilot-language
                    , copilot-libraries
+                   , copilot-sbv
+                   , copilot-cbmc
                    , copilot-c99 >= 0.2
                    , directory >= 1.1
+                   , random