diff --git a/copilot-cbmc.cabal b/copilot-cbmc.cabal
--- a/copilot-cbmc.cabal
+++ b/copilot-cbmc.cabal
@@ -1,6 +1,6 @@
 cabal-version             : >= 1.10
 name                      : copilot-cbmc
-version                   : 0.2
+version                   : 0.11
 synopsis                  : Copilot interface to a C model-checker.
 description               : Depends on CBMC <http://www.cprover.org/cbmc/>.  Generates a driver to prove the Atom and SBV backends generate equivalent code.
 license                   : BSD3
diff --git a/src/Copilot/Tools/CBMC.hs b/src/Copilot/Tools/CBMC.hs
--- a/src/Copilot/Tools/CBMC.hs
+++ b/src/Copilot/Tools/CBMC.hs
@@ -4,14 +4,7 @@
 
 {-# LANGUAGE GADTs #-}
 
-module Copilot.Tools.CBMC 
-  ( Params (..)
-  , defaultParams
-  , genCBMC
-  , atomPrefix
-  , sbvPrefix
-  , appendPrefix
-  ) where
+module Copilot.Tools.CBMC (Params (..), defaultParams, genCBMC) where
 
 import Copilot.Core
 import qualified Copilot.Compile.C99 as C99
@@ -19,48 +12,39 @@
 import qualified System.IO as I
 import Text.PrettyPrint.HughesPJ
 
---------------------------------------------------------------------------------
-
 data Params = Params
   { numIterations :: Int }
 
---------------------------------------------------------------------------------
-
 defaultParams :: Params
 defaultParams = Params
   { numIterations = 10 }
 
---------------------------------------------------------------------------------
-
-atomPrefix, sbvPrefix :: Maybe String
-atomPrefix = Just "atm"
-sbvPrefix = Just "sbv"
-
-appendPrefix :: Maybe String -> String -> String
-appendPrefix (Just pre) name = pre ++ "_" ++ name
-appendPrefix Nothing name = name
-
---------------------------------------------------------------------------------
-
 genCBMC :: Params -> Spec -> IO ()
 genCBMC params spec =
   do
-    C99.compile (C99.defaultParams { C99.prefix = atomPrefix }) spec
-    SBV.compile (SBV.defaultParams { SBV.prefix = sbvPrefix }) spec
+    C99.compile (C99.defaultParams { C99.prefix = Just "atm" }) spec
+    SBV.compile (SBV.defaultParams { SBV.prefix = Just "sbv" }) spec
     h <- I.openFile "cbmc_driver.c" I.WriteMode
     I.hPutStrLn h (render (driver params spec))
 
---------------------------------------------------------------------------------
-
 driver :: Params -> Spec -> Doc
 driver Params { numIterations = k } spec = vcat
   [ text "#include <stdbool.h>"
   , text "#include <stdint.h>"
-  , text "#include <assert.h>"
-  , include atomPrefix C99.c99DirName C99.c99FileRoot
-  , include sbvPrefix SBV.sbvDirName "copilot"
+  , text "#include \"atm_copilot.h\""
+  , text "#include \"sbv_copilot/sbv_copilot.h\""
   , text ""
-  , declNonDets spec
+  , text "int32_t nondet_bool();"
+  , text "int32_t nondet_uint8_t();"
+  , text "int32_t nondet_uint16_t();"
+  , text "int32_t nondet_uint32_t();"
+  , text "int32_t nondet_uint64_t();"
+  , text "int32_t nondet_int8_t();"
+  , text "int32_t nondet_int16_t();"
+  , text "int32_t nondet_int32_t();"
+  , text "int32_t nondet_int64_t();"
+  , text "int32_t nondet_float();"
+  , text "int32_t nondet_double();"
   , text ""
   , declExterns spec
   , text ""
@@ -75,8 +59,8 @@
   , text "  for (i = 0; i < " <> int k <> text "; i++)"
   , text "  {"
   , text "    sampleExterns();"
-  , text $ "    " ++ appendPrefix atomPrefix "step();"
-  , text $ "    " ++ appendPrefix sbvPrefix "step();"
+  , text "    atm_step();"
+  , text "    sbv_step();"
   , text "    verify_observers();"
   , text "  }"
   , text ""
@@ -84,35 +68,13 @@
   , text "}"
   ]
 
-  where
-  include prefix dir header = text "#include" <+> doubleQuotes
-     (   text (appendPrefix prefix dir) <> text"/" 
-      <> text (appendPrefix prefix (header ++ ".h"))
-     )
-
---------------------------------------------------------------------------------
-
-declNonDets :: Spec -> Doc
-declNonDets = vcat . map declNonDet . externVars
-  where
-  declNonDet :: ExtVar -> Doc
-  declNonDet ext@(ExtVar _ t) = typeSpec t <+> nonDetName ext 
-
---------------------------------------------------------------------------------
-
-nonDetName :: ExtVar -> Doc
-nonDetName (ExtVar name t) = 
-  text ("nondet_" ++ name ++ "_") <> (typeSpec t) <> text "();"
-
---------------------------------------------------------------------------------
-
 declExterns :: Spec -> Doc
 declExterns = vcat . map declExtern . externVars
+
   where
-  declExtern :: ExtVar -> Doc
-  declExtern (ExtVar name t) = typeSpec t <+> text name <> semi
 
---------------------------------------------------------------------------------
+    declExtern :: ExtVar -> Doc
+    declExtern (ExtVar name t) = typeSpec t <+> text name <> semi
 
 sampleExterns :: Spec -> Doc
 sampleExterns spec = vcat
@@ -124,11 +86,10 @@
   ]
 
   where
-  sampleExtern :: ExtVar -> Doc
-  sampleExtern ext@(ExtVar name _) =
-    text name <+> text "=" <+> nonDetName ext
 
---------------------------------------------------------------------------------
+    sampleExtern :: ExtVar -> Doc
+    sampleExtern (ExtVar name t) =
+      text name <+> text "=" <+> text "nondet_" <> typeSpec t <> text "();"
 
 verifyObservers :: Spec -> Doc
 verifyObservers spec = vcat
@@ -140,16 +101,17 @@
   ]
 
   where
-  verifyObserver :: Observer -> Doc
-  verifyObserver (Observer name _ _) =
-    text "assert(" <> text (appendPrefix atomPrefix name) <+> text "==" 
-      <+> text (appendPrefix sbvPrefix name) <> text ");"
 
---------------------------------------------------------------------------------
+    verifyObserver :: Observer -> Doc
+    verifyObserver (Observer name _ _) =
+      text "assert(" <> text "atm_" <> text name <+> text "==" <+> text "sbv_" <>
+      text name <> text ");"
 
 typeSpec :: UType -> Doc
 typeSpec UType { uTypeType = t } = text (typeSpec' t)
+
   where
+
   typeSpec' Bool   = "bool"
   typeSpec' Int8   = "int8_t"
   typeSpec' Int16  = "int16_t"
@@ -161,5 +123,3 @@
   typeSpec' Word64 = "uint64_t"
   typeSpec' Float  = "float"
   typeSpec' Double = "double"
-
---------------------------------------------------------------------------------