diff --git a/Examples/ExtFuns.hs b/Examples/ExtFuns.hs
--- a/Examples/ExtFuns.hs
+++ b/Examples/ExtFuns.hs
@@ -9,35 +9,36 @@
 module ExtFuns ( extFuns ) where
 
 import Language.Copilot 
---import qualified Copilot.Compile.C99 as C
+import qualified Copilot.Compile.C99 as C
+import qualified Copilot.Compile.SBV as S
+--import qualified Copilot.Tools.CBMC as B
 
 --------------------------------------------------------------------------------
 
-nats :: Stream Word16
-nats = [0] ++ nats + 1
+doubles :: Stream Word16
+doubles = [0,1] ++ doubles + 1
 
 ---------------------------------------------------------------------------------
--- Function func0 and it's environment for interpreting
 
+-- Function func0 and it's environment for interpreting
 func0 :: Stream Word16
-func0 = externFun "func0" [ funArg x, funArg nats ]
-          (Just $ cast x + nats)
+func0 = externFun "func0" [ arg x, arg doubles ]
+          (Just $ cast x + doubles)
   where x = externW8 "x" (Just [0..])
-          
----------------------------------------------------------------------------------
--- Function func0 with another set of args and it's environment for interpreting
 
--- func2 :: Stream Word16
--- func2 = externFun "func0" [ funArg $ constW8 3, funArg $ constW16 4 ]
---           (Just $ constW16 4 + 1)
-
 ---------------------------------------------------------------------------------
 
----------------------------------------------------------------------------------
 -- Function func1 and it's environment for interpreting
 func1 :: Stream Bool
 func1 = externFun "func1" [] (Just $ [False] ++ not func1)
+          
+---------------------------------------------------------------------------------
 
+-- Function func0 with another set of args and it's environment for interpreting
+func2 :: Stream Word16
+func2 = externFun "func0" [ arg $ constW8 3, arg $ constW16 4 ]
+          (Just $ cast (constW8 3) + constW16 4)
+
 ---------------------------------------------------------------------------------
 
 a :: Stream Word16
@@ -46,11 +47,14 @@
 spec :: Spec
 spec = trigger "trigger" true [ arg func0
                               , arg func1
+                              , arg func2
                               , arg a ]
   
 extFuns :: IO ()
 extFuns = do
---    reify spec >>= C.compile C.defaultParams 
-    interpret 10 spec
+   interpret 10 spec
+   reify spec >>= C.compile C.defaultParams 
+   reify spec >>= S.compile S.defaultParams 
+
 
 --------------------------------------------------------------------------------
diff --git a/Examples/Sat.hs b/Examples/Sat.hs
new file mode 100644
--- /dev/null
+++ b/Examples/Sat.hs
@@ -0,0 +1,67 @@
+-- | Example of a simple SAT solver (simply constructs the truth table) in
+-- Copilot.
+
+-- {-# LANGUAGE RebindableSyntax #-}
+
+module Sat where
+
+import Language.Copilot
+import qualified Prelude as P
+import Control.Monad (foldM_)
+
+---------------------------------------------------------------------------------
+
+-- | Number of sat variables and a Boolean function over those variables.
+type SatFunc = (Int, [Stream Bool] -> Stream Bool)
+
+-- Takes a Sat function and returns the stream of variables and a SAT function.
+sat :: SatFunc -> ([Stream Bool], Stream Bool)
+sat (i,f) = (xs, res)
+  where
+  -- If it becomes true, it stays true.
+  res   = [False] ++ (f xs || res)
+
+  xs  = xs' i
+
+  xs' 0 = []
+  xs' n = clk (period $ 2 P.^ n) (phase (0 :: Int)) : xs' (n P.- 1)
+
+satSpec :: SatFunc -> Spec
+satSpec f = do
+  observer "sat" (snd $ sat f)
+  observer "done" done
+  foldM_ mkObs (0 :: Int) xs
+
+  where
+  xs = fst $ sat f
+  cnt :: Stream Word64 -- Would need to be extended depending on number of
+                       -- variables.
+  cnt = [1] ++ cnt + 1
+  done = cnt == (2 P.^ length xs)
+  mkObs idx strm = do observer ("obs" P.++ show idx) strm
+                      return (idx P.+ 1)
+
+
+f0 :: SatFunc
+--f0 = (3, \[a,b,c] -> a && (b || (not c)))
+f0 = (3, f) 
+  where 
+  f [a,b,c] = a && (b || (not c))
+  f _       = error "Bad SAT function."
+
+f1 :: SatFunc
+f1 = (9, f')
+  where
+  f' [a,b,c,d,e,f,g,h,i] = 
+    a && b && c && d && e && 
+      f && g && h && i && i && not i
+  f' _ = error "Bad SAT function."
+
+-- | Run the interpreter long enough to get an answer.
+runFunc :: SatFunc -> IO ()
+runFunc f = interpret (2 P.^ fst f) (satSpec f)
+
+satExamples :: IO ()
+satExamples = runFunc f0 >> runFunc f1
+
+---------------------------------------------------------------------------------
diff --git a/copilot.cabal b/copilot.cabal
--- a/copilot.cabal
+++ b/copilot.cabal
@@ -1,5 +1,5 @@
 name:                copilot
-version:             2.0.5
+version:             2.0.6
 cabal-version:       >= 1.10
 license:             BSD3
 license-file:        LICENSE
@@ -30,7 +30,7 @@
     build-depends:
                        base >= 4.0 && <5
                      , copilot-core >= 0.2.3
-                     , copilot-language >= 0.3
+                     , copilot-language >= 0.4
                      , copilot-libraries
                      , copilot-cbmc
     exposed-modules: Language.Copilot
@@ -63,6 +63,8 @@
                   , PTLTLExamples
                   , Random
                   , RegExpExamples
+                  , Sat
                   , StackExamples
                   , StatExamples
                   , VotingExamples
+