diff --git a/COPYRIGHT b/COPYRIGHT
--- a/COPYRIGHT
+++ b/COPYRIGHT
@@ -1,4 +1,4 @@
-Copyright (c) 2010-2011, Levent Erkok (erkokl@gmail.com)
+Copyright (c) 2010-2012, Levent Erkok (erkokl@gmail.com)
 All rights reserved.
 
 The sbv library is distributed with the BSD3 license. See the LICENSE file
diff --git a/Data/SBV.hs b/Data/SBV.hs
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -20,7 +20,7 @@
 --
 -- >>> prove $ forAll ["x"] $ \x -> x `shiftL` 2 .== (x :: SWord8)
 -- Falsifiable. Counter-example:
---   x = 128 :: SWord8
+--   x = 51 :: SWord8
 --
 -- The function 'prove' has the following type:
 --
@@ -166,6 +166,9 @@
   , minimize, maximize, optimize
   , minimizeWith, maximizeWith, optimizeWith
 
+  -- * Computing expected values
+  , expectedValue, expectedValueWith
+
   -- * Model extraction
   -- $modelExtraction
 
@@ -175,7 +178,7 @@
 
   -- ** Programmable model extraction
   -- $programmableExtraction
-  , SatModel(..), Modelable(..), displayModels
+  , SatModel(..), Modelable(..), displayModels, extractModels
 
   -- * SMT Interface: Configurations and solvers
   , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), yices, z3, defaultSMTCfg
@@ -187,14 +190,14 @@
   , compileToSMTLib
 
   -- * Test case generation
-  , genTest, CW(..), Size(..)
+  , genTest, getTestValues, TestVectors, TestStyle(..), renderTest, CW(..), Size(..), cwToBool
 
   -- * Code generation from symbolic programs
   -- $cCodeGeneration
   , SBVCodeGen
 
   -- ** Setting code-generation options
-  , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver
+  , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile
 
   -- ** Designating inputs
   , cgInput, cgInputArr
@@ -220,17 +223,18 @@
   ) where
 
 import Data.SBV.BitVectors.Data
-import Data.SBV.BitVectors.GenTest
 import Data.SBV.BitVectors.Model
-import Data.SBV.BitVectors.Optimize
 import Data.SBV.BitVectors.PrettyNum
-import Data.SBV.BitVectors.Polynomial
 import Data.SBV.BitVectors.SignCast
 import Data.SBV.BitVectors.Splittable
 import Data.SBV.BitVectors.STree
 import Data.SBV.Compilers.C
 import Data.SBV.Compilers.CodeGen
 import Data.SBV.Provers.Prover
+import Data.SBV.Tools.GenTest
+import Data.SBV.Tools.ExpectedValue
+import Data.SBV.Tools.Optimize
+import Data.SBV.Tools.Polynomial
 import Data.SBV.Utils.Boolean
 import Data.Bits
 import Data.Word
@@ -423,15 +427,28 @@
 A probabilistic constraint (see 'pConstrain') attaches a probability threshold for the
 constraint to be considered. For instance:
 
-  @'pConstrain' 0.8 c@
+  @
+     'pConstrain' 0.8 c
+  @
 
-will add the constraint @c@ 80% of the time. This variant is useful for 'genTest' and 'quickCheck' functions,
-where we want to filter the test cases according to some probability distribution, to make sure that the test-vectors
-are drawn from interesting subsets of the input space.
+will make sure that the condition @c@ is satisfied 80% of the time (and correspondingly, falsified 20%
+of the time), in expectation. This variant is useful for 'genTest' and 'quickCheck' functions, where we
+want to filter the test cases according to some probability distribution, to make sure that the test-vectors
+are drawn from interesting subsets of the input space. For instance, if we were to generate 100 test cases
+with the above constraint, we'd expect about 80 of them to satisfy the condition @c@, while about 20 of them
+will fail it.
 
+The following properties hold:
+
+  @
+    'constrain'      = 'pConstrain' 1
+    'pConstrain' t c = 'pConstrain' (1-t) (not c)
+  @
+
 Note that while 'constrain' can be used freely, 'pConstrain' is only allowed in the contexts of
-'genTest' or 'quickCheck'. Calls to 'pConstrain' in a prove/sat call will be rejected as it makes no sense.
-Also, 'constrain' and 'pConstrain' calls during code-generation will also be rejected, for similar reasons.
+'genTest' or 'quickCheck'. Calls to 'pConstrain' in a prove/sat call will be rejected as SBV does not
+deal with probabilistic constraints when it comes to satisfiability and proofs.
+Also, both 'constrain' and 'pConstrain' calls during code-generation will also be rejected, for similar reasons.
 -}
 
 {-# ANN module "HLint: ignore Use import/export shortcut" #-}
diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs
--- a/Data/SBV/BitVectors/Data.hs
+++ b/Data/SBV/BitVectors/Data.hs
@@ -22,7 +22,7 @@
  ( SBool, SWord8, SWord16, SWord32, SWord64
  , SInt8, SInt16, SInt32, SInt64, SInteger
  , SymWord(..)
- , CW(..), cwSameType, cwIsBit, cwToBool, constrain, pConstrain
+ , CW(..), cwSameType, cwIsBit, cwToBool
  , mkConstCW ,liftCW2, mapCW, mapCW2
  , SW(..), trueSW, falseSW, trueCW, falseCW
  , SBV(..), NodeId(..), mkSymSBV
@@ -30,7 +30,8 @@
  , sbvToSW, sbvToSymSW
  , SBVExpr(..), newExpr
  , cache, uncache, uncacheAI, HasSignAndSize(..)
- , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Size(..), Outputtable(..), Result(..), getTraceInfo, getConstraints
+ , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Size(..), Outputtable(..), Result(..)
+ , getTraceInfo, getConstraints, addConstraint
  , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom
  , Quantifier(..), needsExistentials
  , SMTLibPgm(..), SMTLibVersion(..)
@@ -72,6 +73,7 @@
 cwIsBit :: CW -> Bool
 cwIsBit x = not (hasSign x) && not (isInfPrec x) && intSizeOf x == 1
 
+-- | Convert a CW to a Haskell boolean
 cwToBool :: CW -> Bool
 cwToBool x = cwVal x /= 0
 
@@ -357,11 +359,17 @@
         external (ArrayMerge{})  = False
 
 -- | Different means of running a symbolic piece of code
-data SBVRunMode = Proof Bool  -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance
-                | CodeGen     -- ^ Code generation mode
-                | Concrete    -- ^ Concrete simulation mode
+data SBVRunMode = Proof Bool      -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance
+                | CodeGen         -- ^ Code generation mode
+                | Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs
 
+isConcreteMode :: SBVRunMode -> Bool
+isConcreteMode (Concrete _) = True
+isConcreteMode (Proof{})    = False
+isConcreteMode CodeGen      = False
+
 data State  = State { runMode       :: SBVRunMode
+                    , rStdGen       :: IORef StdGen
                     , rCInfo        :: IORef [(String, CW)]
                     , rctr          :: IORef Int
                     , rInfPrec      :: IORef Bool
@@ -382,9 +390,9 @@
 
 inProofMode :: State -> Bool
 inProofMode s = case runMode s of
-                  Proof{}  -> True
-                  CodeGen  -> False
-                  Concrete -> False
+                  Proof{}    -> True
+                  CodeGen    -> False
+                  Concrete{} -> False
 
 -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic
 -- value (@Right Cached@). Note that caching is essential for making
@@ -422,7 +430,7 @@
 -- | Infinite precision signed symbolic value
 type SInteger = SBV Integer
 
--- Needed to satisfy the Num hierarchy
+-- Not particularly "desirable", but will do if needed
 instance Show (SBV a) where
   show (SBV _                     (Left c))  = show c
   show (SBV (_  , Size Nothing)   (Right _)) = "<symbolic> :: SInteger"
@@ -446,6 +454,12 @@
               i `seq` writeIORef (rctr s) i
               return ctr
 
+throwDice :: State -> IO Double
+throwDice st = do g <- readIORef (rStdGen st)
+                  let (r, g') = randomR (0, 1) g
+                  writeIORef (rStdGen st) g'
+                  return r
+
 newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
 newUninterpreted st nm t mbCode
   | null nm || not (isAlpha (head nm)) || not (all validChar (tail nm))
@@ -520,17 +534,17 @@
         st <- ask
         let q = case (mbQ, runMode st) of
                   (Just x,  _)           -> x   -- user given, just take it
-                  (Nothing, Concrete)    -> ALL -- concrete simulation, pick universal
+                  (Nothing, Concrete{})  -> ALL -- concrete simulation, pick universal
                   (Nothing, Proof True)  -> EX  -- sat mode, pick existential
                   (Nothing, Proof False) -> ALL -- proof mode, pick universal
                   (Nothing, CodeGen)     -> ALL -- code generation, pick universal
         case runMode st of
-          Concrete | q == EX -> case mbNm of
-                                  Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: SBV a)
-                                  Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ showType (undefined :: SBV a)
-          Concrete           -> do v@(SBV _ (Left cw)) <- liftIO randomIO
-                                   liftIO $ modifyIORef (rCInfo st) ((maybe "_" id mbNm, cw):)
-                                   return v
+          Concrete _ | q == EX -> case mbNm of
+                                    Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: SBV a)
+                                    Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ showType (undefined :: SBV a)
+          Concrete _           -> do v@(SBV _ (Left cw)) <- liftIO randomIO
+                                     liftIO $ modifyIORef (rCInfo st) ((maybe "_" id mbNm, cw):)
+                                     return v
           _          -> do ctr <- liftIO $ incCtr st
                            let nm = maybe ('s':show ctr) id mbNm
                                sw = SW sgnsz (NodeId ctr)
@@ -560,6 +574,12 @@
           liftIO $ modifyIORef (routs st) (sw:)
           return i
 
+instance Outputtable a => Outputtable [a] where
+  output = mapM output
+
+instance Outputtable () where
+  output = return
+
 instance (Outputtable a, Outputtable b) => Outputtable (a, b) where
   output = mlift2 (,) output output
 
@@ -613,7 +633,11 @@
    aiCache <- newIORef IMap.empty
    infPrec <- newIORef False
    cstrs   <- newIORef []
+   rGen    <- case currentRunMode of
+                Concrete g -> newIORef g
+                _          -> newStdGen >>= newIORef
    let st = State { runMode      = currentRunMode
+                  , rStdGen      = rGen
                   , rCInfo       = cInfo
                   , rctr         = ctr
                   , rInfPrec     = infPrec
@@ -829,32 +853,27 @@
 mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
 mkSFunArray = SFunArray
 
----------------------------------------------------------------------------------
--- | Adding arbitrary constraints.
----------------------------------------------------------------------------------
-constrain :: SBool -> Symbolic ()
-constrain c = do
-        st <- ask
-        liftIO $ do v <- sbvToSW st c
-                    modifyIORef (rConstraints st) (v:)
 
----------------------------------------------------------------------------------
--- | Adding a probabilistic constraint. The 'Double' argument is the probability
--- threshold. A threshold of '0' would mean the constraint is ignored, while a
--- threshold of '1' means the constraint is always added. Probabilistic constraints
--- are useful for 'genTest' and 'quickCheck' calls where we restrict our attention
--- to /interesting/ parts of the input domain.
----------------------------------------------------------------------------------
-pConstrain :: Double -> SBool -> Symbolic ()
-pConstrain t c
+-- | Handling constraints
+imposeConstraint :: SBool -> Symbolic ()
+imposeConstraint c = do st <- ask
+                        case runMode st of
+                          CodeGen -> error "SBV: constraints are not allowed in code-generation"
+                          _       -> do liftIO $ do v <- sbvToSW st c
+                                                    modifyIORef (rConstraints st) (v:)
+
+addConstraint :: Maybe Double -> SBool -> SBool -> Symbolic ()
+addConstraint Nothing  c _  = imposeConstraint c
+addConstraint (Just t) c c'
   | t < 0 || t > 1
   = error $ "SBV: pConstrain: Invalid probability threshold: " ++ show t ++ ", must be in [0, 1]."
   | True
   = do st <- ask
-       case runMode st of
-         Concrete -> when (t > 0) $ do r <- liftIO $ randomRIO (0, 1)
-                                       when (r <= t) $ constrain c
-         _        -> error "SBV: pConstrain only allowed in 'genTest' or 'quickCheck' contexts."
+       when (not (isConcreteMode (runMode st))) $ error "SBV: pConstrain only allowed in 'genTest' or 'quickCheck' contexts."
+       case () of
+         () | t > 0 && t < 1 -> liftIO (throwDice st) >>= \d -> imposeConstraint (if d <= t then c else c')
+            | t > 0          -> imposeConstraint c
+            | True           -> imposeConstraint c'
 
 ---------------------------------------------------------------------------------
 -- * Cached values
diff --git a/Data/SBV/BitVectors/GenTest.hs b/Data/SBV/BitVectors/GenTest.hs
deleted file mode 100644
--- a/Data/SBV/BitVectors/GenTest.hs
+++ /dev/null
@@ -1,37 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Data.SBV.BitVectors.GenTest
--- Copyright   :  (c) Levent Erkok
--- License     :  BSD3
--- Maintainer  :  erkokl@gmail.com
--- Stability   :  experimental
--- Portability :  portable
---
--- Test generation from symbolic programs
------------------------------------------------------------------------------
-
-module Data.SBV.BitVectors.GenTest (genTest) where
-
-import Data.Maybe (fromMaybe)
-
-import Data.SBV.BitVectors.Data
-
--- | Generate a set of concrete test values from a symbolic program. The output
--- can be rendered as test vectors in different languages as necessary. Use the
--- function 'output' call to indicate what fields should be in the test result.
--- (Also see 'constrain' and 'pConstrain' for filtering acceptable test values.)
-genTest :: Int -> Symbolic () -> IO [([CW], [CW])]
-genTest n m = gen 0 []
-  where gen i sofar
-         | i == n = return (reverse sofar)
-         | True   = do mbT <- tc
-                       case mbT of
-                        Nothing -> gen i     sofar
-                        Just t  -> gen (i+1) (t:sofar)
-        tc = do (_, Result _ tvals _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' Concrete m
-                let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpeted constants!") . (`lookup` cs)
-                    cond = all (cwToBool . cval) cstrs
-                    io   = (map snd tvals, map cval os)
-                if cond
-                   then return $ Just io
-                   else return Nothing
diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs
--- a/Data/SBV/BitVectors/Model.hs
+++ b/Data/SBV/BitVectors/Model.hs
@@ -23,6 +23,7 @@
     Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..)
   , bitValue, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE
   , lsb, msb, SBVUF, sbvUFName, genFinVar, genFinVar_, forall, forall_, exists, exists_
+  , constrain, pConstrain
   )
   where
 
@@ -37,7 +38,7 @@
 
 import Test.QuickCheck                           (Testable(..), Arbitrary(..))
 import qualified Test.QuickCheck         as QC   (whenFail)
-import qualified Test.QuickCheck.Monadic as QC   (monadicIO, run, pre)
+import qualified Test.QuickCheck.Monadic as QC   (monadicIO, run)
 import System.Random
 
 import Data.SBV.BitVectors.Data
@@ -541,7 +542,7 @@
 -- a concrete argument for obvious reasons. Other variants (succ, pred, [x..]) etc are similarly
 -- limited. While symbolic variants can be defined for many of these, they will just diverge
 -- as final sizes cannot be determined statically.
-instance (Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) where
+instance (Show a, Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) where
   succ x
     | v == (maxBound :: a) = error $ "Enum.succ{" ++ showType x ++ "}: tried to take `succ' of maxBound"
     | True                 = fromIntegral $ v + 1
@@ -735,9 +736,11 @@
                       () | swt == falseSW -> sbvToSW st b
                       () -> do swa <- sbvToSW st a
                                swb <- sbvToSW st b
-                               if swa == swb
-                                  then return swa
-                                  else newExpr st sgnsz (SBVApp Ite [swt, swa, swb])
+                               case () of
+                                 () | swa == swb                      -> return swa
+                                 () | swa == trueSW && swb == falseSW -> return swt
+                                 () | swa == falseSW && swa == trueSW -> newExpr st sgnsz (SBVApp Not [swt])
+                                 ()                                   -> newExpr st sgnsz (SBVApp Ite [swt, swa, swb])
   -- Custom version of select that translates to SMT-Lib tables at the base type of words
   select xs err ind
     | Just i <- unliteral ind
@@ -1126,6 +1129,20 @@
   sbvUninterpret mbCgData nm = let (h, f) = sbvUninterpret (uc7 `fmap` mbCgData) nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6)
     where uc7 (cs, fn) = (cs, \a b c d e f g -> fn (a, b, c, d, e, f, g))
 
+---------------------------------------------------------------------------------
+-- | Adding arbitrary constraints.
+---------------------------------------------------------------------------------
+constrain :: SBool -> Symbolic ()
+constrain c = addConstraint Nothing c (bnot c)
+
+---------------------------------------------------------------------------------
+-- | Adding a probabilistic constraint. The 'Double' argument is the probability
+-- threshold. Probabilistic constraints are useful for 'genTest' and 'quickCheck'
+-- calls where we restrict our attention to /interesting/ parts of the input domain.
+---------------------------------------------------------------------------------
+pConstrain :: Double -> SBool -> Symbolic ()
+pConstrain t c = addConstraint (Just t) c (bnot c)
+
 -- Quickcheck interface on symbolic-booleans..
 instance Testable SBool where
   property (SBV _ (Left b)) = property (cwToBool b)
@@ -1133,21 +1150,17 @@
 
 instance Testable (Symbolic SBool) where
   property m = QC.whenFail (putStrLn msg) $ QC.monadicIO test
-    where test = do mbDie <- QC.run $ do
-                                (r, Result _ tvals _ _ cs _ _ _ _ _ cstrs _) <- runSymbolic' Concrete m
-                                let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)
-                                    cond = all (cwToBool . cval) cstrs
-                                when (isSymbolic r) $ error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show r ++ ")"
-                                if cond
-                                   then if r `isConcretely` id
-                                           then return $ Just True
-                                           else do putStrLn $ complain tvals
-                                                   return Nothing
-                                   else return $ Just False
-                    case mbDie of
-                      Just True  -> return ()           -- test successfull, continue
-                      Just False -> QC.pre False        -- precondition failed, ignore
-                      Nothing    -> fail "Falsifiable"  -- property failed, die
+    where runOnce g = do (r, Result _ tvals _ _ cs _ _ _ _ _ cstrs _) <- runSymbolic' (Concrete g) m
+                         let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)
+                             cond = all (cwToBool . cval) cstrs
+                         when (isSymbolic r) $ error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show r ++ ")"
+                         if cond then if r `isConcretely` id
+                                         then return False
+                                         else do putStrLn $ complain tvals
+                                                 return True
+                                 else runOnce g -- cstrs failed, go again
+          test = do die <- QC.run $ newStdGen >>= runOnce
+                    when die $ fail "Falsifiable"
           msg = "*** SBV: See the custom counter example reported above."
           complain []     = "*** SBV Counter Example: Predicate contains no universally quantified variables."
           complain qcInfo = intercalate "\n" $ "*** SBV Counter Example:" : map (("  " ++) . info) qcInfo
diff --git a/Data/SBV/BitVectors/Optimize.hs b/Data/SBV/BitVectors/Optimize.hs
deleted file mode 100644
--- a/Data/SBV/BitVectors/Optimize.hs
+++ /dev/null
@@ -1,108 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Data.SBV.BitVectors.Optimize
--- Copyright   :  (c) Levent Erkok
--- License     :  BSD3
--- Maintainer  :  erkokl@gmail.com
--- Stability   :  experimental
--- Portability :  portable
---
--- Number representations in hex/bin
------------------------------------------------------------------------------
-
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-
-module Data.SBV.BitVectors.Optimize (OptimizeOpts(..), optimize, optimizeWith, minimize, minimizeWith, maximize, maximizeWith) where
-
-import Data.Maybe (fromJust)
-
-import Data.SBV.BitVectors.Data
-import Data.SBV.BitVectors.Model (OrdSymbolic(..), EqSymbolic(..))
-import Data.SBV.Provers.Prover   (satWith, z3)
-import Data.SBV.SMT.SMT          (SatModel, getModel, SMTConfig(..))
-import Data.SBV.Utils.Boolean
-
--- | Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable.
--- For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions
--- can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.
-data OptimizeOpts = Iterative  Bool   -- ^ Iteratively search. if True, it will be reporting progress
-                  | Quantified        -- ^ Use quantifiers
-
--- | Symbolic optimization. Generalization on 'minimize' and 'maximize' that allows arbitrary
--- cost functions and comparisons.
-optimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c)
-             => SMTConfig                         -- ^ SMT configuration
-             -> OptimizeOpts                      -- ^ Optimization options
-             -> (SBV c -> SBV c -> SBool)         -- ^ comparator
-             -> ([SBV a] -> SBV c)                -- ^ cost function
-             -> Int                               -- ^ how many elements?
-             -> ([SBV a] -> SBool)                -- ^ validity constraint
-             -> IO (Maybe [a])
-optimizeWith cfg (Iterative chatty) = iterOptimize chatty cfg
-optimizeWith cfg Quantified         = quantOptimize cfg
-
--- | Variant of 'optimizeWith' using z3
-optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
-optimize = optimizeWith z3
-
--- | Variant of 'maximize' allowing the use of a user specified solver.
-maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
-maximizeWith cfg opts = optimizeWith cfg opts (.>=)
-
--- | Maximizes a cost function with respect to a constraint. Examples:
---
---   >>> maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))
---   Just [9,9,9]
-maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
-maximize = maximizeWith z3
-
--- | Variant of 'minimize' allowing the use of a user specified solver.
-minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
-minimizeWith cfg opts = optimizeWith cfg opts (.<=)
-
--- | Minimizes a cost function with respect to a constraint. Examples:
---
---   >>> minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))
---   Just [11,11,11]
-minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
-minimize = minimizeWith z3
-
--- | Optimization using quantifiers
-quantOptimize :: (SatModel a, SymWord a) => SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
-quantOptimize cfg cmp cost n valid = do
-           m <- satWith cfg $ do xs <- mkExistVars  n
-                                 ys <- mkForallVars n
-                                 return $ valid xs &&& (valid ys ==> cost xs `cmp` cost ys)
-           case getModel m of
-              Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""
-              Right (False, a) -> return $ Just a
-              Left _           -> return Nothing
-
--- | Optimization using iteration
-iterOptimize :: (SatModel a, Show a, SymWord a, Show c, SymWord c) =>  Bool -> SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
-iterOptimize chatty cfg cmp cost n valid = do
-        msg "Trying to find a satisfying solution."
-        m <- satWith cfg $ valid `fmap` mkExistVars n
-        case getModel m of
-          Left _ -> return Nothing
-          Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""
-          Right (False, a) -> do msg $ "First solution found: " ++ show a
-                                 let c = cost (map literal a)
-                                 msg $ "Initial value is    : " ++ show (fromJust (unliteral c))
-                                 msg "Starting iterative search."
-                                 go (1::Int) a c
-  where msg m | chatty = putStrLn $ "*** " ++ m
-              | True   = return ()
-        go i curSol curCost = do
-                msg $ "Round " ++ show i ++ " ****************************"
-                m <- satWith cfg $ do xs <- mkExistVars n
-                                      return $ let c = cost xs in valid xs &&& (c `cmp` curCost &&& c ./= curCost)
-                case getModel m of
-                  Left _ -> do msg "The current solution is optimal. Terminating search."
-                               return $ Just curSol
-                  Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""
-                  Right (False, a) -> do msg $ "Solution: " ++ show a
-                                         let c = cost (map literal a)
-                                         msg $ "Value   : " ++ show (fromJust (unliteral c))
-                                         go (i+1) a c
diff --git a/Data/SBV/BitVectors/Polynomial.hs b/Data/SBV/BitVectors/Polynomial.hs
deleted file mode 100644
--- a/Data/SBV/BitVectors/Polynomial.hs
+++ /dev/null
@@ -1,238 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  Data.SBV.BitVectors.Polynomials
--- Copyright   :  (c) Levent Erkok
--- License     :  BSD3
--- Maintainer  :  erkokl@gmail.com
--- Stability   :  experimental
--- Portability :  portable
---
--- Implementation of polynomial arithmetic
------------------------------------------------------------------------------
-
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-
-module Data.SBV.BitVectors.Polynomial (Polynomial(..), crc, crcBV) where
-
-import Data.Bits  (Bits(..))
-import Data.List  (genericTake)
-import Data.Maybe (fromJust)
-import Data.Word  (Word8, Word16, Word32, Word64)
-
-import Data.SBV.BitVectors.Data
-import Data.SBV.BitVectors.Model
-import Data.SBV.BitVectors.Splittable
-import Data.SBV.Utils.Boolean
-
--- | Implements polynomial addition, multiplication, division, and modulus operations
--- over GF(2^n).  NB. Similar to 'bvQuotRem', division by @0@ is interpreted as follows:
---
---     @x `pDivMod` 0 = (0, x)@
---
--- for all @x@ (including @0@)
---
--- Minimal complete definiton: 'pMult', 'pDivMod', 'showPolynomial'
-class Bits a => Polynomial a where
- -- | Given bit-positions to be set, create a polynomial
- -- For instance
- --
- --     @polynomial [0, 1, 3] :: SWord8@
- -- 
- -- will evaluate to @11@, since it sets the bits @0@, @1@, and @3@. Mathematicans would write this polynomial
- -- as @x^3 + x + 1@. And in fact, 'showPoly' will show it like that.
- polynomial :: [Int] -> a
- -- | Add two polynomials in GF(2^n)
- pAdd  :: a -> a -> a
- -- | Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by
- -- the polynomial as specified by coefficients of the third argument. Note that the third
- -- argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our
- -- formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not
- -- support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles,
- -- so this should not be a problem in practice.)
- --
- -- Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't
- -- fit into the resulting size.
- pMult :: (a, a, [Int]) -> a
- -- | Divide two polynomials in GF(2^n), see above note for division by 0
- pDiv  :: a -> a -> a
- -- | Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0
- pMod  :: a -> a -> a
- -- | Division and modulus packed together
- pDivMod :: a -> a -> (a, a)
- -- | Display a polynomial like a mathematician would (over the monomial @x@), with a type
- showPoly :: a -> String
- -- | Display a polynomial like a mathematician would (over the monomial @x@), the first argument
- -- controls if the final type is shown as well.
- showPolynomial :: Bool -> a -> String
-
- -- defaults.. Minumum complete definition: pMult, pDivMod, showPolynomial
- polynomial = foldr (flip setBit) 0
- pAdd       = xor
- pDiv x y   = fst (pDivMod x y)
- pMod x y   = snd (pDivMod x y)
- showPoly   = showPolynomial False
-
-
-instance Polynomial Word8   where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}
-instance Polynomial Word16  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}
-instance Polynomial Word32  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}
-instance Polynomial Word64  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}
-instance Polynomial SWord8  where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}
-instance Polynomial SWord16 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}
-instance Polynomial SWord32 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}
-instance Polynomial SWord64 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}
-
-lift :: SymWord a => ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
-lift f (x, y, z) = fromJust $ unliteral $ f (literal x, literal y, z)
-liftC :: SymWord a => (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
-liftC f x y = let (a, b) = f (literal x) (literal y) in (fromJust (unliteral a), fromJust (unliteral b))
-liftS :: SymWord a => (a -> String) -> SBV a -> String
-liftS f s
-  | Just x <- unliteral s = f x
-  | True                  = show s
-
--- | Pretty print as a polynomial
-sp :: Bits a => Bool -> a -> String
-sp st a
- | null cs = '0' : t
- | True    = foldr (\x y -> sh x ++ " + " ++ y) (sh (last cs)) (init cs) ++ t
- where t | st   = " :: GF(2^" ++ show n ++ ")"
-         | True = ""
-       n  = bitSize a
-       is = [n-1, n-2 .. 0]
-       cs = map fst $ filter snd $ zip is (map (testBit a) is)
-       sh 0 = "1"
-       sh 1 = "x"
-       sh i = "x^" ++ show i
-
--- | Add two polynomials
-addPoly :: [SBool] -> [SBool] -> [SBool]
-addPoly xs    []      = xs
-addPoly []    ys      = ys
-addPoly (x:xs) (y:ys) = x <+> y : addPoly xs ys
-
-ites :: SBool -> [SBool] -> [SBool] -> [SBool]
-ites s xs ys
- | Just t <- unliteral s
- = if t then xs else ys
- | True
- = go xs ys
- where go [] []         = []
-       go []     (b:bs) = ite s false b : go [] bs
-       go (a:as) []     = ite s a false : go as []
-       go (a:as) (b:bs) = ite s a b : go as bs
-
--- | Multiply two polynomials and reduce by the third (concrete) irreducible, given by its coefficients.
--- See the remarks for the 'pMult' function for this design choice
-polyMult :: (Bits a, SymWord a, FromBits (SBV a)) => (SBV a, SBV a, [Int]) -> SBV a
-polyMult (x, y, red)
-  | isInfPrec x
-  = error $ "SBV.polyMult: Received infinite precision value: " ++ show x
-  | True
-  = fromBitsLE $ genericTake sz $ r ++ repeat false
-  where (_, r) = mdp ms rs
-        ms = genericTake (2*sz) $ mul (blastLE x) (blastLE y) [] ++ repeat false
-        rs = genericTake (2*sz) $ [if i `elem` red then true else false |  i <- [0 .. foldr max 0 red] ] ++ repeat false
-        sz = intSizeOf x
-        mul _  []     ps = ps
-        mul as (b:bs) ps = mul (false:as) bs (ites b (as `addPoly` ps) ps)
-
-polyDivMod :: (Bits a, SymWord a, FromBits (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
-polyDivMod x y
-   | isInfPrec x
-   = error $ "SBV.polyDivMod: Received infinite precision value: " ++ show x
-   | True
-   = ite (y .== 0) (0, x) (adjust d, adjust r)
-   where adjust xs = fromBitsLE $ genericTake sz $ xs ++ repeat false
-         sz        = intSizeOf x
-         (d, r)    = mdp (blastLE x) (blastLE y)
-
--- conservative over-approximation of the degree
-degree :: [SBool] -> Int
-degree xs = walk (length xs - 1) $ reverse xs
-  where walk n []     = n
-        walk n (b:bs)
-         | Just t <- unliteral b
-         = if t then n else walk (n-1) bs
-         | True
-         = n -- over-estimate
-
-mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
-mdp xs ys = go (length ys - 1) (reverse ys)
-  where degTop  = degree xs
-        go _ []     = error "SBV.Polynomial.mdp: Impossible happened; exhausted ys before hitting 0"
-        go n (b:bs)
-         | n == 0   = (reverse qs, rs)
-         | True     = let (rqs, rrs) = go (n-1) bs
-                      in (ites b (reverse qs) rqs, ites b rs rrs)
-         where degQuot = degTop - n
-               ys' = replicate degQuot false ++ ys
-               (qs, rs) = divx (degQuot+1) degTop xs ys'
-
--- return the element at index i; if not enough elements, return false
--- N.B. equivalent to '(xs ++ repeat false) !! i', but more efficient
-idx :: [SBool] -> Int -> SBool
-idx []     _ = false
-idx (x:_)  0 = x
-idx (_:xs) i = idx xs (i-1)
-
-divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
-divx n _ xs _ | n <= 0 = ([], xs)
-divx n i xs ys'        = (q:qs, rs)
-  where q        = xs `idx` i
-        xs'      = ites q (xs `addPoly` ys') xs
-        (qs, rs) = divx (n-1) (i-1) xs' (tail ys')
-
--- | Compute CRCs over bit-vectors. The call @crcBV n m p@ computes
--- the CRC of the message @m@ with respect to polynomial @p@. The
--- inputs are assumed to be blasted big-endian. The number
--- @n@ specifies how many bits of CRC is needed. Note that @n@
--- is actually the degree of the polynomial @p@, and thus it seems
--- redundant to pass it in. However, in a typical proof context,
--- the polynomial can be symbolic, so we cannot compute the degree
--- easily. While this can be worked-around by generating code that
--- accounts for all possible degrees, the resulting code would
--- be unnecessarily big and complicated, and much harder to reason
--- with. (Also note that a CRC is just the remainder from the
--- polynomial division, but this routine is much faster in practice.)
---
--- NB. The @n@th bit of the polynomial @p@ /must/ be set for the CRC
--- to be computed correctly. Note that the polynomial argument 'p' will
--- not even have this bit present most of the time, as it will typically
--- contain bits @0@ through @n-1@ as usual in the CRC literature. The higher
--- order @n@th bit is simply assumed to be set, as it does not make
--- sense to use a polynomial of a lesser degree. This is usually not a problem
--- since CRC polynomials are designed and expressed this way.
---
--- NB. The literature on CRC's has many variants on how CRC's are computed.
--- We follow the painless guide (<http://www.ross.net/crc/download/crc_v3.txt>)
--- and compute the CRC as follows:
---
---     * Extend the message 'm' by adding 'n' 0 bits on the right
---
---     * Divide the polynomial thus obtained by the 'p'
---
---     * The remainder is the CRC value.
---
--- There are many variants on final XOR's, reversed polynomials etc., so
--- it is essential to double check you use the correct /algorithm/.
-crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
-crcBV n m p = take n $ go (replicate n false) (m ++ replicate n false)
-  where mask = drop (length p - n) p
-        go c []     = c
-        go c (b:bs) = go next bs
-          where c' = drop 1 c ++ [b]
-                next = ite (head c) (zipWith (<+>) c' mask) c'
-
--- | Compute CRC's over polynomials, i.e., symbolic words. The first
--- 'Int' argument plays the same role as the one in the 'crcBV' function.
-crc :: (FromBits (SBV a), FromBits (SBV b), Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b
-crc n m p
-  | isInfPrec m || isInfPrec p
-  = error $ "SBV.crc: Received an infinite precision value: " ++ show (m, p)
-  | True
-  = fromBitsBE $ replicate (sz - n) false ++ crcBV n (blastBE m) (blastBE p)
-  where sz = intSizeOf p
diff --git a/Data/SBV/BitVectors/PrettyNum.hs b/Data/SBV/BitVectors/PrettyNum.hs
--- a/Data/SBV/BitVectors/PrettyNum.hs
+++ b/Data/SBV/BitVectors/PrettyNum.hs
@@ -13,7 +13,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
-module Data.SBV.BitVectors.PrettyNum (PrettyNum(..), readBin, shex, sbin) where
+module Data.SBV.BitVectors.PrettyNum (PrettyNum(..), readBin, shex, shexI, sbin, sbinI) where
 
 import Data.Char  (ord)
 import Data.Int   (Int8, Int16, Int32, Int64)
@@ -83,7 +83,7 @@
   hex  s = maybe (show s) (hex :: a -> String)  $ unliteral s
   bin  s = maybe (show s) (bin :: a -> String)  $ unliteral s
 
-shex :: (Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
+shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
 shex shType shPre (signed, size) a
  | a < 0
  = "-" ++ pre ++ pad l (s16 (abs (fromIntegral a :: Integer)))  ++ t
@@ -106,7 +106,7 @@
        pre | shPre = "0x"
            | True  = ""
 
-sbin :: (Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
+sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
 sbin shType shPre (signed,size) a
  | a < 0
  = "-" ++ pre ++ pad size (s2 (abs (fromIntegral a :: Integer)))  ++ t
@@ -131,7 +131,7 @@
 pad :: Int -> String -> String
 pad l s = replicate (l - length s) '0' ++ s
 
-s2, s16 :: Integral a => a -> String
+s2, s16 :: (Show a, Integral a) => a -> String
 s2  v = showIntAtBase 2 dig v "" where dig = fromJust . flip lookup [(0, '0'), (1, '1')]
 s16 v = showHex v ""
 
diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs
--- a/Data/SBV/Compilers/C.hs
+++ b/Data/SBV/Compilers/C.hs
@@ -19,9 +19,9 @@
 import Data.List                     (nub)
 import Data.Maybe                    (isJust, fromMaybe, isNothing)
 import qualified Data.Foldable as F  (toList)
-import Text.PrettyPrint.HughesPJ
 import System.FilePath               (takeBaseName, replaceExtension)
 import System.Random
+import Text.PrettyPrint.HughesPJ
 
 import Data.SBV.BitVectors.Data
 import Data.SBV.BitVectors.PrettyNum (shex)
@@ -96,7 +96,7 @@
    -- we rnf the sig to make sure any exceptions in type conversion pop-out early enough
    -- this is purely cosmetic, of course..
    = rnf (render sig) `seq` result
-  where result = CgPgmBundle $ filt [ ("Makefile",  (CgMakefile flags, [genMake driver nm nmd flags]))
+  where result = CgPgmBundle $ filt [ ("Makefile",  (CgMakefile flags, [genMake (cgGenDriver cfg) nm nmd flags]))
                                     , (nm  ++ ".h", (CgHeader [sig],   [genHeader nm [sig] extProtos]))
                                     , (nmd ++ ".c", (CgDriver,         genDriver mbISize randVals nm ins outs mbRet))
                                     , (nm  ++ ".c", (CgSource,         genCProg rtc mbISize nm sig sbvProg ins outs mbRet extDecls))
@@ -104,8 +104,10 @@
         rtc      = cgRTC cfg
         mbISize  = cgInteger cfg
         randVals = cgDriverVals cfg
-        driver   = cgGenDriver cfg
-        filt xs  = if driver then xs else filter (not . isCgDriver . fst . snd) xs
+        filt xs  = [c | c@(_, (k, _)) <- xs, need k]
+          where need k | isCgDriver   k = cgGenDriver cfg
+                       | isCgMakefile k = cgGenMakefile cfg
+                       | True           = True
         nmd      = nm ++ "_driver"
         sig      = pprCFunHeader mbISize nm ins outs mbRet
         ins      = cgInputs st
@@ -153,12 +155,12 @@
 -- | Renders as "s0", etc, or the corresponding constant
 showSW :: Maybe Int -> [(SW, CW)] -> SW -> Doc
 showSW mbISize consts sw
-  | sw == falseSW                 = text "0"
-  | sw == trueSW                  = text "1"
+  | sw == falseSW                 = text "false"
+  | sw == trueSW                  = text "true"
   | Just cw <- sw `lookup` consts = showConst mbISize cw
   | True                          = text $ show sw
 
--- | Words as it would be defined in the standard header stdint.h
+-- | Words as it would map to a C word
 pprCWord :: Bool -> (Bool, Int) -> Doc
 pprCWord cnst sgsz = (if cnst then text "const" else empty) <+> text (showCType sgsz)
 
@@ -188,7 +190,7 @@
 --   Note that this automatically takes care of the boolean (1-bit) value problem, since it
 --   shows the result as an integer, which is OK as far as C is concerned.
 mkConst :: Integer -> (Bool, Int) -> Doc
-mkConst i   (False,  1) = integer i
+mkConst i   (False,  1) = text (if i == 0 then "false" else "true")
 mkConst i   (False,  8) = integer i
 mkConst i   (True,   8) = integer i
 mkConst i t@(False, 16) = text (shex False True t i) <> text "U"
@@ -255,9 +257,12 @@
   $$ text ""
   $$ text "#include <inttypes.h>"
   $$ text "#include <stdint.h>"
+  $$ text "#include <stdbool.h>"
   $$ text ""
+  $$ text "/* The boolean type */"
+  $$ text "typedef bool SBool;"
+  $$ text ""
   $$ text "/* Unsigned bit-vectors */"
-  $$ text "typedef uint8_t  SBool  ;"
   $$ text "typedef uint8_t  SWord8 ;"
   $$ text "typedef uint16_t SWord16;"
   $$ text "typedef uint32_t SWord32;"
@@ -290,6 +295,7 @@
               $$ text ""
               $$ text "#include <inttypes.h>"
               $$ text "#include <stdint.h>"
+              $$ text "#include <stdbool.h>"
               $$ text "#include <stdio.h>"
        header =  text "#include" <+> doubleQuotes (nm <> text ".h")
               $$ text ""
@@ -380,6 +386,7 @@
               $$ text ""
               $$ text "#include <inttypes.h>"
               $$ text "#include <stdint.h>"
+              $$ text "#include <stdbool.h>"
        header = text "#include" <+> doubleQuotes (nm <> text ".h")
        post   = text ""
              $$ vcat (map codeSeg cgs)
@@ -461,7 +468,7 @@
         p Not [a]
           -- be careful about booleans, bitwise complement is not correct for them!
           | s == 1
-          = parens (text "~" <> a) <+> text "&" <+> text "0x01U"
+          = text "!" <> a
           | True
           = text "~" <> a
           where s = cSizeOf mbISize (head opArgs)
@@ -555,9 +562,10 @@
 
 -- | Merge a bunch of bundles to generate code for a library
 mergeToLib :: String -> [CgPgmBundle] -> CgPgmBundle
-mergeToLib libName bundles = CgPgmBundle $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake]
+mergeToLib libName bundles = CgPgmBundle $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake]
   where files       = concat [fs | CgPgmBundle fs <- bundles]
         sigs        = concat [ss | (_, (CgHeader ss, _)) <- files]
+        anyMake     = not (null [() | (_, (CgMakefile{}, _)) <- files])
         drivers     = [ds | (_, (CgDriver, ds)) <- files]
         anyDriver   = not (null drivers)
         mkFlags     = nub (concat [xs | (_, (CgMakefile xs, _)) <- files])
@@ -620,6 +628,7 @@
             $$ text ""
             $$ text "#include <inttypes.h>"
             $$ text "#include <stdint.h>"
+            $$ text "#include <stdbool.h>"
             $$ text "#include <stdio.h>"
             $$ inc
         mkDFun (f, [_pre, _header, body, _post]) = [header, body, post]
diff --git a/Data/SBV/Compilers/CodeGen.hs b/Data/SBV/Compilers/CodeGen.hs
--- a/Data/SBV/Compilers/CodeGen.hs
+++ b/Data/SBV/Compilers/CodeGen.hs
@@ -17,11 +17,12 @@
 
 import Control.Monad.Trans
 import Control.Monad.State.Lazy
-import Data.Char (toLower)
-import Data.List (nub, isPrefixOf, intercalate, (\\))
-import System.Directory (createDirectory, doesDirectoryExist, doesFileExist)
-import System.FilePath ((</>))
-import Text.PrettyPrint.HughesPJ (Doc, render, vcat)
+import Data.Char                 (toLower, isSpace)
+import Data.List                 (nub, isPrefixOf, intercalate, (\\))
+import System.Directory          (createDirectory, doesDirectoryExist, doesFileExist)
+import System.FilePath           ((</>))
+import Text.PrettyPrint.HughesPJ (Doc, vcat)
+import qualified Text.PrettyPrint.HughesPJ as P (render)
 
 import Data.SBV.BitVectors.Data
 
@@ -32,15 +33,16 @@
 
 -- | Options for code-generation.
 data CgConfig = CgConfig {
-          cgRTC        :: Bool          -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.
-        , cgInteger    :: Maybe Int     -- ^ Bit-size to use for representing SInteger (if any)
-        , cgDriverVals :: [Integer]     -- ^ Values to use for the driver program generated, useful for generating non-random drivers.
-        , cgGenDriver  :: Bool          -- ^ If 'True', will generate a driver program
+          cgRTC         :: Bool          -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.
+        , cgInteger     :: Maybe Int     -- ^ Bit-size to use for representing SInteger (if any)
+        , cgDriverVals  :: [Integer]     -- ^ Values to use for the driver program generated, useful for generating non-random drivers.
+        , cgGenDriver   :: Bool          -- ^ If 'True', will generate a driver program
+        , cgGenMakefile :: Bool          -- ^ If 'True', will generate a makefile
         }
 
 -- | Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.
 defaultCgConfig :: CgConfig
-defaultCgConfig = CgConfig { cgRTC = False, cgInteger = Nothing, cgDriverVals = [], cgGenDriver = True }
+defaultCgConfig = CgConfig { cgRTC = False, cgInteger = Nothing, cgDriverVals = [], cgGenDriver = True, cgGenMakefile = True }
 
 -- | Abstraction of target language values
 data CgVal = CgAtomic SW
@@ -96,11 +98,15 @@
   | True
   = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgInteger = Just i }})
 
--- | Should we generate a driver program? Default: 'True'. When a library is generated, then it will have
+-- | Should we generate a driver program? Default: 'True'. When a library is generated, it will have
 -- a driver if any of the contituent functions has a driver. (See 'compileToCLib'.)
 cgGenerateDriver :: Bool -> SBVCodeGen ()
 cgGenerateDriver b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenDriver = b } })
 
+-- | Should we generate a Makefile? Default: 'True'.
+cgGenerateMakefile :: Bool -> SBVCodeGen ()
+cgGenerateMakefile b = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgGenMakefile = b } })
+
 -- | Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.
 cgSetDriverValues :: [Integer] -> SBVCodeGen ()
 cgSetDriverValues vs = modify (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgDriverVals = vs } })
@@ -180,12 +186,16 @@
 isCgDriver CgDriver = True
 isCgDriver _        = False
 
+isCgMakefile :: CgPgmKind -> Bool
+isCgMakefile CgMakefile{} = True
+isCgMakefile _            = False
+
 instance Show CgPgmBundle where
    show (CgPgmBundle fs) = intercalate "\n" $ map showFile fs
 
 showFile :: (FilePath, (CgPgmKind, [Doc])) -> String
 showFile (f, (_, ds)) =  "== BEGIN: " ++ show f ++ " ================\n"
-                      ++ render (vcat ds)
+                      ++ render' (vcat ds)
                       ++ "== END: " ++ show f ++ " =================="
 
 codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle
@@ -219,4 +229,10 @@
                 else putStrLn "Aborting."
   where renderFile (f, (_, ds)) = do let fn = dirName </> f
                                      putStrLn $ "Generating: " ++ show fn ++ ".."
-                                     writeFile fn (render (vcat ds))
+                                     writeFile fn (render' (vcat ds))
+
+-- Pretty's render might have "leading" white-space in empty lines, eliminate:
+render' :: Doc -> String
+render' = unlines . map clean . lines . P.render
+  where clean x | all isSpace x = ""
+                | True          = x
diff --git a/Data/SBV/Examples/BitPrecise/Legato.hs b/Data/SBV/Examples/BitPrecise/Legato.hs
--- a/Data/SBV/Examples/BitPrecise/Legato.hs
+++ b/Data/SBV/Examples/BitPrecise/Legato.hs
@@ -283,7 +283,7 @@
 
 -- | The correctness theorem.
 --   On a decent MacBook Pro, this proof takes about 3 minutes with the 'SFunArray' memory model
---   and about 30 minutes with the 'SArray' model.
+--   and about 30 minutes with the 'SArray' model, using yices as the SMT solver
 correctnessTheorem :: IO ThmResult
 correctnessTheorem = proveWith yices{timing = True} $
     forAll ["mem", "addrX", "x", "addrY", "y", "addrLow", "regX", "regA", "memVals", "flagC", "flagZ"]
diff --git a/Data/SBV/Examples/BitPrecise/PrefixSum.hs b/Data/SBV/Examples/BitPrecise/PrefixSum.hs
--- a/Data/SBV/Examples/BitPrecise/PrefixSum.hs
+++ b/Data/SBV/Examples/BitPrecise/PrefixSum.hs
@@ -127,9 +127,11 @@
 --
 -- Also, the unit @0@ is clearly not a left-unit for @flOp@, as the third
 -- equation for @flOp@ will simply map many elements to @0@.
+-- (NB. We need to use yices for this proof as the uninterpreted function
+-- examples are only supported through the yices interface currently.)
 thm3 :: IO ThmResult
-thm3 = prove $ do args :: PowerList SWord32 <- mkForallVars 8
-                  return $ ps (u, op) args .== lf (u, op) args
+thm3 = proveWith yices $ do args :: PowerList SWord32 <- mkForallVars 8
+                            return $ ps (u, op) args .== lf (u, op) args
   where op :: SWord32 -> SWord32 -> SWord32
         op = uninterpret "flOp"
         u :: SWord32
diff --git a/Data/SBV/Examples/CodeGeneration/AddSub.hs b/Data/SBV/Examples/CodeGeneration/AddSub.hs
--- a/Data/SBV/Examples/CodeGeneration/AddSub.hs
+++ b/Data/SBV/Examples/CodeGeneration/AddSub.hs
@@ -18,113 +18,120 @@
 addSub :: SWord8 -> SWord8 -> (SWord8, SWord8)
 addSub x y = (x+y, x-y)
 
--- | Generate C code for addSub. This will place the files in a directory called @genAddSub@,
--- generating the following files:
---
--- File: @Makefile@
---
--- > # Makefile for addSub. Automatically generated by SBV. Do not edit!
--- > 
--- > # include any user-defined .mk file in the current directory.
--- > -include *.mk
--- > 
--- > CC=gcc
--- > CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
--- > 
--- > all: addSub_driver
--- > 
--- > addSub.o: addSub.c addSub.h
--- > 	${CC} ${CCFLAGS} -c $< -o $@
--- > 
--- > addSub_driver.o: addSub_driver.c
--- > 	${CC} ${CCFLAGS} -c $< -o $@
--- > 
--- > addSub_driver: addSub.o addSub_driver.o
--- > 	${CC} ${CCFLAGS} $^ -o $@
--- > 
--- > clean:
--- > 	rm -f *.o
--- > 
--- > veryclean: clean
--- > 	rm -f addSub_driver
---
--- File: @addSub.h@
---
--- > /* Header file for addSub. Automatically generated by SBV. Do not edit! */
--- > 
--- > #ifndef __addSub__HEADER_INCLUDED__
--- > #define __addSub__HEADER_INCLUDED__
--- > 
--- > #include <inttypes.h>
--- > #include <stdint.h>
--- > 
--- > /* Unsigned bit-vectors */
--- > typedef uint8_t  SBool  ;
--- > typedef uint8_t  SWord8 ;
--- > typedef uint16_t SWord16;
--- > typedef uint32_t SWord32;
--- > typedef uint64_t SWord64;
--- > 
--- > /* Signed bit-vectors */
--- > typedef int8_t  SInt8 ;
--- > typedef int16_t SInt16;
--- > typedef int32_t SInt32;
--- > typedef int64_t SInt64;
--- > 
--- > /* Entry point prototype: */
--- > void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
--- >             SWord8 *dif);
--- > 
--- > #endif /* __addSub__HEADER_INCLUDED__ */
---
--- File: @addSub.c@
---
--- > /* File: "addSub.c". Automatically generated by SBV. Do not edit! */
--- > 
--- > #include <inttypes.h>
--- > #include <stdint.h>
--- > #include "addSub.h"
--- > 
--- > void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
--- >             SWord8 *dif)
--- > {
--- >   const SWord8 s0 = x;
--- >   const SWord8 s1 = y;
--- >   const SWord8 s2 = s0 + s1;
--- >   const SWord8 s3 = s0 - s1;
--- >   
--- >   *sum = s2;
--- >   *dif = s3;
--- > }
---
--- File: @addSub_driver.c@
+-- | Generate C code for addSub. Here's the output showing the generated C code:
 --
--- > /* Example driver program for addSub. */
--- > /* Automatically generated by SBV. Edit as you see fit! */
--- > 
--- > #include <inttypes.h>
--- > #include <stdint.h>
--- > #include <stdio.h>
--- > #include "addSub.h"
--- > 
--- > int main(void)
--- > {
--- >   SWord8 sum;
--- >   SWord8 dif;
--- >   
--- >   addSub(132, 241, &sum, &dif);
--- >   
--- >   printf("addSub(132, 241, &sum, &dif) ->\n");
--- >   printf("  sum = %"PRIu8"\n", sum);
--- >   printf("  dif = %"PRIu8"\n", dif);
--- >   
--- >   return 0;
--- > }
+-- >>> genAddSub
+-- == BEGIN: "Makefile" ================
+-- # Makefile for addSub. Automatically generated by SBV. Do not edit!
+-- <BLANKLINE>
+-- # include any user-defined .mk file in the current directory.
+-- -include *.mk
+-- <BLANKLINE>
+-- CC=gcc
+-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+-- <BLANKLINE>
+-- all: addSub_driver
+-- <BLANKLINE>
+-- addSub.o: addSub.c addSub.h
+-- 	${CC} ${CCFLAGS} -c $< -o $@
+-- <BLANKLINE>
+-- addSub_driver.o: addSub_driver.c
+-- 	${CC} ${CCFLAGS} -c $< -o $@
+-- <BLANKLINE>
+-- addSub_driver: addSub.o addSub_driver.o
+-- 	${CC} ${CCFLAGS} $^ -o $@
+-- <BLANKLINE>
+-- clean:
+-- 	rm -f *.o
+-- <BLANKLINE>
+-- veryclean: clean
+-- 	rm -f addSub_driver
+-- == END: "Makefile" ==================
+-- == BEGIN: "addSub.h" ================
+-- /* Header file for addSub. Automatically generated by SBV. Do not edit! */
+-- <BLANKLINE>
+-- #ifndef __addSub__HEADER_INCLUDED__
+-- #define __addSub__HEADER_INCLUDED__
+-- <BLANKLINE>
+-- #include <inttypes.h>
+-- #include <stdint.h>
+-- #include <stdbool.h>
+-- <BLANKLINE>
+-- /* The boolean type */
+-- typedef bool SBool;
+-- <BLANKLINE>
+-- /* Unsigned bit-vectors */
+-- typedef uint8_t  SWord8 ;
+-- typedef uint16_t SWord16;
+-- typedef uint32_t SWord32;
+-- typedef uint64_t SWord64;
+-- <BLANKLINE>
+-- /* Signed bit-vectors */
+-- typedef int8_t  SInt8 ;
+-- typedef int16_t SInt16;
+-- typedef int32_t SInt32;
+-- typedef int64_t SInt64;
+-- <BLANKLINE>
+-- /* Entry point prototype: */
+-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
+--             SWord8 *dif);
+-- <BLANKLINE>
+-- #endif /* __addSub__HEADER_INCLUDED__ */
+-- == END: "addSub.h" ==================
+-- == BEGIN: "addSub_driver.c" ================
+-- /* Example driver program for addSub. */
+-- /* Automatically generated by SBV. Edit as you see fit! */
+-- <BLANKLINE>
+-- #include <inttypes.h>
+-- #include <stdint.h>
+-- #include <stdbool.h>
+-- #include <stdio.h>
+-- #include "addSub.h"
+-- <BLANKLINE>
+-- int main(void)
+-- {
+--   SWord8 sum;
+--   SWord8 dif;
+-- <BLANKLINE>
+--   addSub(132, 241, &sum, &dif);
+-- <BLANKLINE>
+--   printf("addSub(132, 241, &sum, &dif) ->\n");
+--   printf("  sum = %"PRIu8"\n", sum);
+--   printf("  dif = %"PRIu8"\n", dif);
+-- <BLANKLINE>
+--   return 0;
+-- }
+-- == END: "addSub_driver.c" ==================
+-- == BEGIN: "addSub.c" ================
+-- /* File: "addSub.c". Automatically generated by SBV. Do not edit! */
+-- <BLANKLINE>
+-- #include <inttypes.h>
+-- #include <stdint.h>
+-- #include <stdbool.h>
+-- #include "addSub.h"
+-- <BLANKLINE>
+-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
+--             SWord8 *dif)
+-- {
+--   const SWord8 s0 = x;
+--   const SWord8 s1 = y;
+--   const SWord8 s2 = s0 + s1;
+--   const SWord8 s3 = s0 - s1;
+-- <BLANKLINE>
+--   *sum = s2;
+--   *dif = s3;
+-- }
+-- == END: "addSub.c" ==================
 --
 genAddSub :: IO ()
-genAddSub = compileToC (Just "xx") "addSub" $ do
+genAddSub = compileToC outDir "addSub" $ do
         x <- cgInput "x"
         y <- cgInput "y"
+        -- leave the cgDriverVals call out for generating a driver with random values
+        cgSetDriverValues [132, 241]
         let (s, d) = addSub x y
         cgOutput "sum" s
         cgOutput "dif" d
+ where -- use Just "dirName" for putting the output to the named directory
+       -- otherwise, it'll go to standard output
+       outDir = Nothing
diff --git a/Data/SBV/Examples/CodeGeneration/GCD.hs b/Data/SBV/Examples/CodeGeneration/GCD.hs
--- a/Data/SBV/Examples/CodeGeneration/GCD.hs
+++ b/Data/SBV/Examples/CodeGeneration/GCD.hs
@@ -81,6 +81,7 @@
 -- > 
 -- > #include <inttypes.h>
 -- > #include <stdint.h>
+-- > #include <stdbool.h>
 -- > #include "sgcd.h"
 -- > 
 -- > SWord8 sgcd(const SWord8 x, const SWord8 y)
diff --git a/Data/SBV/Examples/CodeGeneration/PopulationCount.hs b/Data/SBV/Examples/CodeGeneration/PopulationCount.hs
--- a/Data/SBV/Examples/CodeGeneration/PopulationCount.hs
+++ b/Data/SBV/Examples/CodeGeneration/PopulationCount.hs
@@ -40,8 +40,8 @@
 -- go 8 bits at a time instead of one by one, by using a precomputed table
 -- of population-count values for each byte. This algorithm /loops/ only
 -- 8 times, and hence is at least 8 times more efficient.
-popCount :: SWord64 -> SWord8
-popCount inp = go inp 0 0
+popCountFast :: SWord64 -> SWord8
+popCountFast inp = go inp 0 0
   where go :: SWord64 -> Int -> SWord8 -> SWord8
         go _ 8 c = c
         go x i c = go (x `shiftR` 8) (i+1) (c + select pop8 0 (x .&. 0xff))
@@ -57,19 +57,20 @@
 -----------------------------------------------------------------------------
 
 {- $VerificationIntro
-We prove that `popCount` and `popCountSlow` are functionally equivalent.
-This is essential as we will automatically generate C code from `popCount`,
+We prove that `popCountFast` and `popCountSlow` are functionally equivalent.
+This is essential as we will automatically generate C code from `popCountFast`,
 and we would like to make sure that the fast version is correct with
 respect to the slower reference version.
 -}
 
 -- | States the correctness of faster population-count algorithm, with respect
--- to the reference slow version. We have:
+-- to the reference slow version. (We use yices here as it's quite fast for
+-- this problem. Z3 seems to take much longer.) We have:
 --
--- >>> prove fastPopCountIsCorrect
+-- >>> proveWith yices fastPopCountIsCorrect
 -- Q.E.D.
 fastPopCountIsCorrect :: SWord64 -> SBool
-fastPopCountIsCorrect x = popCount x .== popCountSlow x
+fastPopCountIsCorrect x = popCountFast x .== popCountSlow x
 
 -----------------------------------------------------------------------------
 -- * Code generation
@@ -79,142 +80,145 @@
 -- generate C code to compute population-counts for us. This action will generate all the
 -- C files that you will need, including a driver program for test purposes.
 --
--- Below is the generated header file for `popCount`:
---
--- > /* Header file for popCount. Automatically generated by SBV. Do not edit! */
--- > 
--- > #ifndef __popCount__HEADER_INCLUDED__
--- > #define __popCount__HEADER_INCLUDED__
--- > 
--- > #include <inttypes.h>
--- > #include <stdint.h>
--- > 
--- > /* Unsigned bit-vectors */
--- > typedef uint8_t  SBool  ;
--- > typedef uint8_t  SWord8 ;
--- > typedef uint16_t SWord16;
--- > typedef uint32_t SWord32;
--- > typedef uint64_t SWord64;
--- > 
--- > /* Signed bit-vectors */
--- > typedef int8_t  SInt8 ;
--- > typedef int16_t SInt16;
--- > typedef int32_t SInt32;
--- > typedef int64_t SInt64;
--- > 
--- > /* Entry point prototype: */
--- > SWord8 popCount(const SWord64 x);
--- > 
--- > #endif /* __popCount__HEADER_INCLUDED__ */
---
--- The generated C function. Note how the Haskell list `pop8` is turned into a look-up
--- table automatically (see @table0@ below) in the C code.
---
--- > /* File: "popCount.c". Automatically generated by SBV. Do not edit! */
--- > 
--- > #include <inttypes.h>
--- > #include <stdint.h>
--- > #include "popCount.h"
--- > 
--- > SWord8 popCount(const SWord64 x)
--- > {
--- >   const SWord64 s0 = x;
--- >   static const SWord8 table0[] = {
--- >       0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3,
--- >       3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4,
--- >       3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2,
--- >       2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5,
--- >       3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5,
--- >       5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3,
--- >       2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4,
--- >       4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
--- >       3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4,
--- >       4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6,
--- >       5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5,
--- >       5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8
--- >   };
--- >   const SWord64 s11 = s0 & 0x00000000000000ffULL;
--- >   const SWord8  s12 = table0[s11];
--- >   const SWord64 s13 = s0 >> 8;
--- >   const SWord64 s14 = 0x00000000000000ffULL & s13;
--- >   const SWord8  s15 = table0[s14];
--- >   const SWord8  s16 = s12 + s15;
--- >   const SWord64 s17 = s13 >> 8;
--- >   const SWord64 s18 = 0x00000000000000ffULL & s17;
--- >   const SWord8  s19 = table0[s18];
--- >   const SWord8  s20 = s16 + s19;
--- >   const SWord64 s21 = s17 >> 8;
--- >   const SWord64 s22 = 0x00000000000000ffULL & s21;
--- >   const SWord8  s23 = table0[s22];
--- >   const SWord8  s24 = s20 + s23;
--- >   const SWord64 s25 = s21 >> 8;
--- >   const SWord64 s26 = 0x00000000000000ffULL & s25;
--- >   const SWord8  s27 = table0[s26];
--- >   const SWord8  s28 = s24 + s27;
--- >   const SWord64 s29 = s25 >> 8;
--- >   const SWord64 s30 = 0x00000000000000ffULL & s29;
--- >   const SWord8  s31 = table0[s30];
--- >   const SWord8  s32 = s28 + s31;
--- >   const SWord64 s33 = s29 >> 8;
--- >   const SWord64 s34 = 0x00000000000000ffULL & s33;
--- >   const SWord8  s35 = table0[s34];
--- >   const SWord8  s36 = s32 + s35;
--- >   const SWord64 s37 = s33 >> 8;
--- >   const SWord64 s38 = 0x00000000000000ffULL & s37;
--- >   const SWord8  s39 = table0[s38];
--- >   const SWord8  s40 = s36 + s39;
--- >   
--- >   return s40;
--- > }
---
--- SBV will also generate a driver program for test purposes. The driver will call
--- the generated function with random values. (It is also possible to instruct SBV
--- to use prescribed values, see the function `compileToC''.)
---
--- > /* Example driver program for popCount. */
--- > /* Automatically generated by SBV. Edit as you see fit! */
--- > 
--- > #include <inttypes.h>
--- > #include <stdint.h>
--- > #include <stdio.h>
--- > #include "popCount.h"
--- > 
--- > int main(void)
--- > {
--- >   const SWord8 __result = popCount(0x000000007016b176ULL);
--- >   
--- >   printf("popCount(0x000000007016b176ULL) = %"PRIu8"\n", __result);
--- >   
--- >   return 0;
--- > }
---
--- And a @Makefile@ to simplify compilation:
+-- Below is the generated header file for `popCountFast`:
 --
--- > # Makefile for popCount. Automatically generated by SBV. Do not edit!
--- > 
--- > # include any user-defined .mk file in the current directory.
--- > -include *.mk
--- > 
--- > CC=gcc
--- > CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
--- > 
--- > all: popCount_driver
--- > 
--- > popCount.o: popCount.c popCount.h
--- > 	${CC} ${CCFLAGS} -c $< -o $@
--- > 
--- > popCount_driver.o: popCount_driver.c
--- > 	${CC} ${CCFLAGS} -c $< -o $@
--- > 
--- > popCount_driver: popCount.o popCount_driver.o
--- > 	${CC} ${CCFLAGS} $^ -o $@
--- > 
--- > clean:
--- > 	rm -f *.o
--- > 
--- > veryclean: clean
--- >	rm -f popCount_driver
+-- >>> genPopCountInC
+-- == BEGIN: "Makefile" ================
+-- # Makefile for popCount. Automatically generated by SBV. Do not edit!
+-- <BLANKLINE>
+-- # include any user-defined .mk file in the current directory.
+-- -include *.mk
+-- <BLANKLINE>
+-- CC=gcc
+-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+-- <BLANKLINE>
+-- all: popCount_driver
+-- <BLANKLINE>
+-- popCount.o: popCount.c popCount.h
+-- 	${CC} ${CCFLAGS} -c $< -o $@
+-- <BLANKLINE>
+-- popCount_driver.o: popCount_driver.c
+-- 	${CC} ${CCFLAGS} -c $< -o $@
+-- <BLANKLINE>
+-- popCount_driver: popCount.o popCount_driver.o
+-- 	${CC} ${CCFLAGS} $^ -o $@
+-- <BLANKLINE>
+-- clean:
+-- 	rm -f *.o
+-- <BLANKLINE>
+-- veryclean: clean
+-- 	rm -f popCount_driver
+-- == END: "Makefile" ==================
+-- == BEGIN: "popCount.h" ================
+-- /* Header file for popCount. Automatically generated by SBV. Do not edit! */
+-- <BLANKLINE>
+-- #ifndef __popCount__HEADER_INCLUDED__
+-- #define __popCount__HEADER_INCLUDED__
+-- <BLANKLINE>
+-- #include <inttypes.h>
+-- #include <stdint.h>
+-- #include <stdbool.h>
+-- <BLANKLINE>
+-- /* The boolean type */
+-- typedef bool SBool;
+-- <BLANKLINE>
+-- /* Unsigned bit-vectors */
+-- typedef uint8_t  SWord8 ;
+-- typedef uint16_t SWord16;
+-- typedef uint32_t SWord32;
+-- typedef uint64_t SWord64;
+-- <BLANKLINE>
+-- /* Signed bit-vectors */
+-- typedef int8_t  SInt8 ;
+-- typedef int16_t SInt16;
+-- typedef int32_t SInt32;
+-- typedef int64_t SInt64;
+-- <BLANKLINE>
+-- /* Entry point prototype: */
+-- SWord8 popCount(const SWord64 x);
+-- <BLANKLINE>
+-- #endif /* __popCount__HEADER_INCLUDED__ */
+-- == END: "popCount.h" ==================
+-- == BEGIN: "popCount_driver.c" ================
+-- /* Example driver program for popCount. */
+-- /* Automatically generated by SBV. Edit as you see fit! */
+-- <BLANKLINE>
+-- #include <inttypes.h>
+-- #include <stdint.h>
+-- #include <stdbool.h>
+-- #include <stdio.h>
+-- #include "popCount.h"
+-- <BLANKLINE>
+-- int main(void)
+-- {
+--   const SWord8 __result = popCount(0x1b02e143e4f0e0e5ULL);
+-- <BLANKLINE>
+--   printf("popCount(0x1b02e143e4f0e0e5ULL) = %"PRIu8"\n", __result);
+-- <BLANKLINE>
+--   return 0;
+-- }
+-- == END: "popCount_driver.c" ==================
+-- == BEGIN: "popCount.c" ================
+-- /* File: "popCount.c". Automatically generated by SBV. Do not edit! */
+-- <BLANKLINE>
+-- #include <inttypes.h>
+-- #include <stdint.h>
+-- #include <stdbool.h>
+-- #include "popCount.h"
+-- <BLANKLINE>
+-- SWord8 popCount(const SWord64 x)
+-- {
+--   const SWord64 s0 = x;
+--   static const SWord8 table0[] = {
+--       0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3,
+--       3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4,
+--       3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2,
+--       2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5,
+--       3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5,
+--       5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3,
+--       2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4,
+--       4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
+--       3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4,
+--       4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6,
+--       5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5,
+--       5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8
+--   };
+--   const SWord64 s11 = s0 & 0x00000000000000ffULL;
+--   const SWord8  s12 = table0[s11];
+--   const SWord64 s13 = s0 >> 8;
+--   const SWord64 s14 = 0x00000000000000ffULL & s13;
+--   const SWord8  s15 = table0[s14];
+--   const SWord8  s16 = s12 + s15;
+--   const SWord64 s17 = s13 >> 8;
+--   const SWord64 s18 = 0x00000000000000ffULL & s17;
+--   const SWord8  s19 = table0[s18];
+--   const SWord8  s20 = s16 + s19;
+--   const SWord64 s21 = s17 >> 8;
+--   const SWord64 s22 = 0x00000000000000ffULL & s21;
+--   const SWord8  s23 = table0[s22];
+--   const SWord8  s24 = s20 + s23;
+--   const SWord64 s25 = s21 >> 8;
+--   const SWord64 s26 = 0x00000000000000ffULL & s25;
+--   const SWord8  s27 = table0[s26];
+--   const SWord8  s28 = s24 + s27;
+--   const SWord64 s29 = s25 >> 8;
+--   const SWord64 s30 = 0x00000000000000ffULL & s29;
+--   const SWord8  s31 = table0[s30];
+--   const SWord8  s32 = s28 + s31;
+--   const SWord64 s33 = s29 >> 8;
+--   const SWord64 s34 = 0x00000000000000ffULL & s33;
+--   const SWord8  s35 = table0[s34];
+--   const SWord8  s36 = s32 + s35;
+--   const SWord64 s37 = s33 >> 8;
+--   const SWord64 s38 = 0x00000000000000ffULL & s37;
+--   const SWord8  s39 = table0[s38];
+--   const SWord8  s40 = s36 + s39;
+-- <BLANKLINE>
+--   return s40;
+-- }
+-- == END: "popCount.c" ==================
 genPopCountInC :: IO ()
 genPopCountInC = compileToC Nothing "popCount" $ do
+        cgSetDriverValues [0x1b02e143e4f0e0e5]  -- remove this line to get a random test value
         x <- cgInput "x"
-        cgReturn $ popCount x
+        cgReturn $ popCountFast x
diff --git a/Data/SBV/Examples/Puzzles/U2Bridge.hs b/Data/SBV/Examples/Puzzles/U2Bridge.hs
--- a/Data/SBV/Examples/Puzzles/U2Bridge.hs
+++ b/Data/SBV/Examples/Puzzles/U2Bridge.hs
@@ -249,16 +249,16 @@
 -- Checking for solutions with 5 moves.
 -- Solution #1: 
 --  0 --> Edge, Bono
---  2 <-- Edge
---  4 --> Larry, Adam
--- 14 <-- Bono
+--  2 <-- Bono
+--  3 --> Larry, Adam
+-- 13 <-- Edge
 -- 15 --> Edge, Bono
 -- Total time: 17
 -- Solution #2: 
 --  0 --> Edge, Bono
---  2 <-- Bono
---  3 --> Larry, Adam
--- 13 <-- Edge
+--  2 <-- Edge
+--  4 --> Larry, Adam
+-- 14 <-- Bono
 -- 15 --> Edge, Bono
 -- Total time: 17
 -- Found: 2 solutions with 5 moves.
diff --git a/Data/SBV/Examples/Uninterpreted/Function.hs b/Data/SBV/Examples/Uninterpreted/Function.hs
--- a/Data/SBV/Examples/Uninterpreted/Function.hs
+++ b/Data/SBV/Examples/Uninterpreted/Function.hs
@@ -26,11 +26,12 @@
 thmGood x y z = x .== y+2 ==> f x z .== f (y + 2) z
 
 -- | Asserts that @f@ is commutative; which is not necessarily true!
--- Indeed, the SMT solver (Yices in this case) returns a counter-example
--- function that is not commutative. We have:
+-- Indeed, the SMT solver returns a counter-example function that is
+-- not commutative. (Note that we have to use Yices as Z3 function
+-- counterexamples are not yet supported by sbv.) We have:
 --
 --
--- >>> prove $ forAll ["x", "y"] thmBad
+-- >>> proveWith yices $ forAll ["x", "y"] thmBad
 -- Falsifiable. Counter-example:
 --   x = 0 :: SWord8
 --   y = 128 :: SWord8
diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs
--- a/Data/SBV/Provers/Prover.hs
+++ b/Data/SBV/Provers/Prover.hs
@@ -27,7 +27,7 @@
        , sat, satWith
        , allSat, allSatWith
        , isVacuous, isVacuousWith
-       , SatModel(..), Modelable(..), displayModels
+       , SatModel(..), Modelable(..), displayModels, extractModels
        , yices, z3, defaultSMTCfg
        , compileToSMTLib
        ) where
@@ -49,17 +49,20 @@
 import qualified Data.SBV.Provers.Z3    as Z3
 import Data.SBV.Utils.TDiff
 
+mkConfig :: SMTSolver -> Bool -> SMTConfig
+mkConfig s isSMTLib2 = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, smtFile = Nothing, solver = s, useSMTLib2 = isSMTLib2}
+
 -- | Default configuration for the Yices SMT Solver.
 yices :: SMTConfig
-yices = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, smtFile = Nothing, solver = Yices.yices, useSMTLib2 = False}
+yices = mkConfig Yices.yices False
 
 -- | Default configuration for the Z3 SMT solver
 z3 :: SMTConfig
-z3 = yices { solver = Z3.z3, useSMTLib2 = True }
+z3 = mkConfig Z3.z3 True
 
--- | The default solver used by SBV. This is currently set to yices.
+-- | The default solver used by SBV. This is currently set to z3.
 defaultSMTCfg :: SMTConfig
-defaultSMTCfg = yices
+defaultSMTCfg = z3
 
 -- | A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and
 -- purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The 'Symbolic'
@@ -396,7 +399,7 @@
         let msg = when (verbose config) . putStrLn . ("** " ++)
             isTiming = timing config
         msg "Starting symbolic simulation.."
-        res <- timeIf isTiming "problem construction" $ runSymbolic isSat $ forAll_ predicate >>= output
+        res <- timeIf isTiming "problem construction" $ runSymbolic isSat $ (if isSat then forSome_ else forAll_) predicate >>= output
         msg $ "Generated symbolic trace:\n" ++ show res
         msg "Translating to SMT-Lib.."
         runProofOn converter config isSat comments res
diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs
--- a/Data/SBV/Provers/Yices.hs
+++ b/Data/SBV/Provers/Yices.hs
@@ -10,10 +10,13 @@
 -- The connection to the Yices SMT solver
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PatternGuards       #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Data.SBV.Provers.Yices(yices) where
 
+import qualified Control.Exception as C
+
 import Data.Char          (isDigit)
 import Data.List          (sortBy, isPrefixOf, intercalate, transpose, partition)
 import Data.Maybe         (mapMaybe, isNothing, fromJust)
@@ -34,8 +37,8 @@
          -- , options    = ["-tc", "-smt", "-e"]   -- For Yices1
          , options    = ["-m", "-f"]  -- For Yices2
          , engine     = \cfg _isSat qinps modelMap _skolemMap pgm -> do
-                                execName <-                getEnv "SBV_YICES"          `catch` (\_ -> return (executable (solver cfg)))
-                                execOpts <- (words `fmap`  getEnv "SBV_YICES_OPTIONS") `catch` (\_ -> return (options (solver cfg)))
+                                execName <-                getEnv "SBV_YICES"          `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))
+                                execOpts <- (words `fmap`  getEnv "SBV_YICES_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))
                                 let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }
                                     script = SMTScript { scriptBody = pgm, scriptModel = Nothing }
                                 standardSolver cfg' script id (ProofError cfg) (interpretSolverOutput cfg (extractMap (map snd qinps) modelMap))
diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs
--- a/Data/SBV/Provers/Z3.hs
+++ b/Data/SBV/Provers/Z3.hs
@@ -11,9 +11,12 @@
 -----------------------------------------------------------------------------
 
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Data.SBV.Provers.Z3(z3) where
 
+import qualified Control.Exception as C
+
 import Data.Char          (isDigit, toLower)
 import Data.List          (sortBy, intercalate, isPrefixOf)
 import System.Environment (getEnv)
@@ -40,8 +43,8 @@
          , executable = "z3"
          , options    = map (optionPrefix:) ["in", "smt2"]
          , engine     = \cfg isSat qinps modelMap skolemMap pgm -> do
-                                execName <-               getEnv "SBV_Z3"          `catch` (\_ -> return (executable (solver cfg)))
-                                execOpts <- (words `fmap` getEnv "SBV_Z3_OPTIONS") `catch` (\_ -> return (options (solver cfg)))
+                                execName <-               getEnv "SBV_Z3"          `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))
+                                execOpts <- (words `fmap` getEnv "SBV_Z3_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))
                                 let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }
                                     script = SMTScript { scriptBody = "(set-option :mbqi true)\n" ++ pgm, scriptModel = Just (cont skolemMap)}
                                 standardSolver cfg' script cleanErrs (ProofError cfg) (interpretSolverOutput cfg (extractMap isSat qinps modelMap . zipWith match skolemMap))
@@ -66,8 +69,7 @@
        addTimeOut Nothing  o   = o
        addTimeOut (Just i) o
          | i < 0               = error $ "Z3: Timeout value must be non-negative, received: " ++ show i
-         | S.os == "linux"     = o ++ ["-T:" ++ show i]
-         | True                = o ++ ["/T:" ++ show i]
+         | True                = o ++ [optionPrefix : "T:" ++ show i]
 
 extractMap :: Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [String] -> SMTModel
 extractMap isSat qinps _modelMap solverLines =
diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs
--- a/Data/SBV/SMT/SMT.hs
+++ b/Data/SBV/SMT/SMT.hs
@@ -248,6 +248,11 @@
                      Right (_, b) -> Just b
                      _            -> Nothing
 
+-- | Return all the models from an 'allSat' call, similar to 'extractModel' but
+-- is suitable for the case of multiple results.
+extractModels :: SatModel a => AllSatResult -> [a]
+extractModels (AllSatResult (_, xs)) = [ms | Right (_, ms) <- map getModel xs]
+
 instance Modelable ThmResult where
   getModel    (ThmResult r) = getModel r
   modelExists (ThmResult r) = modelExists r
diff --git a/Data/SBV/Tools/ExpectedValue.hs b/Data/SBV/Tools/ExpectedValue.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Tools/ExpectedValue.hs
@@ -0,0 +1,85 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Tools.ExpectedValue
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Computing the expected value of a symbolic variable
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE PatternGuards #-}
+module Data.SBV.Tools.ExpectedValue (expectedValue, expectedValueWith) where
+
+import Control.DeepSeq (rnf)
+import System.Random   (newStdGen, StdGen)
+import Numeric
+
+import Data.SBV.BitVectors.Data
+
+-- | Generalized version of 'expectedValue', allowing the user to specify the
+-- warm-up count and the convergence factor. Maximum iteration count can also
+-- be specified, at which point convergence won't be sought. The boolean controls verbosity.
+expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double]
+expectedValueWith verbose warmupCount mbMaxIter epsilon m
+  | warmupCount < 0 || epsilon < 0
+  = error $ "SBV.expectedValue: warmup count and epsilon both must be non-negative, received: " ++ show (warmupCount, epsilon)
+  | True
+  = warmup warmupCount (repeat 0) >>= go warmupCount
+  where progress s | not verbose = return ()
+                   | True        = putStr $ "\r*** " ++ s
+        warmup :: Int -> [Integer] -> IO [Integer]
+        warmup 0 v = do progress $ "Warmup complete, performed " ++ show warmupCount ++ " rounds.\n"
+                        return v
+        warmup n v = do progress $ "Performing warmup, round: " ++ show (warmupCount - n)
+                        g <- newStdGen
+                        t <- runOnce g
+                        let v' = zipWith (+) v t
+                        rnf v' `seq` warmup (n-1) v'
+        runOnce :: StdGen -> IO [Integer]
+        runOnce g = do (_, Result _ _ _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output)
+                       let cval o = case o `lookup` cs of
+                                      Nothing -> error "SBV.expectedValue: Cannot compute expected-values in the presence of uninterpreted constants!"
+                                      Just cw -> case (cwSigned cw, cwSize cw) of
+                                                   (True,  Size Nothing ) -> error "Cannot compute expected-values for unbounded integer results."
+                                                   (False, Size (Just 1)) -> if cwToBool cw then 1 else 0
+                                                   _                      -> cwVal cw
+                       if all ((== 1) . cval) cstrs
+                          then return $ map cval os
+                          else runOnce g -- constraint not satisfied try again with the same set of constraints
+        go :: Int -> [Integer] -> IO [Double]
+        go cases curSums
+         | Just n <- mbMaxIter, n < curRound
+         = do progress "\n"
+              progress "Maximum iteration count reached, stopping.\n"
+              return curEVs
+         | True
+         = do g <- newStdGen
+              t <- runOnce g
+              let newSums  = zipWith (+) curSums t
+                  newEVs = map ev' newSums
+                  diffs  = zipWith (\x y -> abs (x - y)) newEVs curEVs
+              if all (< epsilon) diffs
+                 then do progress $ "Converges with epsilon " ++ show epsilon ++ " after " ++ show curRound ++ " rounds.\n"
+                         return newEVs
+                 else do progress $ "Tuning, round: " ++ show curRound ++ " (margin: " ++ showFFloat (Just 6) (maximum (0:diffs)) "" ++ ")"
+                         go newCases newSums
+         where curRound = cases - warmupCount
+               newCases = cases + 1
+               ev, ev' :: Integer -> Double
+               ev  x  = fromIntegral x / fromIntegral cases
+               ev' x  = fromIntegral x / fromIntegral newCases
+               curEVs = map ev curSums
+
+-- | Given a symbolic computation that produces a value, compute the
+-- expected value that value would take if this computation is run
+-- with its free variables drawn from uniform distributions of its
+-- respective values, satisfying the given constraints specified by
+-- 'constrain' and 'pConstrain' calls. This is equivalent to calling
+-- 'expectedValueWith' the following parameters: verbose, warm-up
+-- round count of @10000@, no maximum iteration count, and with
+-- convergence margin @0.0001@.
+expectedValue :: Outputtable a => Symbolic a -> IO [Double]
+expectedValue = expectedValueWith True 10000 Nothing 0.0001
diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Tools/GenTest.hs
@@ -0,0 +1,259 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Tools.GenTest
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Test generation from symbolic programs
+-----------------------------------------------------------------------------
+
+module Data.SBV.Tools.GenTest (genTest, TestVectors, getTestValues, renderTest, TestStyle(..)) where
+
+import Data.Bits     (testBit)
+import Data.Char     (isAlpha, toUpper)
+import Data.Maybe    (fromMaybe)
+import Data.List     (intercalate, groupBy)
+import System.Random
+
+import Data.SBV.BitVectors.Data
+import Data.SBV.BitVectors.PrettyNum
+
+-- | Type of test vectors (abstract)
+newtype TestVectors = TV [([CW], [CW])]
+
+-- | Retrieve the test vectors for further processing. This function
+-- is useful in cases where 'renderTest' is not sufficient and custom
+-- output (or further preprocessing) is needed.
+getTestValues :: TestVectors -> [([CW], [CW])]
+getTestValues (TV vs) = vs
+
+-- | Generate a set of concrete test values from a symbolic program. The output
+-- can be rendered as test vectors in different languages as necessary. Use the
+-- function 'output' call to indicate what fields should be in the test result.
+-- (Also see 'constrain' and 'pConstrain' for filtering acceptable test values.)
+genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors
+genTest n m = gen 0 []
+  where gen i sofar
+         | i == n = return $ TV $ reverse sofar
+         | True   = do g <- newStdGen
+                       t <- tc g
+                       gen (i+1) (t:sofar)
+        tc g = do (_, Result _ tvals _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output)
+                  let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpeted constants!") . (`lookup` cs)
+                      cond = all (cwToBool . cval) cstrs
+                  if cond
+                     then return (map snd tvals, map cval os)
+                     else tc g  -- try again, with the same set of constraints
+
+-- | Test output style
+data TestStyle = Haskell String                     -- ^ As a Haskell value with given name
+               | C       String                     -- ^ As a C array of structs with given name
+               | Forte   String Bool ([Int], [Int]) -- ^ As a Forte/Verilog value with given name.
+                                                    -- If the boolean is True then vectors are blasted big-endian, otherwise little-endian
+                                                    -- The indices are the split points on bit-vectors for input and output values
+
+-- | Render the test as a Haskell value with the given name @n@.
+renderTest :: TestStyle -> TestVectors -> String
+renderTest (Haskell n)    (TV vs) = haskell n vs
+renderTest (C n)          (TV vs) = c       n vs
+renderTest (Forte n b ss) (TV vs) = forte   n b ss vs
+
+haskell :: String -> [([CW], [CW])] -> String
+haskell vname vs = intercalate "\n" $ [ "-- Automatically generated by SBV. Do not edit!"
+                                      , ""
+                                      , "module " ++ modName ++ "(" ++ n ++ ") where"
+                                      , ""
+                                      ]
+                                   ++ imports
+                                   ++ [ n ++ " :: " ++ getType vs
+                                      , n ++ " = [ " ++ intercalate ("\n" ++ pad ++  ", ") (map mkLine vs), pad ++ "]"
+                                      ]
+  where n | null vname                 = "testVectors"
+          | not (isAlpha (head vname)) = "tv" ++ vname
+          | True                       = vname
+        imports
+          | null vs               = []
+          | needsInt && needsWord = ["import Data.Int", "import Data.Word", ""]
+          | needsInt              = ["import Data.Int", ""]
+          | needsWord             = ["import Data.Word", ""]
+          | True                  = []
+          where ((is, os):_) = vs
+                params       = is ++ os
+                needsInt     = any isSW params
+                needsWord    = any isUW params
+                isSW cw      =      cwSigned cw  && cwSize cw /= Size Nothing && cwSize cw /= Size (Just 1)
+                isUW cw      = not (cwSigned cw) && cwSize cw /= Size Nothing && cwSize cw /= Size (Just 1)
+        modName = let (f:r) = n in toUpper f : r
+        pad = replicate (length n + 3) ' '
+        getType []         = "[a]"
+        getType ((i, o):_) = "[(" ++ mapType typeOf i ++ ", " ++ mapType typeOf o ++ ")]"
+        mkLine  (i, o)     = "("  ++ mapType valOf  i ++ ", " ++ mapType valOf  o ++ ")"
+        mapType f cws = mkTuple $ map f $ groupBy (\c1 c2 -> (cwSigned c1, cwSize c1) == (cwSigned c2, cwSize c2)) cws
+        mkTuple [x] = x
+        mkTuple xs  = "(" ++ intercalate ", " xs ++ ")"
+        typeOf []    = "()"
+        typeOf [x]   = t x
+        typeOf (x:_) = "[" ++ t x ++ "]"
+        valOf  []    = "()"
+        valOf  [x]   = s x
+        valOf  xs    = "[" ++ intercalate ", " (map s xs) ++ "]"
+        t cw = case (cwSigned cw, cwSize cw) of
+                  (False, Size (Just  1)) -> "Bool"
+                  (False, Size (Just  8)) -> "Word8"
+                  (False, Size (Just 16)) -> "Word16"
+                  (False, Size (Just 32)) -> "Word32"
+                  (False, Size (Just 64)) -> "Word64"
+                  (True,  Size (Just  8)) -> "Int8"
+                  (True,  Size (Just 16)) -> "Int16"
+                  (True,  Size (Just 32)) -> "Int32"
+                  (True,  Size (Just 64)) -> "Int64"
+                  (True,  Size Nothing)   -> "Integer"
+                  _                       -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw
+        s cw = case (cwSigned cw, cwSize cw) of
+                  (False, Size (Just 1)) -> take 5 (show (cwToBool cw) ++ repeat ' ')
+                  (sgn, Size (Just sz))  -> shex  False True (sgn, sz) (cwVal cw)
+                  (_,   Size Nothing)    -> shexI False True           (cwVal cw)
+
+c :: String -> [([CW], [CW])] -> String
+c n vs = intercalate "\n" $
+              [ "/* Automatically generated by SBV. Do not edit! */"
+              , ""
+              , "#include <stdio.h>"
+              , "#include <inttypes.h>"
+              , "#include <stdint.h>"
+              , "#include <stdbool.h>"
+              , ""
+              , "/* The boolean type */"
+              , "typedef bool SBool;"
+              , ""
+              , "/* Unsigned bit-vectors */"
+              , "typedef uint8_t  SWord8 ;"
+              , "typedef uint16_t SWord16;"
+              , "typedef uint32_t SWord32;"
+              , "typedef uint64_t SWord64;"
+              , ""
+              , "/* Signed bit-vectors */"
+              , "typedef int8_t  SInt8 ;"
+              , "typedef int16_t SInt16;"
+              , "typedef int32_t SInt32;"
+              , "typedef int64_t SInt64;"
+              , ""
+              , "typedef struct {"
+              , "  struct {"
+              ]
+           ++ (if null vs then [] else zipWith (mkField "i") (fst (head vs)) [(0::Int)..])
+           ++ [ "  } input;"
+              , "  struct {"
+              ]
+           ++ (if null vs then [] else zipWith (mkField "o") (snd (head vs)) [(0::Int)..])
+           ++ [ "  } output;"
+              , "} " ++ n ++ "TestVector;"
+              , ""
+              , n ++ "TestVector " ++ n ++ "[] = {"
+              ]
+           ++ ["      " ++ intercalate "\n    , " (map mkLine vs)]
+           ++ [ "};"
+              , ""
+              , "int " ++ n ++ "Length = " ++ show (length vs) ++ ";"
+              , ""
+              , "/* Stub driver showing the test values, replace with code that uses the test vectors. */"
+              , "int main(void)"
+              , "{"
+              , "  int i;"
+              , "  for(i = 0; i < " ++ n ++ "Length; ++i)"
+              , "  {"
+              , "    " ++ outLine
+              , "  }"
+              , ""
+              , "  return 0;"
+              , "}"
+              ]
+  where mkField p cw i = "    " ++ t ++ " " ++ p ++ show i ++ ";"
+            where t = case (cwSigned cw, cwSize cw) of
+                        (False, Size (Just  1)) -> "SBool"
+                        (False, Size (Just  8)) -> "SWord8"
+                        (False, Size (Just 16)) -> "SWord16"
+                        (False, Size (Just 32)) -> "SWord32"
+                        (False, Size (Just 64)) -> "SWord64"
+                        (True,  Size (Just  8)) -> "SInt8"
+                        (True,  Size (Just 16)) -> "SInt16"
+                        (True,  Size (Just 32)) -> "SInt32"
+                        (True,  Size (Just 64)) -> "SInt64"
+                        (True,  Size Nothing)   -> error "SBV.rendertest: Unbounded integers are not supported when generating C test-cases."
+                        _                       -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw
+        mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}"
+        v cw = case (cwSigned cw, cwSize cw) of
+                  (False, Size (Just 1)) -> if cwToBool cw then "true " else "false"
+                  (sgn, Size (Just sz))  -> shex  False True (sgn, sz) (cwVal cw)
+                  (_,   Size Nothing)    -> shexI False True           (cwVal cw)
+        outLine
+          | null vs = "printf(\"\");"
+          | True    = "printf(\"%*d. " ++ fmtString ++ "\\n\", " ++ show (length (show (length vs - 1))) ++ ", i"
+                    ++ concatMap ("\n           , " ++ ) (zipWith inp is [(0::Int)..] ++ zipWith out os [(0::Int)..])
+                    ++ ");"
+          where (is, os) = head vs
+                inp cw i = mkBool cw (n ++ "[i].input.i"  ++ show i)
+                out cw i = mkBool cw (n ++ "[i].output.o" ++ show i)
+                mkBool cw s = case (cwSigned cw, cwSize cw) of
+                                (False, Size (Just 1)) -> "(" ++ s ++ " == true) ? \"true \" : \"false\""
+                                _                      -> s
+                fmtString = unwords (map fmt is) ++ " -> " ++ unwords (map fmt os)
+        fmt cw = case (cwSigned cw, cwSize cw) of
+                    (False, Size (Just  1)) -> "%s"
+                    (False, Size (Just  8)) -> "0x%02\"PRIx8\""
+                    (False, Size (Just 16)) -> "0x%04\"PRIx16\"U"
+                    (False, Size (Just 32)) -> "0x%08\"PRIx32\"UL"
+                    (False, Size (Just 64)) -> "0x%016\"PRIx64\"ULL"
+                    (True,  Size (Just  8)) -> "%\"PRId8\""
+                    (True,  Size (Just 16)) -> "%\"PRId16\""
+                    (True,  Size (Just 32)) -> "%\"PRId32\"L"
+                    (True,  Size (Just 64)) -> "%\"PRId64\"LL"
+                    (True,  Size Nothing)   -> error "SBV.rendertest: Unsupported unbounded integers for C generation."
+                    _                       -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw
+
+forte :: String -> Bool -> ([Int], [Int]) -> [([CW], [CW])] -> String
+forte vname bigEndian ss vs = intercalate "\n" $ [ "// Automatically generated by SBV. Do not edit!"
+                                             , "let " ++ n ++ " ="
+                                             , "   let c s = val [_, r] = str_split s \"'\" in " ++ blaster
+                                             ]
+                                          ++ [ "   in [ " ++ intercalate "\n      , " (map mkLine vs)
+                                             , "      ];"
+                                             ]
+  where n | null vname                 = "testVectors"
+          | not (isAlpha (head vname)) = "tv" ++ vname
+          | True                       = vname
+        blaster
+         | bigEndian = "map (\\s. s == \"1\") (explode (string_tl r))"
+         | True      = "rev (map (\\s. s == \"1\") (explode (string_tl r)))"
+        toF True  = '1'
+        toF False = '0'
+        blast cw = case (cwSigned cw, cwSize cw) of
+                     (False, Size (Just  1)) -> [toF (cwToBool cw)]
+                     (False, Size (Just  8)) -> xlt  8 (cwVal cw)
+                     (False, Size (Just 16)) -> xlt 16 (cwVal cw)
+                     (False, Size (Just 32)) -> xlt 32 (cwVal cw)
+                     (False, Size (Just 64)) -> xlt 64 (cwVal cw)
+                     (True,  Size (Just  8)) -> xlt  8 (cwVal cw)
+                     (True,  Size (Just 16)) -> xlt 16 (cwVal cw)
+                     (True,  Size (Just 32)) -> xlt 32 (cwVal cw)
+                     (True,  Size (Just 64)) -> xlt 64 (cwVal cw)
+                     (True,  Size Nothing)   -> error "SBV.rendertest: Unbounded integers are not supported when generating Forte test-cases."
+                     _                       -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw
+        xlt s v = [toF (testBit v i) | i <- [s-1, s-2 .. 0]]
+        mkLine  (i, o) = "("  ++ mkTuple (form (fst ss) (concatMap blast i)) ++ ", " ++ mkTuple (form (snd ss) (concatMap blast o)) ++ ")"
+        mkTuple []  = "()"
+        mkTuple [x] = x
+        mkTuple xs  = "(" ++ intercalate ", " xs ++ ")"
+        form []     [] = []
+        form []     bs = error $ "SBV.renderTest: Mismatched index in stream, extra " ++ show (length bs) ++ " bit(s) remain."
+        form (i:is) bs
+          | length bs < i = error $ "SBV.renderTest: Mismatched index in stream, was looking for " ++ show i ++ " bit(s), but only " ++ show i ++ " remains."
+          | i == 1        = let b:r = bs
+                                v   = if b == '1' then "T" else "F"
+                            in v : form is r
+          | True          = let (f, r) = splitAt i bs
+                                v      = "c \"" ++ show i ++ "'b" ++ f ++ "\""
+                            in v : form is r
diff --git a/Data/SBV/Tools/Optimize.hs b/Data/SBV/Tools/Optimize.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Tools/Optimize.hs
@@ -0,0 +1,108 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Tools.Optimize
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- SMT based optimization
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Data.SBV.Tools.Optimize (OptimizeOpts(..), optimize, optimizeWith, minimize, minimizeWith, maximize, maximizeWith) where
+
+import Data.Maybe (fromJust)
+
+import Data.SBV.BitVectors.Data
+import Data.SBV.BitVectors.Model (OrdSymbolic(..), EqSymbolic(..))
+import Data.SBV.Provers.Prover   (satWith, z3)
+import Data.SBV.SMT.SMT          (SatModel, getModel, SMTConfig(..))
+import Data.SBV.Utils.Boolean
+
+-- | Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable.
+-- For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions
+-- can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.
+data OptimizeOpts = Iterative  Bool   -- ^ Iteratively search. if True, it will be reporting progress
+                  | Quantified        -- ^ Use quantifiers
+
+-- | Symbolic optimization. Generalization on 'minimize' and 'maximize' that allows arbitrary
+-- cost functions and comparisons.
+optimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c)
+             => SMTConfig                         -- ^ SMT configuration
+             -> OptimizeOpts                      -- ^ Optimization options
+             -> (SBV c -> SBV c -> SBool)         -- ^ comparator
+             -> ([SBV a] -> SBV c)                -- ^ cost function
+             -> Int                               -- ^ how many elements?
+             -> ([SBV a] -> SBool)                -- ^ validity constraint
+             -> IO (Maybe [a])
+optimizeWith cfg (Iterative chatty) = iterOptimize chatty cfg
+optimizeWith cfg Quantified         = quantOptimize cfg
+
+-- | Variant of 'optimizeWith' using z3
+optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
+optimize = optimizeWith z3
+
+-- | Variant of 'maximize' allowing the use of a user specified solver.
+maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
+maximizeWith cfg opts = optimizeWith cfg opts (.>=)
+
+-- | Maximizes a cost function with respect to a constraint. Examples:
+--
+--   >>> maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))
+--   Just [9,9,9]
+maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
+maximize = maximizeWith z3
+
+-- | Variant of 'minimize' allowing the use of a user specified solver.
+minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
+minimizeWith cfg opts = optimizeWith cfg opts (.<=)
+
+-- | Minimizes a cost function with respect to a constraint. Examples:
+--
+--   >>> minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))
+--   Just [11,11,11]
+minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
+minimize = minimizeWith z3
+
+-- | Optimization using quantifiers
+quantOptimize :: (SatModel a, SymWord a) => SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
+quantOptimize cfg cmp cost n valid = do
+           m <- satWith cfg $ do xs <- mkExistVars  n
+                                 ys <- mkForallVars n
+                                 return $ valid xs &&& (valid ys ==> cost xs `cmp` cost ys)
+           case getModel m of
+              Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""
+              Right (False, a) -> return $ Just a
+              Left _           -> return Nothing
+
+-- | Optimization using iteration
+iterOptimize :: (SatModel a, Show a, SymWord a, Show c, SymWord c) =>  Bool -> SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
+iterOptimize chatty cfg cmp cost n valid = do
+        msg "Trying to find a satisfying solution."
+        m <- satWith cfg $ valid `fmap` mkExistVars n
+        case getModel m of
+          Left _ -> return Nothing
+          Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""
+          Right (False, a) -> do msg $ "First solution found: " ++ show a
+                                 let c = cost (map literal a)
+                                 msg $ "Initial value is    : " ++ show (fromJust (unliteral c))
+                                 msg "Starting iterative search."
+                                 go (1::Int) a c
+  where msg m | chatty = putStrLn $ "*** " ++ m
+              | True   = return ()
+        go i curSol curCost = do
+                msg $ "Round " ++ show i ++ " ****************************"
+                m <- satWith cfg $ do xs <- mkExistVars n
+                                      return $ let c = cost xs in valid xs &&& (c `cmp` curCost &&& c ./= curCost)
+                case getModel m of
+                  Left _ -> do msg "The current solution is optimal. Terminating search."
+                               return $ Just curSol
+                  Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""
+                  Right (False, a) -> do msg $ "Solution: " ++ show a
+                                         let c = cost (map literal a)
+                                         msg $ "Value   : " ++ show (fromJust (unliteral c))
+                                         go (i+1) a c
diff --git a/Data/SBV/Tools/Polynomial.hs b/Data/SBV/Tools/Polynomial.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Tools/Polynomial.hs
@@ -0,0 +1,238 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.BitVectors.Polynomials
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+-- Portability :  portable
+--
+-- Implementation of polynomial arithmetic
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternGuards #-}
+
+module Data.SBV.Tools.Polynomial (Polynomial(..), crc, crcBV) where
+
+import Data.Bits  (Bits(..))
+import Data.List  (genericTake)
+import Data.Maybe (fromJust)
+import Data.Word  (Word8, Word16, Word32, Word64)
+
+import Data.SBV.BitVectors.Data
+import Data.SBV.BitVectors.Model
+import Data.SBV.BitVectors.Splittable
+import Data.SBV.Utils.Boolean
+
+-- | Implements polynomial addition, multiplication, division, and modulus operations
+-- over GF(2^n).  NB. Similar to 'bvQuotRem', division by @0@ is interpreted as follows:
+--
+--     @x `pDivMod` 0 = (0, x)@
+--
+-- for all @x@ (including @0@)
+--
+-- Minimal complete definiton: 'pMult', 'pDivMod', 'showPolynomial'
+class Bits a => Polynomial a where
+ -- | Given bit-positions to be set, create a polynomial
+ -- For instance
+ --
+ --     @polynomial [0, 1, 3] :: SWord8@
+ -- 
+ -- will evaluate to @11@, since it sets the bits @0@, @1@, and @3@. Mathematicans would write this polynomial
+ -- as @x^3 + x + 1@. And in fact, 'showPoly' will show it like that.
+ polynomial :: [Int] -> a
+ -- | Add two polynomials in GF(2^n)
+ pAdd  :: a -> a -> a
+ -- | Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by
+ -- the polynomial as specified by coefficients of the third argument. Note that the third
+ -- argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our
+ -- formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not
+ -- support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles,
+ -- so this should not be a problem in practice.)
+ --
+ -- Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't
+ -- fit into the resulting size.
+ pMult :: (a, a, [Int]) -> a
+ -- | Divide two polynomials in GF(2^n), see above note for division by 0
+ pDiv  :: a -> a -> a
+ -- | Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0
+ pMod  :: a -> a -> a
+ -- | Division and modulus packed together
+ pDivMod :: a -> a -> (a, a)
+ -- | Display a polynomial like a mathematician would (over the monomial @x@), with a type
+ showPoly :: a -> String
+ -- | Display a polynomial like a mathematician would (over the monomial @x@), the first argument
+ -- controls if the final type is shown as well.
+ showPolynomial :: Bool -> a -> String
+
+ -- defaults.. Minumum complete definition: pMult, pDivMod, showPolynomial
+ polynomial = foldr (flip setBit) 0
+ pAdd       = xor
+ pDiv x y   = fst (pDivMod x y)
+ pMod x y   = snd (pDivMod x y)
+ showPoly   = showPolynomial False
+
+
+instance Polynomial Word8   where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}
+instance Polynomial Word16  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}
+instance Polynomial Word32  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}
+instance Polynomial Word64  where {showPolynomial   = sp;           pMult = lift polyMult; pDivMod = liftC polyDivMod}
+instance Polynomial SWord8  where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}
+instance Polynomial SWord16 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}
+instance Polynomial SWord32 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}
+instance Polynomial SWord64 where {showPolynomial b = liftS (sp b); pMult = polyMult;      pDivMod = polyDivMod}
+
+lift :: SymWord a => ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
+lift f (x, y, z) = fromJust $ unliteral $ f (literal x, literal y, z)
+liftC :: SymWord a => (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
+liftC f x y = let (a, b) = f (literal x) (literal y) in (fromJust (unliteral a), fromJust (unliteral b))
+liftS :: SymWord a => (a -> String) -> SBV a -> String
+liftS f s
+  | Just x <- unliteral s = f x
+  | True                  = show s
+
+-- | Pretty print as a polynomial
+sp :: Bits a => Bool -> a -> String
+sp st a
+ | null cs = '0' : t
+ | True    = foldr (\x y -> sh x ++ " + " ++ y) (sh (last cs)) (init cs) ++ t
+ where t | st   = " :: GF(2^" ++ show n ++ ")"
+         | True = ""
+       n  = bitSize a
+       is = [n-1, n-2 .. 0]
+       cs = map fst $ filter snd $ zip is (map (testBit a) is)
+       sh 0 = "1"
+       sh 1 = "x"
+       sh i = "x^" ++ show i
+
+-- | Add two polynomials
+addPoly :: [SBool] -> [SBool] -> [SBool]
+addPoly xs    []      = xs
+addPoly []    ys      = ys
+addPoly (x:xs) (y:ys) = x <+> y : addPoly xs ys
+
+ites :: SBool -> [SBool] -> [SBool] -> [SBool]
+ites s xs ys
+ | Just t <- unliteral s
+ = if t then xs else ys
+ | True
+ = go xs ys
+ where go [] []         = []
+       go []     (b:bs) = ite s false b : go [] bs
+       go (a:as) []     = ite s a false : go as []
+       go (a:as) (b:bs) = ite s a b : go as bs
+
+-- | Multiply two polynomials and reduce by the third (concrete) irreducible, given by its coefficients.
+-- See the remarks for the 'pMult' function for this design choice
+polyMult :: (Bits a, SymWord a, FromBits (SBV a)) => (SBV a, SBV a, [Int]) -> SBV a
+polyMult (x, y, red)
+  | isInfPrec x
+  = error $ "SBV.polyMult: Received infinite precision value: " ++ show x
+  | True
+  = fromBitsLE $ genericTake sz $ r ++ repeat false
+  where (_, r) = mdp ms rs
+        ms = genericTake (2*sz) $ mul (blastLE x) (blastLE y) [] ++ repeat false
+        rs = genericTake (2*sz) $ [if i `elem` red then true else false |  i <- [0 .. foldr max 0 red] ] ++ repeat false
+        sz = intSizeOf x
+        mul _  []     ps = ps
+        mul as (b:bs) ps = mul (false:as) bs (ites b (as `addPoly` ps) ps)
+
+polyDivMod :: (Bits a, SymWord a, FromBits (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
+polyDivMod x y
+   | isInfPrec x
+   = error $ "SBV.polyDivMod: Received infinite precision value: " ++ show x
+   | True
+   = ite (y .== 0) (0, x) (adjust d, adjust r)
+   where adjust xs = fromBitsLE $ genericTake sz $ xs ++ repeat false
+         sz        = intSizeOf x
+         (d, r)    = mdp (blastLE x) (blastLE y)
+
+-- conservative over-approximation of the degree
+degree :: [SBool] -> Int
+degree xs = walk (length xs - 1) $ reverse xs
+  where walk n []     = n
+        walk n (b:bs)
+         | Just t <- unliteral b
+         = if t then n else walk (n-1) bs
+         | True
+         = n -- over-estimate
+
+mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
+mdp xs ys = go (length ys - 1) (reverse ys)
+  where degTop  = degree xs
+        go _ []     = error "SBV.Polynomial.mdp: Impossible happened; exhausted ys before hitting 0"
+        go n (b:bs)
+         | n == 0   = (reverse qs, rs)
+         | True     = let (rqs, rrs) = go (n-1) bs
+                      in (ites b (reverse qs) rqs, ites b rs rrs)
+         where degQuot = degTop - n
+               ys' = replicate degQuot false ++ ys
+               (qs, rs) = divx (degQuot+1) degTop xs ys'
+
+-- return the element at index i; if not enough elements, return false
+-- N.B. equivalent to '(xs ++ repeat false) !! i', but more efficient
+idx :: [SBool] -> Int -> SBool
+idx []     _ = false
+idx (x:_)  0 = x
+idx (_:xs) i = idx xs (i-1)
+
+divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
+divx n _ xs _ | n <= 0 = ([], xs)
+divx n i xs ys'        = (q:qs, rs)
+  where q        = xs `idx` i
+        xs'      = ites q (xs `addPoly` ys') xs
+        (qs, rs) = divx (n-1) (i-1) xs' (tail ys')
+
+-- | Compute CRCs over bit-vectors. The call @crcBV n m p@ computes
+-- the CRC of the message @m@ with respect to polynomial @p@. The
+-- inputs are assumed to be blasted big-endian. The number
+-- @n@ specifies how many bits of CRC is needed. Note that @n@
+-- is actually the degree of the polynomial @p@, and thus it seems
+-- redundant to pass it in. However, in a typical proof context,
+-- the polynomial can be symbolic, so we cannot compute the degree
+-- easily. While this can be worked-around by generating code that
+-- accounts for all possible degrees, the resulting code would
+-- be unnecessarily big and complicated, and much harder to reason
+-- with. (Also note that a CRC is just the remainder from the
+-- polynomial division, but this routine is much faster in practice.)
+--
+-- NB. The @n@th bit of the polynomial @p@ /must/ be set for the CRC
+-- to be computed correctly. Note that the polynomial argument 'p' will
+-- not even have this bit present most of the time, as it will typically
+-- contain bits @0@ through @n-1@ as usual in the CRC literature. The higher
+-- order @n@th bit is simply assumed to be set, as it does not make
+-- sense to use a polynomial of a lesser degree. This is usually not a problem
+-- since CRC polynomials are designed and expressed this way.
+--
+-- NB. The literature on CRC's has many variants on how CRC's are computed.
+-- We follow the painless guide (<http://www.ross.net/crc/download/crc_v3.txt>)
+-- and compute the CRC as follows:
+--
+--     * Extend the message 'm' by adding 'n' 0 bits on the right
+--
+--     * Divide the polynomial thus obtained by the 'p'
+--
+--     * The remainder is the CRC value.
+--
+-- There are many variants on final XOR's, reversed polynomials etc., so
+-- it is essential to double check you use the correct /algorithm/.
+crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
+crcBV n m p = take n $ go (replicate n false) (m ++ replicate n false)
+  where mask = drop (length p - n) p
+        go c []     = c
+        go c (b:bs) = go next bs
+          where c' = drop 1 c ++ [b]
+                next = ite (head c) (zipWith (<+>) c' mask) c'
+
+-- | Compute CRC's over polynomials, i.e., symbolic words. The first
+-- 'Int' argument plays the same role as the one in the 'crcBV' function.
+crc :: (FromBits (SBV a), FromBits (SBV b), Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b
+crc n m p
+  | isInfPrec m || isInfPrec p
+  = error $ "SBV.crc: Received an infinite precision value: " ++ show (m, p)
+  | True
+  = fromBitsBE $ replicate (sz - n) false ++ crcBV n (blastBE m) (blastBE p)
+  where sz = intSizeOf p
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 SBV: A library for Symbolic Bitvectors
 
-Copyright (c) 2010-2011, Levent Erkok (erkokl@gmail.com)
+Copyright (c) 2010-2012, Levent Erkok (erkokl@gmail.com)
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
diff --git a/README b/README
--- a/README
+++ b/README
@@ -62,7 +62,8 @@
   - used in synthesis (the `sat` function with existentials)
   - optimized with respect to cost functions (the 'optimize', 'maximize', and 'minimize' functions)
   - quick-checked
-  - used in concrete test case generation (the 'genTest' function)
+  - used in concrete test case generation (the 'genTest' function), rendered as values in various
+    languages, including Haskell and C.
 
 If a predicate is not valid, `prove` will return a counterexample: An 
 assignment to inputs such that the predicate fails. The `sat` function will
@@ -79,25 +80,25 @@
 
 The SBV library is designed to work with any SMT-Lib compliant SMT-solver, although integration with
 individual solvers require some library work.
-Currently, we fully support the [Yices](http://yices.csl.sri.com) SMT solver from SRI,
-and the [Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/)
-SMT solver from Microsoft.
+Currently, we fully support 
+the [Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) SMT solver from Microsoft,
+and 
+the [Yices](http://yices.csl.sri.com) SMT solver from SRI.
 Both solvers are available for Windows, Linux, and Mac OSX.
 
 Prerequisites
 =============
-You **should** [download](http://yices.csl.sri.com/download-yices2.shtml)
-and install Yices (version 2.X) on your machine, and
-make sure the "yices" executable is in your path before using the sbv library,
-as it is the current default solver. Alternatively, you can specify the location
-of yices executable in the environment variable `SBV_YICES` and the options to yices
-in `SBV_YICES_OPTIONS`. The default for the latter is `"-m -f"`.
+You **should** have at least one of 
+Z3 [(download)](http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html), or
+Yices [(download)](http://yices.csl.sri.com/download-yices2.shtml) (version 2.X) 
+installed on your machine, preferably both. Note that z3 is the default solver used by 'sat',
+'allSat', 'prove', etc. commands. To use "yices", use the 'satWith', 'proveWith', 'allSatWith' variants.
 
-SBV can also use Microsoft's Z3 SMT solver as a
-backend [(download)](http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html).
-The environment variables `SBV_Z3` and `SBV_Z3_OPTIONS` can be used for choosing executable location
-and custom options.  The default for the latter is `"/in /smt2"` on Windows and `"-in -smt2"`
-on Mac and Linux. You should download Z3 version 3.2 or later.
+Make sure the executables for the solvers are in your path. Alternatively, you can specify the location
+of the yices executable in the environment variable `SBV_YICES` and the options to yices in `SBV_YICES_OPTIONS`.
+(The default for the latter is `"-m -f"`). Similarly the environment variables `SBV_Z3` and `SBV_Z3_OPTIONS` can
+be used for choosing executable location and custom options for Z3.  (The default for the latter is
+`"/in /smt2"` on Windows and `"-in -smt2"` on Mac and Linux. You should use Z3 version 3.2 or later.)
 
 Examples
 =========
diff --git a/RELEASENOTES b/RELEASENOTES
--- a/RELEASENOTES
+++ b/RELEASENOTES
@@ -1,6 +1,33 @@
 Hackage: <http://hackage.haskell.org/package/sbv>
 GitHub:  <http://github.com/LeventErkok/sbv>
 
+Latest Hackage released version: 1.0
+
+======================================================================
+Version 1.0, 2012-02-13
+
+ Library:
+  * Z3 is now the "default" SMT solver. Yices is still available, but
+    has to be specifically selected. (Use satWith, allSatWith, proveWith, etc.)
+  * Better handling of the pConstrain probability threshold for test
+    case generation and quickCheck purposes.
+  * Add 'renderTest', which accompanies 'genTest' to render test
+    vectors as Haskell/C/Forte program segments.
+  * Add 'expectedValue' which can compute the expected value of
+    a symbolic value under the given constraints. Useful for statistical
+    analysis and probability computations.
+  * When saturating provable values, use forAll_ for proofs and forSome_
+    for sat/allSat. (Previously we were allways using forAll_, which is
+    not incorrect but less intuitive.)
+  * add function:
+      extractModels :: SatModel a => AllSatResult -> [a]
+    which simplifies accessing allSat results greatly.
+ Code-generation:
+  * add "cgGenerateMakefile" which allows the user to choose if SBV
+    should generate a Makefile. (default: True)
+ Other
+  * Changes to make it compile with GHC 7.4.1.
+
 ======================================================================
 Version 0.9.24, 2011-12-28
 
diff --git a/SBVUnitTest/GoldFiles/U2Bridge.gold b/SBVUnitTest/GoldFiles/U2Bridge.gold
--- a/SBVUnitTest/GoldFiles/U2Bridge.gold
+++ b/SBVUnitTest/GoldFiles/U2Bridge.gold
@@ -3,13 +3,13 @@
   s1 = 1 :: SWord8
   s2 = 0 :: SWord8
   s3 = True
-  s4 = 1 :: SWord8
+  s4 = 0 :: SWord8
   s5 = 0 :: SWord8
   s6 = False
   s7 = 3 :: SWord8
   s8 = 2 :: SWord8
   s9 = True
-  s10 = 0 :: SWord8
+  s10 = 1 :: SWord8
   s11 = 0 :: SWord8
   s12 = False
   s13 = 1 :: SWord8
diff --git a/SBVUnitTest/GoldFiles/addSub.gold b/SBVUnitTest/GoldFiles/addSub.gold
--- a/SBVUnitTest/GoldFiles/addSub.gold
+++ b/SBVUnitTest/GoldFiles/addSub.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -58,6 +61,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "addSub.h"
 
@@ -65,9 +69,9 @@
 {
   SWord8 sum;
   SWord8 dif;
-  
+
   addSub(76, 92, &sum, &dif);
-  
+
   printf("addSub(76, 92, &sum, &dif) ->\n");
   printf("  sum = %"PRIu8"\n", sum);
   printf("  dif = %"PRIu8"\n", dif);
@@ -80,6 +84,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "addSub.h"
 
 void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
@@ -89,7 +94,7 @@
   const SWord8 s1 = y;
   const SWord8 s2 = s0 + s1;
   const SWord8 s3 = s0 - s1;
-  
+
   *sum = s2;
   *dif = s3;
 }
diff --git a/SBVUnitTest/GoldFiles/aes128Dec.gold b/SBVUnitTest/GoldFiles/aes128Dec.gold
--- a/SBVUnitTest/GoldFiles/aes128Dec.gold
+++ b/SBVUnitTest/GoldFiles/aes128Dec.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,6 +60,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "aes128Dec.h"
 
@@ -65,25 +69,25 @@
   const SWord32 pt[4] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array pt:\n");
   int pt_ctr;
   for(pt_ctr = 0; pt_ctr < 4 ; ++pt_ctr)
     printf("  pt[%d] = 0x%08"PRIx32"UL\n", pt_ctr ,pt[pt_ctr]);
-  
+
   const SWord32 key[4] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array key:\n");
   int key_ctr;
   for(key_ctr = 0; key_ctr < 4 ; ++key_ctr)
     printf("  key[%d] = 0x%08"PRIx32"UL\n", key_ctr ,key[key_ctr]);
-  
+
   SWord32 ct[4];
-  
+
   aes128Dec(pt, key, ct);
-  
+
   printf("aes128Dec(pt, key, ct) ->\n");
   int ct_ctr;
   for(ct_ctr = 0; ct_ctr < 4 ; ++ct_ctr)
@@ -97,6 +101,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "aes128Dec.h"
 
 void aes128Dec(const SWord32 *pt, const SWord32 *key, SWord32 *ct)
@@ -2591,7 +2596,7 @@
   const SWord16 s3368 = (((SWord16) s3365) << 8) | ((SWord16) s3367);
   const SWord32 s3369 = (((SWord32) s3363) << 16) | ((SWord32) s3368);
   const SWord32 s3370 = s7 ^ s3369;
-  
+
   ct[0] = s3330;
   ct[1] = s3344;
   ct[2] = s3358;
diff --git a/SBVUnitTest/GoldFiles/aes128Enc.gold b/SBVUnitTest/GoldFiles/aes128Enc.gold
--- a/SBVUnitTest/GoldFiles/aes128Enc.gold
+++ b/SBVUnitTest/GoldFiles/aes128Enc.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,6 +60,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "aes128Enc.h"
 
@@ -65,25 +69,25 @@
   const SWord32 pt[4] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array pt:\n");
   int pt_ctr;
   for(pt_ctr = 0; pt_ctr < 4 ; ++pt_ctr)
     printf("  pt[%d] = 0x%08"PRIx32"UL\n", pt_ctr ,pt[pt_ctr]);
-  
+
   const SWord32 key[4] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array key:\n");
   int key_ctr;
   for(key_ctr = 0; key_ctr < 4 ; ++key_ctr)
     printf("  key[%d] = 0x%08"PRIx32"UL\n", key_ctr ,key[key_ctr]);
-  
+
   SWord32 ct[4];
-  
+
   aes128Enc(pt, key, ct);
-  
+
   printf("aes128Enc(pt, key, ct) ->\n");
   int ct_ctr;
   for(ct_ctr = 0; ct_ctr < 4 ; ++ct_ctr)
@@ -97,6 +101,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "aes128Enc.h"
 
 void aes128Enc(const SWord32 *pt, const SWord32 *key, SWord32 *ct)
@@ -1149,7 +1154,7 @@
   const SWord32 s2036 = (((SWord32) s2030) << 16) | ((SWord32) s2035);
   const SWord32 s2037 = s1972 ^ s2024;
   const SWord32 s2038 = s2036 ^ s2037;
-  
+
   ct[0] = s1995;
   ct[1] = s2010;
   ct[2] = s2025;
diff --git a/SBVUnitTest/GoldFiles/aes128Lib.gold b/SBVUnitTest/GoldFiles/aes128Lib.gold
--- a/SBVUnitTest/GoldFiles/aes128Lib.gold
+++ b/SBVUnitTest/GoldFiles/aes128Lib.gold
@@ -3,6 +3,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "aes128Lib.h"
 
 void aes128KeySchedule(const SWord32 *key, SWord32 *encKS,
@@ -1644,7 +1645,7 @@
   const SWord8  s1779 = s1773 ^ s1778;
   const SWord16 s1780 = (((SWord16) s1772) << 8) | ((SWord16) s1779);
   const SWord32 s1781 = (((SWord32) s1765) << 16) | ((SWord32) s1780);
-  
+
   encKS[0] = s0;
   encKS[1] = s1;
   encKS[2] = s2;
@@ -1740,6 +1741,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "aes128Lib.h"
 
 void aes128BlockEncrypt(const SWord32 *pt, const SWord32 *xkey,
@@ -2643,7 +2645,7 @@
   const SWord16 s1886 = (((SWord16) s1883) << 8) | ((SWord16) s1885);
   const SWord32 s1887 = (((SWord32) s1881) << 16) | ((SWord32) s1886);
   const SWord32 s1888 = s47 ^ s1887;
-  
+
   ct[0] = s1848;
   ct[1] = s1862;
   ct[2] = s1876;
@@ -2655,6 +2657,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "aes128Lib.h"
 
 void aes128BlockDecrypt(const SWord32 *ct, const SWord32 *xkey,
@@ -3558,7 +3561,7 @@
   const SWord16 s1886 = (((SWord16) s1883) << 8) | ((SWord16) s1885);
   const SWord32 s1887 = (((SWord32) s1881) << 16) | ((SWord32) s1886);
   const SWord32 s1888 = s47 ^ s1887;
-  
+
   pt[0] = s1848;
   pt[1] = s1862;
   pt[2] = s1876;
@@ -3573,9 +3576,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -3603,6 +3609,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "aes128Lib.h"
 
@@ -3611,17 +3618,17 @@
   const SWord32 key[4] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array key:\n");
   int key_ctr;
   for(key_ctr = 0; key_ctr < 4 ; ++key_ctr)
     printf("  key[%d] = 0x%08"PRIx32"UL\n", key_ctr ,key[key_ctr]);
-  
+
   SWord32 encKS[44];
   SWord32 decKS[44];
-  
+
   aes128KeySchedule(key, encKS, decKS);
-  
+
   printf("aes128KeySchedule(key, encKS, decKS) ->\n");
   int encKS_ctr;
   for(encKS_ctr = 0; encKS_ctr < 44 ; ++encKS_ctr)
@@ -3636,12 +3643,12 @@
   const SWord32 pt[4] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array pt:\n");
   int pt_ctr;
   for(pt_ctr = 0; pt_ctr < 4 ; ++pt_ctr)
     printf("  pt[%d] = 0x%08"PRIx32"UL\n", pt_ctr ,pt[pt_ctr]);
-  
+
   const SWord32 xkey[44] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,
@@ -3655,16 +3662,16 @@
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array xkey:\n");
   int xkey_ctr;
   for(xkey_ctr = 0; xkey_ctr < 44 ; ++xkey_ctr)
     printf("  xkey[%d] = 0x%08"PRIx32"UL\n", xkey_ctr ,xkey[xkey_ctr]);
-  
+
   SWord32 ct[4];
-  
+
   aes128BlockEncrypt(pt, xkey, ct);
-  
+
   printf("aes128BlockEncrypt(pt, xkey, ct) ->\n");
   int ct_ctr;
   for(ct_ctr = 0; ct_ctr < 4 ; ++ct_ctr)
@@ -3676,12 +3683,12 @@
   const SWord32 ct[4] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array ct:\n");
   int ct_ctr;
   for(ct_ctr = 0; ct_ctr < 4 ; ++ct_ctr)
     printf("  ct[%d] = 0x%08"PRIx32"UL\n", ct_ctr ,ct[ct_ctr]);
-  
+
   const SWord32 xkey[44] = {
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,
@@ -3695,16 +3702,16 @@
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL,
       0x00000000UL, 0x00000000UL, 0x00000000UL, 0x00000000UL
   };
-  
+
   printf("Contents of input array xkey:\n");
   int xkey_ctr;
   for(xkey_ctr = 0; xkey_ctr < 44 ; ++xkey_ctr)
     printf("  xkey[%d] = 0x%08"PRIx32"UL\n", xkey_ctr ,xkey[xkey_ctr]);
-  
+
   SWord32 pt[4];
-  
+
   aes128BlockDecrypt(ct, xkey, pt);
-  
+
   printf("aes128BlockDecrypt(ct, xkey, pt) ->\n");
   int pt_ctr;
   for(pt_ctr = 0; pt_ctr < 4 ; ++pt_ctr)
@@ -3717,19 +3724,20 @@
   printf("** Driver run for aes128KeySchedule:\n");
   printf("====================================\n");
   aes128KeySchedule_driver();
-  
+
   printf("=====================================\n");
   printf("** Driver run for aes128BlockEncrypt:\n");
   printf("=====================================\n");
   aes128BlockEncrypt_driver();
-  
+
   printf("=====================================\n");
   printf("** Driver run for aes128BlockDecrypt:\n");
   printf("=====================================\n");
   aes128BlockDecrypt_driver();
-  
+
   return 0;
-}== END: "aes128Lib_driver.c" ==================
+}
+== END: "aes128Lib_driver.c" ==================
 == BEGIN: "Makefile" ================
 # Makefile for aes128Lib. Automatically generated by SBV. Do not edit!
 
diff --git a/SBVUnitTest/GoldFiles/cgUninterpret.gold b/SBVUnitTest/GoldFiles/cgUninterpret.gold
--- a/SBVUnitTest/GoldFiles/cgUninterpret.gold
+++ b/SBVUnitTest/GoldFiles/cgUninterpret.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,6 +60,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "tstShiftLeft.h"
 
@@ -65,15 +69,15 @@
   const SWord32 vs[3] = {
       0x00000001UL, 0x00000002UL, 0x00000003UL
   };
-  
+
   printf("Contents of input array vs:\n");
   int vs_ctr;
   for(vs_ctr = 0; vs_ctr < 3 ; ++vs_ctr)
     printf("  vs[%d] = 0x%08"PRIx32"UL\n", vs_ctr ,vs[vs_ctr]);
-  
-  
+
+
   const SWord32 __result = tstShiftLeft(vs);
-  
+
   printf("tstShiftLeft(vs) = 0x%08"PRIx32"UL\n", __result);
 
   return 0;
@@ -84,6 +88,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "tstShiftLeft.h"
 
 /* User specified custom code for "SBV_SHIFTLEFT" */
@@ -99,7 +104,7 @@
   const SWord32 s4 = /* Uninterpreted function */ SBV_SHIFTLEFT(s1,
                                                                 s2);
   const SWord32 s5 = s3 + s4;
-  
+
   return s5;
 }
 == END: "tstShiftLeft.c" ==================
diff --git a/SBVUnitTest/GoldFiles/codeGen1.gold b/SBVUnitTest/GoldFiles/codeGen1.gold
--- a/SBVUnitTest/GoldFiles/codeGen1.gold
+++ b/SBVUnitTest/GoldFiles/codeGen1.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -58,6 +61,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "foo.h"
 
@@ -80,18 +84,18 @@
       0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL,
       0x0000000000000000LL, 0x0000000000000000LL, 0x0000000000000000LL
   };
-  
+
   printf("Contents of input array xArr:\n");
   int xArr_ctr;
   for(xArr_ctr = 0; xArr_ctr < 45 ; ++xArr_ctr)
     printf("  xArr[%d] = %"PRId64"LL\n", xArr_ctr ,xArr[xArr_ctr]);
-  
+
   SWord16 z;
   SInt16 zArr[7];
   SInt64 yArr[45];
-  
+
   const SInt16 __result = foo(0x0000, xArr, &z, zArr, yArr);
-  
+
   printf("foo(0x0000, xArr, &z, zArr, yArr) = %"PRId16"\n", __result);
   printf("  z = 0x%04"PRIx16"U\n", z);
   int zArr_ctr;
@@ -109,6 +113,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "foo.h"
 
 SInt16 foo(const SInt16 x, const SInt64 *xArr, SWord16 *z,
@@ -162,7 +167,7 @@
   const SInt64 s45 = xArr[44];
   const SInt16 s48 = s0 + 0x0001;
   const SInt16 s50 = s0 * 0x0002;
-  
+
   *z = 0x0005U;
   zArr[0] = s48;
   zArr[1] = s48;
diff --git a/SBVUnitTest/GoldFiles/crcUSB5_1.gold b/SBVUnitTest/GoldFiles/crcUSB5_1.gold
--- a/SBVUnitTest/GoldFiles/crcUSB5_1.gold
+++ b/SBVUnitTest/GoldFiles/crcUSB5_1.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "crcUSB5.h"
 
 int main(void)
 {
   const SWord16 __result = crcUSB5(0xfedcU);
-  
+
   printf("crcUSB5(0xfedcU) = 0x%04"PRIx16"U\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "crcUSB5.h"
 
 SWord16 crcUSB5(const SWord16 msg)
@@ -101,77 +106,72 @@
   const SBool   s31 = 0x0000U != s30;
   const SWord16 s33 = s0 & 0x0001U;
   const SBool   s34 = 0x0000U != s33;
-  const SBool   s35 = (~s13) & 0x01U;
+  const SBool   s35 = !s13;
   const SBool   s36 = s4 ? s35 : s13;
-  const SBool   s37 = (~s16) & 0x01U;
+  const SBool   s37 = !s16;
   const SBool   s38 = s7 ? s37 : s16;
-  const SBool   s39 = (~s19) & 0x01U;
+  const SBool   s39 = !s19;
   const SBool   s40 = s4 ? s39 : s19;
-  const SBool   s41 = (~s40) & 0x01U;
+  const SBool   s41 = !s40;
   const SBool   s42 = s10 ? s41 : s40;
-  const SBool   s43 = (~s22) & 0x01U;
+  const SBool   s43 = !s22;
   const SBool   s44 = s7 ? s43 : s22;
-  const SBool   s45 = (~s44) & 0x01U;
+  const SBool   s45 = !s44;
   const SBool   s46 = s36 ? s45 : s44;
-  const SBool   s47 = (~s25) & 0x01U;
+  const SBool   s47 = !s25;
   const SBool   s48 = s10 ? s47 : s25;
-  const SBool   s49 = (~s48) & 0x01U;
+  const SBool   s49 = !s48;
   const SBool   s50 = s38 ? s49 : s48;
-  const SBool   s51 = (~s28) & 0x01U;
+  const SBool   s51 = !s28;
   const SBool   s52 = s36 ? s51 : s28;
-  const SBool   s53 = (~s52) & 0x01U;
+  const SBool   s53 = !s52;
   const SBool   s54 = s42 ? s53 : s52;
-  const SBool   s55 = (~s31) & 0x01U;
+  const SBool   s55 = !s31;
   const SBool   s56 = s38 ? s55 : s31;
-  const SBool   s57 = (~s56) & 0x01U;
+  const SBool   s57 = !s56;
   const SBool   s58 = s46 ? s57 : s56;
-  const SBool   s59 = (~s34) & 0x01U;
+  const SBool   s59 = !s34;
   const SBool   s60 = s42 ? s59 : s34;
-  const SBool   s61 = (~s60) & 0x01U;
+  const SBool   s61 = !s60;
   const SBool   s62 = s50 ? s61 : s60;
-  const SBool   s63 = s46 ? 1 : 0;
-  const SBool   s64 = (~s63) & 0x01U;
-  const SBool   s65 = s54 ? s64 : s63;
-  const SBool   s66 = s50 ? 1 : 0;
-  const SBool   s67 = (~s66) & 0x01U;
-  const SBool   s68 = s58 ? s67 : s66;
-  const SBool   s69 = s54 ? 1 : 0;
-  const SBool   s70 = (~s69) & 0x01U;
-  const SBool   s71 = s62 ? s70 : s69;
-  const SBool   s72 = s58 ? 1 : 0;
-  const SBool   s73 = s62 ? 1 : 0;
-  const SWord16 s74 = s73 ? 0x0001U : 0x0000U;
-  const SWord16 s75 = 0x0002U | s74;
-  const SWord16 s76 = s72 ? s75 : s74;
-  const SWord16 s77 = 0x0004U | s76;
-  const SWord16 s78 = s71 ? s77 : s76;
-  const SWord16 s79 = 0x0008U | s78;
-  const SWord16 s80 = s68 ? s79 : s78;
-  const SWord16 s81 = 0x0010U | s80;
-  const SWord16 s82 = s65 ? s81 : s80;
-  const SWord16 s83 = 0x0020U | s82;
-  const SWord16 s84 = s34 ? s83 : s82;
-  const SWord16 s85 = 0x0040U | s84;
-  const SWord16 s86 = s31 ? s85 : s84;
-  const SWord16 s87 = 0x0080U | s86;
-  const SWord16 s88 = s28 ? s87 : s86;
-  const SWord16 s89 = 0x0100U | s88;
-  const SWord16 s90 = s25 ? s89 : s88;
-  const SWord16 s91 = 0x0200U | s90;
-  const SWord16 s92 = s22 ? s91 : s90;
-  const SWord16 s93 = 0x0400U | s92;
-  const SWord16 s94 = s19 ? s93 : s92;
-  const SWord16 s96 = s94 | 0x0800U;
-  const SWord16 s97 = s16 ? s96 : s94;
-  const SWord16 s99 = s97 | 0x1000U;
-  const SWord16 s100 = s13 ? s99 : s97;
-  const SWord16 s102 = s100 | 0x2000U;
-  const SWord16 s103 = s10 ? s102 : s100;
-  const SWord16 s105 = s103 | 0x4000U;
-  const SWord16 s106 = s7 ? s105 : s103;
-  const SWord16 s108 = s106 | 0x8000U;
-  const SWord16 s109 = s4 ? s108 : s106;
-  
-  return s109;
+  const SBool   s63 = !s46;
+  const SBool   s64 = s54 ? s63 : s46;
+  const SBool   s65 = !s50;
+  const SBool   s66 = s58 ? s65 : s50;
+  const SBool   s67 = !s54;
+  const SBool   s68 = s62 ? s67 : s54;
+  const SWord16 s69 = s62 ? 0x0001U : 0x0000U;
+  const SWord16 s70 = 0x0002U | s69;
+  const SWord16 s71 = s58 ? s70 : s69;
+  const SWord16 s72 = 0x0004U | s71;
+  const SWord16 s73 = s68 ? s72 : s71;
+  const SWord16 s74 = 0x0008U | s73;
+  const SWord16 s75 = s66 ? s74 : s73;
+  const SWord16 s76 = 0x0010U | s75;
+  const SWord16 s77 = s64 ? s76 : s75;
+  const SWord16 s78 = 0x0020U | s77;
+  const SWord16 s79 = s34 ? s78 : s77;
+  const SWord16 s80 = 0x0040U | s79;
+  const SWord16 s81 = s31 ? s80 : s79;
+  const SWord16 s82 = 0x0080U | s81;
+  const SWord16 s83 = s28 ? s82 : s81;
+  const SWord16 s84 = 0x0100U | s83;
+  const SWord16 s85 = s25 ? s84 : s83;
+  const SWord16 s86 = 0x0200U | s85;
+  const SWord16 s87 = s22 ? s86 : s85;
+  const SWord16 s88 = 0x0400U | s87;
+  const SWord16 s89 = s19 ? s88 : s87;
+  const SWord16 s91 = s89 | 0x0800U;
+  const SWord16 s92 = s16 ? s91 : s89;
+  const SWord16 s94 = s92 | 0x1000U;
+  const SWord16 s95 = s13 ? s94 : s92;
+  const SWord16 s97 = s95 | 0x2000U;
+  const SWord16 s98 = s10 ? s97 : s95;
+  const SWord16 s100 = s98 | 0x4000U;
+  const SWord16 s101 = s7 ? s100 : s98;
+  const SWord16 s103 = s101 | 0x8000U;
+  const SWord16 s104 = s4 ? s103 : s101;
+
+  return s104;
 }
 == END: "crcUSB5.c" ==================
diff --git a/SBVUnitTest/GoldFiles/crcUSB5_2.gold b/SBVUnitTest/GoldFiles/crcUSB5_2.gold
--- a/SBVUnitTest/GoldFiles/crcUSB5_2.gold
+++ b/SBVUnitTest/GoldFiles/crcUSB5_2.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "crcUSB5.h"
 
 int main(void)
 {
   const SWord16 __result = crcUSB5(0xfedcU);
-  
+
   printf("crcUSB5(0xfedcU) = 0x%04"PRIx16"U\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "crcUSB5.h"
 
 SWord16 crcUSB5(const SWord16 msg)
@@ -88,95 +93,95 @@
   const SBool   s11 = 0x0000U != s10;
   const SWord16 s13 = s1 & 0x1000U;
   const SBool   s14 = 0x0000U != s13;
-  const SBool   s15 = (~s14) & 0x01U;
+  const SBool   s15 = !s14;
   const SBool   s16 = s5 ? s15 : s14;
   const SWord16 s18 = s1 & 0x0800U;
   const SBool   s19 = 0x0000U != s18;
-  const SBool   s20 = (~s19) & 0x01U;
+  const SBool   s20 = !s19;
   const SBool   s21 = s8 ? s20 : s19;
   const SWord16 s23 = s1 & 0x0400U;
   const SBool   s24 = 0x0000U != s23;
-  const SBool   s25 = (~s24) & 0x01U;
+  const SBool   s25 = !s24;
   const SBool   s26 = s5 ? s25 : s24;
-  const SBool   s27 = (~s26) & 0x01U;
+  const SBool   s27 = !s26;
   const SBool   s28 = s11 ? s27 : s26;
   const SWord16 s30 = s1 & 0x0200U;
   const SBool   s31 = 0x0000U != s30;
-  const SBool   s32 = (~s31) & 0x01U;
+  const SBool   s32 = !s31;
   const SBool   s33 = s8 ? s32 : s31;
-  const SBool   s34 = (~s33) & 0x01U;
+  const SBool   s34 = !s33;
   const SBool   s35 = s16 ? s34 : s33;
   const SWord16 s37 = s1 & 0x0100U;
   const SBool   s38 = 0x0000U != s37;
-  const SBool   s39 = (~s38) & 0x01U;
+  const SBool   s39 = !s38;
   const SBool   s40 = s11 ? s39 : s38;
-  const SBool   s41 = (~s40) & 0x01U;
+  const SBool   s41 = !s40;
   const SBool   s42 = s21 ? s41 : s40;
   const SWord16 s44 = s1 & 0x0080U;
   const SBool   s45 = 0x0000U != s44;
-  const SBool   s46 = (~s45) & 0x01U;
+  const SBool   s46 = !s45;
   const SBool   s47 = s16 ? s46 : s45;
-  const SBool   s48 = (~s47) & 0x01U;
+  const SBool   s48 = !s47;
   const SBool   s49 = s28 ? s48 : s47;
   const SWord16 s51 = s1 & 0x0040U;
   const SBool   s52 = 0x0000U != s51;
-  const SBool   s53 = (~s52) & 0x01U;
+  const SBool   s53 = !s52;
   const SBool   s54 = s21 ? s53 : s52;
-  const SBool   s55 = (~s54) & 0x01U;
+  const SBool   s55 = !s54;
   const SBool   s56 = s35 ? s55 : s54;
   const SWord16 s58 = s1 & 0x0020U;
   const SBool   s59 = 0x0000U != s58;
-  const SBool   s60 = (~s59) & 0x01U;
+  const SBool   s60 = !s59;
   const SBool   s61 = s28 ? s60 : s59;
-  const SBool   s62 = (~s61) & 0x01U;
+  const SBool   s62 = !s61;
   const SBool   s63 = s42 ? s62 : s61;
-  const SBool   s64 = (~s5) & 0x01U;
+  const SBool   s64 = !s5;
   const SBool   s65 = s5 ? s64 : s5;
-  const SBool   s66 = (~s8) & 0x01U;
+  const SBool   s66 = !s8;
   const SBool   s67 = s8 ? s66 : s8;
-  const SBool   s68 = (~s11) & 0x01U;
+  const SBool   s68 = !s11;
   const SBool   s69 = s11 ? s68 : s11;
-  const SBool   s70 = (~s16) & 0x01U;
+  const SBool   s70 = !s16;
   const SBool   s71 = s16 ? s70 : s16;
-  const SBool   s72 = (~s21) & 0x01U;
+  const SBool   s72 = !s21;
   const SBool   s73 = s21 ? s72 : s21;
-  const SBool   s74 = (~s28) & 0x01U;
+  const SBool   s74 = !s28;
   const SBool   s75 = s28 ? s74 : s28;
-  const SBool   s76 = (~s35) & 0x01U;
+  const SBool   s76 = !s35;
   const SBool   s77 = s35 ? s76 : s35;
-  const SBool   s78 = (~s42) & 0x01U;
+  const SBool   s78 = !s42;
   const SBool   s79 = s42 ? s78 : s42;
-  const SBool   s80 = (~s49) & 0x01U;
+  const SBool   s80 = !s49;
   const SBool   s81 = s49 ? s80 : s49;
-  const SBool   s82 = (~s56) & 0x01U;
+  const SBool   s82 = !s56;
   const SBool   s83 = s56 ? s82 : s56;
-  const SBool   s84 = (~s63) & 0x01U;
+  const SBool   s84 = !s63;
   const SBool   s85 = s63 ? s84 : s63;
   const SWord16 s87 = s1 & 0x0010U;
   const SBool   s88 = 0x0000U != s87;
-  const SBool   s89 = (~s88) & 0x01U;
+  const SBool   s89 = !s88;
   const SBool   s90 = s35 ? s89 : s88;
-  const SBool   s91 = (~s90) & 0x01U;
+  const SBool   s91 = !s90;
   const SBool   s92 = s49 ? s91 : s90;
   const SWord16 s94 = s1 & 0x0008U;
   const SBool   s95 = 0x0000U != s94;
-  const SBool   s96 = (~s95) & 0x01U;
+  const SBool   s96 = !s95;
   const SBool   s97 = s42 ? s96 : s95;
-  const SBool   s98 = (~s97) & 0x01U;
+  const SBool   s98 = !s97;
   const SBool   s99 = s56 ? s98 : s97;
   const SWord16 s101 = s1 & 0x0004U;
   const SBool   s102 = 0x0000U != s101;
-  const SBool   s103 = (~s102) & 0x01U;
+  const SBool   s103 = !s102;
   const SBool   s104 = s49 ? s103 : s102;
-  const SBool   s105 = (~s104) & 0x01U;
+  const SBool   s105 = !s104;
   const SBool   s106 = s63 ? s105 : s104;
   const SWord16 s108 = s1 & 0x0002U;
   const SBool   s109 = 0x0000U != s108;
-  const SBool   s110 = (~s109) & 0x01U;
+  const SBool   s110 = !s109;
   const SBool   s111 = s56 ? s110 : s109;
   const SWord16 s113 = s1 & 0x0001U;
   const SBool   s114 = 0x0000U != s113;
-  const SBool   s115 = (~s114) & 0x01U;
+  const SBool   s115 = !s114;
   const SBool   s116 = s63 ? s115 : s114;
   const SWord16 s117 = s116 ? 0x0001U : 0x0000U;
   const SWord16 s118 = 0x0002U | s117;
@@ -210,7 +215,7 @@
   const SWord16 s146 = 0x8000U | s145;
   const SWord16 s147 = s65 ? s146 : s145;
   const SWord16 s148 = s1 | s147;
-  
+
   return s148;
 }
 == END: "crcUSB5.c" ==================
diff --git a/SBVUnitTest/GoldFiles/fib1.gold b/SBVUnitTest/GoldFiles/fib1.gold
--- a/SBVUnitTest/GoldFiles/fib1.gold
+++ b/SBVUnitTest/GoldFiles/fib1.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "fib1.h"
 
 int main(void)
 {
   const SWord64 __result = fib1(0x000000000000000cULL);
-  
+
   printf("fib1(0x000000000000000cULL) = 0x%016"PRIx64"ULL\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "fib1.h"
 
 SWord64 fib1(const SWord64 n)
@@ -207,7 +212,7 @@
   const SWord64 s244 = s6 ? 0x0000000000000001ULL : s243;
   const SWord64 s245 = s4 ? 0x0000000000000001ULL : s244;
   const SWord64 s246 = s2 ? 0x0000000000000000ULL : s245;
-  
+
   return s246;
 }
 == END: "fib1.c" ==================
diff --git a/SBVUnitTest/GoldFiles/fib2.gold b/SBVUnitTest/GoldFiles/fib2.gold
--- a/SBVUnitTest/GoldFiles/fib2.gold
+++ b/SBVUnitTest/GoldFiles/fib2.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "fib2.h"
 
 int main(void)
 {
   const SWord64 __result = fib2(0x0000000000000014ULL);
-  
+
   printf("fib2(0x0000000000000014ULL) = 0x%016"PRIx64"ULL\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "fib2.h"
 
 SWord64 fib2(const SWord64 n)
@@ -114,7 +119,7 @@
       0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL
   };
   const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0];
-  
+
   return s65;
 }
 == END: "fib2.c" ==================
diff --git a/SBVUnitTest/GoldFiles/gcd.gold b/SBVUnitTest/GoldFiles/gcd.gold
--- a/SBVUnitTest/GoldFiles/gcd.gold
+++ b/SBVUnitTest/GoldFiles/gcd.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "sgcd.h"
 
 int main(void)
 {
   const SWord8 __result = sgcd(55, 154);
-  
+
   printf("sgcd(55, 154) = %"PRIu8"\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "sgcd.h"
 
 SWord8 sgcd(const SWord8 x, const SWord8 y)
@@ -126,7 +131,7 @@
   const SWord8 s46 = s9 ? s5 : s45;
   const SWord8 s47 = s6 ? s1 : s46;
   const SWord8 s48 = s3 ? s0 : s47;
-  
+
   return s48;
 }
 == END: "sgcd.c" ==================
diff --git a/SBVUnitTest/GoldFiles/legato_c.gold b/SBVUnitTest/GoldFiles/legato_c.gold
--- a/SBVUnitTest/GoldFiles/legato_c.gold
+++ b/SBVUnitTest/GoldFiles/legato_c.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -58,6 +61,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "legatoMult.h"
 
@@ -65,9 +69,9 @@
 {
   SWord8 hi;
   SWord8 lo;
-  
+
   legatoMult(87, 92, &hi, &lo);
-  
+
   printf("legatoMult(87, 92, &hi, &lo) ->\n");
   printf("  hi = %"PRIu8"\n", hi);
   printf("  lo = %"PRIu8"\n", lo);
@@ -80,6 +84,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "legatoMult.h"
 
 void legatoMult(const SWord8 x, const SWord8 y, SWord8 *hi,
@@ -89,22 +94,22 @@
   const SWord8 s1 = y;
   const SWord8 s3 = s0 & 1;
   const SBool  s5 = s3 != 0;
-  const SBool  s6 = 0 == s5;
+  const SBool  s6 = false == s5;
   const SWord8 s7 = (s0 >> 1) | (s0 << 7);
   const SWord8 s9 = s7 & 127;
   const SWord8 s10 = 1 & s9;
   const SBool  s11 = 0 != s10;
-  const SBool  s12 = 0 == s11;
+  const SBool  s12 = false == s11;
   const SWord8 s13 = (s9 >> 1) | (s9 << 7);
   const SWord8 s14 = 127 & s13;
   const SWord8 s15 = 1 & s14;
   const SBool  s16 = 0 != s15;
-  const SBool  s17 = 0 == s16;
+  const SBool  s17 = false == s16;
   const SWord8 s18 = (s14 >> 1) | (s14 << 7);
   const SWord8 s19 = 127 & s18;
   const SWord8 s20 = 1 & s19;
   const SBool  s21 = 0 != s20;
-  const SBool  s22 = 0 == s21;
+  const SBool  s22 = false == s21;
   const SWord8 s24 = s5 ? 128 : 0;
   const SWord8 s25 = 1 & s24;
   const SBool  s26 = 0 != s25;
@@ -117,7 +122,7 @@
   const SWord8 s33 = s29 ? s31 : s32;
   const SWord8 s34 = 1 & s33;
   const SBool  s35 = 0 != s34;
-  const SBool  s36 = 0 == s35;
+  const SBool  s36 = false == s35;
   const SWord8 s37 = (s24 >> 1) | (s24 << 7);
   const SWord8 s38 = 128 | s37;
   const SWord8 s39 = 127 & s37;
@@ -136,7 +141,7 @@
   const SWord8 s52 = s48 ? s50 : s51;
   const SWord8 s53 = 1 & s52;
   const SBool  s54 = 0 != s53;
-  const SBool  s55 = 0 == s54;
+  const SBool  s55 = false == s54;
   const SWord8 s56 = (s40 >> 1) | (s40 << 7);
   const SWord8 s57 = 128 | s56;
   const SWord8 s58 = 127 & s56;
@@ -155,7 +160,7 @@
   const SWord8 s71 = s67 ? s69 : s70;
   const SWord8 s72 = 1 & s71;
   const SBool  s73 = 0 != s72;
-  const SBool  s74 = 0 == s73;
+  const SBool  s74 = false == s73;
   const SWord8 s75 = (s59 >> 1) | (s59 << 7);
   const SWord8 s76 = 128 | s75;
   const SWord8 s77 = 127 & s75;
@@ -174,7 +179,7 @@
   const SWord8 s90 = s86 ? s88 : s89;
   const SWord8 s91 = 1 & s90;
   const SBool  s92 = 0 != s91;
-  const SBool  s93 = 0 == s92;
+  const SBool  s93 = false == s92;
   const SWord8 s94 = (s78 >> 1) | (s78 << 7);
   const SWord8 s95 = 128 | s94;
   const SWord8 s96 = 127 & s94;
@@ -279,7 +284,7 @@
   const SWord8 s195 = s194 ? s88 : s89;
   const SWord8 s196 = 1 & s195;
   const SBool  s197 = 0 != s196;
-  const SBool  s198 = 0 == s197;
+  const SBool  s198 = false == s197;
   const SBool  s199 = s189 < s1;
   const SBool  s200 = s189 < s78;
   const SBool  s201 = s199 | s200;
@@ -388,7 +393,7 @@
   const SWord8 s304 = s303 ? s69 : s70;
   const SWord8 s305 = 1 & s304;
   const SBool  s306 = 0 != s305;
-  const SBool  s307 = 0 == s306;
+  const SBool  s307 = false == s306;
   const SBool  s308 = s298 < s1;
   const SBool  s309 = s298 < s59;
   const SBool  s310 = s308 | s309;
@@ -410,7 +415,7 @@
   const SWord8 s326 = s322 ? s324 : s325;
   const SWord8 s327 = 1 & s326;
   const SBool  s328 = 0 != s327;
-  const SBool  s329 = 0 == s328;
+  const SBool  s329 = false == s328;
   const SWord8 s330 = (s314 >> 1) | (s314 << 7);
   const SWord8 s331 = 128 | s330;
   const SWord8 s332 = 127 & s330;
@@ -515,7 +520,7 @@
   const SWord8 s431 = s430 ? s324 : s325;
   const SWord8 s432 = 1 & s431;
   const SBool  s433 = 0 != s432;
-  const SBool  s434 = 0 == s433;
+  const SBool  s434 = false == s433;
   const SBool  s435 = s425 < s1;
   const SBool  s436 = s425 < s314;
   const SBool  s437 = s435 | s436;
@@ -625,7 +630,7 @@
   const SWord8 s541 = s540 ? s50 : s51;
   const SWord8 s542 = 1 & s541;
   const SBool  s543 = 0 != s542;
-  const SBool  s544 = 0 == s543;
+  const SBool  s544 = false == s543;
   const SBool  s545 = s535 < s1;
   const SBool  s546 = s535 < s40;
   const SBool  s547 = s545 | s546;
@@ -647,7 +652,7 @@
   const SWord8 s563 = s559 ? s561 : s562;
   const SWord8 s564 = 1 & s563;
   const SBool  s565 = 0 != s564;
-  const SBool  s566 = 0 == s565;
+  const SBool  s566 = false == s565;
   const SWord8 s567 = (s551 >> 1) | (s551 << 7);
   const SWord8 s568 = 128 | s567;
   const SWord8 s569 = 127 & s567;
@@ -666,7 +671,7 @@
   const SWord8 s582 = s578 ? s580 : s581;
   const SWord8 s583 = 1 & s582;
   const SBool  s584 = 0 != s583;
-  const SBool  s585 = 0 == s584;
+  const SBool  s585 = false == s584;
   const SWord8 s586 = (s570 >> 1) | (s570 << 7);
   const SWord8 s587 = 128 | s586;
   const SWord8 s588 = 127 & s586;
@@ -771,7 +776,7 @@
   const SWord8 s687 = s686 ? s580 : s581;
   const SWord8 s688 = 1 & s687;
   const SBool  s689 = 0 != s688;
-  const SBool  s690 = 0 == s689;
+  const SBool  s690 = false == s689;
   const SBool  s691 = s681 < s1;
   const SBool  s692 = s681 < s570;
   const SBool  s693 = s691 | s692;
@@ -880,7 +885,7 @@
   const SWord8 s796 = s795 ? s561 : s562;
   const SWord8 s797 = 1 & s796;
   const SBool  s798 = 0 != s797;
-  const SBool  s799 = 0 == s798;
+  const SBool  s799 = false == s798;
   const SBool  s800 = s790 < s1;
   const SBool  s801 = s790 < s551;
   const SBool  s802 = s800 | s801;
@@ -902,7 +907,7 @@
   const SWord8 s818 = s814 ? s816 : s817;
   const SWord8 s819 = 1 & s818;
   const SBool  s820 = 0 != s819;
-  const SBool  s821 = 0 == s820;
+  const SBool  s821 = false == s820;
   const SWord8 s822 = (s806 >> 1) | (s806 << 7);
   const SWord8 s823 = 128 | s822;
   const SWord8 s824 = 127 & s822;
@@ -1007,7 +1012,7 @@
   const SWord8 s923 = s922 ? s816 : s817;
   const SWord8 s924 = 1 & s923;
   const SBool  s925 = 0 != s924;
-  const SBool  s926 = 0 == s925;
+  const SBool  s926 = false == s925;
   const SBool  s927 = s917 < s1;
   const SBool  s928 = s917 < s806;
   const SBool  s929 = s927 | s928;
@@ -1118,7 +1123,7 @@
   const SWord8 s1034 = s1033 ? s31 : s32;
   const SWord8 s1035 = 1 & s1034;
   const SBool  s1036 = 0 != s1035;
-  const SBool  s1037 = 0 == s1036;
+  const SBool  s1037 = false == s1036;
   const SBool  s1038 = s1028 < s1;
   const SBool  s1039 = s1028 < s24;
   const SBool  s1040 = s1038 | s1039;
@@ -1140,7 +1145,7 @@
   const SWord8 s1056 = s1052 ? s1054 : s1055;
   const SWord8 s1057 = 1 & s1056;
   const SBool  s1058 = 0 != s1057;
-  const SBool  s1059 = 0 == s1058;
+  const SBool  s1059 = false == s1058;
   const SWord8 s1060 = (s1044 >> 1) | (s1044 << 7);
   const SWord8 s1061 = 128 | s1060;
   const SWord8 s1062 = 127 & s1060;
@@ -1159,7 +1164,7 @@
   const SWord8 s1075 = s1071 ? s1073 : s1074;
   const SWord8 s1076 = 1 & s1075;
   const SBool  s1077 = 0 != s1076;
-  const SBool  s1078 = 0 == s1077;
+  const SBool  s1078 = false == s1077;
   const SWord8 s1079 = (s1063 >> 1) | (s1063 << 7);
   const SWord8 s1080 = 128 | s1079;
   const SWord8 s1081 = 127 & s1079;
@@ -1178,7 +1183,7 @@
   const SWord8 s1094 = s1090 ? s1092 : s1093;
   const SWord8 s1095 = 1 & s1094;
   const SBool  s1096 = 0 != s1095;
-  const SBool  s1097 = 0 == s1096;
+  const SBool  s1097 = false == s1096;
   const SWord8 s1098 = (s1082 >> 1) | (s1082 << 7);
   const SWord8 s1099 = 128 | s1098;
   const SWord8 s1100 = 127 & s1098;
@@ -1283,7 +1288,7 @@
   const SWord8 s1199 = s1198 ? s1092 : s1093;
   const SWord8 s1200 = 1 & s1199;
   const SBool  s1201 = 0 != s1200;
-  const SBool  s1202 = 0 == s1201;
+  const SBool  s1202 = false == s1201;
   const SBool  s1203 = s1193 < s1;
   const SBool  s1204 = s1193 < s1082;
   const SBool  s1205 = s1203 | s1204;
@@ -1392,7 +1397,7 @@
   const SWord8 s1308 = s1307 ? s1073 : s1074;
   const SWord8 s1309 = 1 & s1308;
   const SBool  s1310 = 0 != s1309;
-  const SBool  s1311 = 0 == s1310;
+  const SBool  s1311 = false == s1310;
   const SBool  s1312 = s1302 < s1;
   const SBool  s1313 = s1302 < s1063;
   const SBool  s1314 = s1312 | s1313;
@@ -1414,7 +1419,7 @@
   const SWord8 s1330 = s1326 ? s1328 : s1329;
   const SWord8 s1331 = 1 & s1330;
   const SBool  s1332 = 0 != s1331;
-  const SBool  s1333 = 0 == s1332;
+  const SBool  s1333 = false == s1332;
   const SWord8 s1334 = (s1318 >> 1) | (s1318 << 7);
   const SWord8 s1335 = 128 | s1334;
   const SWord8 s1336 = 127 & s1334;
@@ -1519,7 +1524,7 @@
   const SWord8 s1435 = s1434 ? s1328 : s1329;
   const SWord8 s1436 = 1 & s1435;
   const SBool  s1437 = 0 != s1436;
-  const SBool  s1438 = 0 == s1437;
+  const SBool  s1438 = false == s1437;
   const SBool  s1439 = s1429 < s1;
   const SBool  s1440 = s1429 < s1318;
   const SBool  s1441 = s1439 | s1440;
@@ -1629,7 +1634,7 @@
   const SWord8 s1545 = s1544 ? s1054 : s1055;
   const SWord8 s1546 = 1 & s1545;
   const SBool  s1547 = 0 != s1546;
-  const SBool  s1548 = 0 == s1547;
+  const SBool  s1548 = false == s1547;
   const SBool  s1549 = s1539 < s1;
   const SBool  s1550 = s1539 < s1044;
   const SBool  s1551 = s1549 | s1550;
@@ -1651,7 +1656,7 @@
   const SWord8 s1567 = s1563 ? s1565 : s1566;
   const SWord8 s1568 = 1 & s1567;
   const SBool  s1569 = 0 != s1568;
-  const SBool  s1570 = 0 == s1569;
+  const SBool  s1570 = false == s1569;
   const SWord8 s1571 = (s1555 >> 1) | (s1555 << 7);
   const SWord8 s1572 = 128 | s1571;
   const SWord8 s1573 = 127 & s1571;
@@ -1670,7 +1675,7 @@
   const SWord8 s1586 = s1582 ? s1584 : s1585;
   const SWord8 s1587 = 1 & s1586;
   const SBool  s1588 = 0 != s1587;
-  const SBool  s1589 = 0 == s1588;
+  const SBool  s1589 = false == s1588;
   const SWord8 s1590 = (s1574 >> 1) | (s1574 << 7);
   const SWord8 s1591 = 128 | s1590;
   const SWord8 s1592 = 127 & s1590;
@@ -1775,7 +1780,7 @@
   const SWord8 s1691 = s1690 ? s1584 : s1585;
   const SWord8 s1692 = 1 & s1691;
   const SBool  s1693 = 0 != s1692;
-  const SBool  s1694 = 0 == s1693;
+  const SBool  s1694 = false == s1693;
   const SBool  s1695 = s1685 < s1;
   const SBool  s1696 = s1685 < s1574;
   const SBool  s1697 = s1695 | s1696;
@@ -1884,7 +1889,7 @@
   const SWord8 s1800 = s1799 ? s1565 : s1566;
   const SWord8 s1801 = 1 & s1800;
   const SBool  s1802 = 0 != s1801;
-  const SBool  s1803 = 0 == s1802;
+  const SBool  s1803 = false == s1802;
   const SBool  s1804 = s1794 < s1;
   const SBool  s1805 = s1794 < s1555;
   const SBool  s1806 = s1804 | s1805;
@@ -1906,7 +1911,7 @@
   const SWord8 s1822 = s1818 ? s1820 : s1821;
   const SWord8 s1823 = 1 & s1822;
   const SBool  s1824 = 0 != s1823;
-  const SBool  s1825 = 0 == s1824;
+  const SBool  s1825 = false == s1824;
   const SWord8 s1826 = (s1810 >> 1) | (s1810 << 7);
   const SWord8 s1827 = 128 | s1826;
   const SWord8 s1828 = 127 & s1826;
@@ -2011,7 +2016,7 @@
   const SWord8 s1927 = s1926 ? s1820 : s1821;
   const SWord8 s1928 = 1 & s1927;
   const SBool  s1929 = 0 != s1928;
-  const SBool  s1930 = 0 == s1929;
+  const SBool  s1930 = false == s1929;
   const SBool  s1931 = s1921 < s1;
   const SBool  s1932 = s1921 < s1810;
   const SBool  s1933 = s1931 | s1932;
@@ -2123,7 +2128,7 @@
   const SWord8 s2039 = s2037 ? s2038 : s19;
   const SWord8 s2040 = 1 & s2039;
   const SBool  s2041 = 0 != s2040;
-  const SBool  s2042 = 0 == s2041;
+  const SBool  s2042 = false == s2041;
   const SWord8 s2043 = (s1 >> 1) | (s1 << 7);
   const SWord8 s2044 = 127 & s2043;
   const SWord8 s2045 = 1 & s2044;
@@ -2140,7 +2145,7 @@
   const SWord8 s2056 = s2052 ? s2054 : s2055;
   const SWord8 s2057 = 1 & s2056;
   const SBool  s2058 = 0 != s2057;
-  const SBool  s2059 = 0 == s2058;
+  const SBool  s2059 = false == s2058;
   const SWord8 s2060 = (s2044 >> 1) | (s2044 << 7);
   const SWord8 s2061 = 128 | s2060;
   const SWord8 s2062 = 127 & s2060;
@@ -2159,7 +2164,7 @@
   const SWord8 s2075 = s2071 ? s2073 : s2074;
   const SWord8 s2076 = 1 & s2075;
   const SBool  s2077 = 0 != s2076;
-  const SBool  s2078 = 0 == s2077;
+  const SBool  s2078 = false == s2077;
   const SWord8 s2079 = (s2063 >> 1) | (s2063 << 7);
   const SWord8 s2080 = 128 | s2079;
   const SWord8 s2081 = 127 & s2079;
@@ -2178,7 +2183,7 @@
   const SWord8 s2094 = s2090 ? s2092 : s2093;
   const SWord8 s2095 = 1 & s2094;
   const SBool  s2096 = 0 != s2095;
-  const SBool  s2097 = 0 == s2096;
+  const SBool  s2097 = false == s2096;
   const SWord8 s2098 = (s2082 >> 1) | (s2082 << 7);
   const SWord8 s2099 = 128 | s2098;
   const SWord8 s2100 = 127 & s2098;
@@ -2197,7 +2202,7 @@
   const SWord8 s2113 = s2109 ? s2111 : s2112;
   const SWord8 s2114 = 1 & s2113;
   const SBool  s2115 = 0 != s2114;
-  const SBool  s2116 = 0 == s2115;
+  const SBool  s2116 = false == s2115;
   const SWord8 s2117 = (s2101 >> 1) | (s2101 << 7);
   const SWord8 s2118 = 128 | s2117;
   const SWord8 s2119 = 127 & s2117;
@@ -2302,7 +2307,7 @@
   const SWord8 s2218 = s2217 ? s2111 : s2112;
   const SWord8 s2219 = 1 & s2218;
   const SBool  s2220 = 0 != s2219;
-  const SBool  s2221 = 0 == s2220;
+  const SBool  s2221 = false == s2220;
   const SBool  s2222 = s2212 < s1;
   const SBool  s2223 = s2212 < s2101;
   const SBool  s2224 = s2222 | s2223;
@@ -2411,7 +2416,7 @@
   const SWord8 s2327 = s2326 ? s2092 : s2093;
   const SWord8 s2328 = 1 & s2327;
   const SBool  s2329 = 0 != s2328;
-  const SBool  s2330 = 0 == s2329;
+  const SBool  s2330 = false == s2329;
   const SBool  s2331 = s2321 < s1;
   const SBool  s2332 = s2321 < s2082;
   const SBool  s2333 = s2331 | s2332;
@@ -2433,7 +2438,7 @@
   const SWord8 s2349 = s2345 ? s2347 : s2348;
   const SWord8 s2350 = 1 & s2349;
   const SBool  s2351 = 0 != s2350;
-  const SBool  s2352 = 0 == s2351;
+  const SBool  s2352 = false == s2351;
   const SWord8 s2353 = (s2337 >> 1) | (s2337 << 7);
   const SWord8 s2354 = 128 | s2353;
   const SWord8 s2355 = 127 & s2353;
@@ -2538,7 +2543,7 @@
   const SWord8 s2454 = s2453 ? s2347 : s2348;
   const SWord8 s2455 = 1 & s2454;
   const SBool  s2456 = 0 != s2455;
-  const SBool  s2457 = 0 == s2456;
+  const SBool  s2457 = false == s2456;
   const SBool  s2458 = s2448 < s1;
   const SBool  s2459 = s2448 < s2337;
   const SBool  s2460 = s2458 | s2459;
@@ -2648,7 +2653,7 @@
   const SWord8 s2564 = s2563 ? s2073 : s2074;
   const SWord8 s2565 = 1 & s2564;
   const SBool  s2566 = 0 != s2565;
-  const SBool  s2567 = 0 == s2566;
+  const SBool  s2567 = false == s2566;
   const SBool  s2568 = s2558 < s1;
   const SBool  s2569 = s2558 < s2063;
   const SBool  s2570 = s2568 | s2569;
@@ -2670,7 +2675,7 @@
   const SWord8 s2586 = s2582 ? s2584 : s2585;
   const SWord8 s2587 = 1 & s2586;
   const SBool  s2588 = 0 != s2587;
-  const SBool  s2589 = 0 == s2588;
+  const SBool  s2589 = false == s2588;
   const SWord8 s2590 = (s2574 >> 1) | (s2574 << 7);
   const SWord8 s2591 = 128 | s2590;
   const SWord8 s2592 = 127 & s2590;
@@ -2689,7 +2694,7 @@
   const SWord8 s2605 = s2601 ? s2603 : s2604;
   const SWord8 s2606 = 1 & s2605;
   const SBool  s2607 = 0 != s2606;
-  const SBool  s2608 = 0 == s2607;
+  const SBool  s2608 = false == s2607;
   const SWord8 s2609 = (s2593 >> 1) | (s2593 << 7);
   const SWord8 s2610 = 128 | s2609;
   const SWord8 s2611 = 127 & s2609;
@@ -2794,7 +2799,7 @@
   const SWord8 s2710 = s2709 ? s2603 : s2604;
   const SWord8 s2711 = 1 & s2710;
   const SBool  s2712 = 0 != s2711;
-  const SBool  s2713 = 0 == s2712;
+  const SBool  s2713 = false == s2712;
   const SBool  s2714 = s2704 < s1;
   const SBool  s2715 = s2704 < s2593;
   const SBool  s2716 = s2714 | s2715;
@@ -2903,7 +2908,7 @@
   const SWord8 s2819 = s2818 ? s2584 : s2585;
   const SWord8 s2820 = 1 & s2819;
   const SBool  s2821 = 0 != s2820;
-  const SBool  s2822 = 0 == s2821;
+  const SBool  s2822 = false == s2821;
   const SBool  s2823 = s2813 < s1;
   const SBool  s2824 = s2813 < s2574;
   const SBool  s2825 = s2823 | s2824;
@@ -2925,7 +2930,7 @@
   const SWord8 s2841 = s2837 ? s2839 : s2840;
   const SWord8 s2842 = 1 & s2841;
   const SBool  s2843 = 0 != s2842;
-  const SBool  s2844 = 0 == s2843;
+  const SBool  s2844 = false == s2843;
   const SWord8 s2845 = (s2829 >> 1) | (s2829 << 7);
   const SWord8 s2846 = 128 | s2845;
   const SWord8 s2847 = 127 & s2845;
@@ -3030,7 +3035,7 @@
   const SWord8 s2946 = s2945 ? s2839 : s2840;
   const SWord8 s2947 = 1 & s2946;
   const SBool  s2948 = 0 != s2947;
-  const SBool  s2949 = 0 == s2948;
+  const SBool  s2949 = false == s2948;
   const SBool  s2950 = s2940 < s1;
   const SBool  s2951 = s2940 < s2829;
   const SBool  s2952 = s2950 | s2951;
@@ -3141,7 +3146,7 @@
   const SWord8 s3057 = s3056 ? s2054 : s2055;
   const SWord8 s3058 = 1 & s3057;
   const SBool  s3059 = 0 != s3058;
-  const SBool  s3060 = 0 == s3059;
+  const SBool  s3060 = false == s3059;
   const SBool  s3061 = s3051 < s1;
   const SBool  s3062 = s3051 < s2044;
   const SBool  s3063 = s3061 | s3062;
@@ -3163,7 +3168,7 @@
   const SWord8 s3079 = s3075 ? s3077 : s3078;
   const SWord8 s3080 = 1 & s3079;
   const SBool  s3081 = 0 != s3080;
-  const SBool  s3082 = 0 == s3081;
+  const SBool  s3082 = false == s3081;
   const SWord8 s3083 = (s3067 >> 1) | (s3067 << 7);
   const SWord8 s3084 = 128 | s3083;
   const SWord8 s3085 = 127 & s3083;
@@ -3182,7 +3187,7 @@
   const SWord8 s3098 = s3094 ? s3096 : s3097;
   const SWord8 s3099 = 1 & s3098;
   const SBool  s3100 = 0 != s3099;
-  const SBool  s3101 = 0 == s3100;
+  const SBool  s3101 = false == s3100;
   const SWord8 s3102 = (s3086 >> 1) | (s3086 << 7);
   const SWord8 s3103 = 128 | s3102;
   const SWord8 s3104 = 127 & s3102;
@@ -3201,7 +3206,7 @@
   const SWord8 s3117 = s3113 ? s3115 : s3116;
   const SWord8 s3118 = 1 & s3117;
   const SBool  s3119 = 0 != s3118;
-  const SBool  s3120 = 0 == s3119;
+  const SBool  s3120 = false == s3119;
   const SWord8 s3121 = (s3105 >> 1) | (s3105 << 7);
   const SWord8 s3122 = 128 | s3121;
   const SWord8 s3123 = 127 & s3121;
@@ -3306,7 +3311,7 @@
   const SWord8 s3222 = s3221 ? s3115 : s3116;
   const SWord8 s3223 = 1 & s3222;
   const SBool  s3224 = 0 != s3223;
-  const SBool  s3225 = 0 == s3224;
+  const SBool  s3225 = false == s3224;
   const SBool  s3226 = s3216 < s1;
   const SBool  s3227 = s3216 < s3105;
   const SBool  s3228 = s3226 | s3227;
@@ -3415,7 +3420,7 @@
   const SWord8 s3331 = s3330 ? s3096 : s3097;
   const SWord8 s3332 = 1 & s3331;
   const SBool  s3333 = 0 != s3332;
-  const SBool  s3334 = 0 == s3333;
+  const SBool  s3334 = false == s3333;
   const SBool  s3335 = s3325 < s1;
   const SBool  s3336 = s3325 < s3086;
   const SBool  s3337 = s3335 | s3336;
@@ -3437,7 +3442,7 @@
   const SWord8 s3353 = s3349 ? s3351 : s3352;
   const SWord8 s3354 = 1 & s3353;
   const SBool  s3355 = 0 != s3354;
-  const SBool  s3356 = 0 == s3355;
+  const SBool  s3356 = false == s3355;
   const SWord8 s3357 = (s3341 >> 1) | (s3341 << 7);
   const SWord8 s3358 = 128 | s3357;
   const SWord8 s3359 = 127 & s3357;
@@ -3542,7 +3547,7 @@
   const SWord8 s3458 = s3457 ? s3351 : s3352;
   const SWord8 s3459 = 1 & s3458;
   const SBool  s3460 = 0 != s3459;
-  const SBool  s3461 = 0 == s3460;
+  const SBool  s3461 = false == s3460;
   const SBool  s3462 = s3452 < s1;
   const SBool  s3463 = s3452 < s3341;
   const SBool  s3464 = s3462 | s3463;
@@ -3652,7 +3657,7 @@
   const SWord8 s3568 = s3567 ? s3077 : s3078;
   const SWord8 s3569 = 1 & s3568;
   const SBool  s3570 = 0 != s3569;
-  const SBool  s3571 = 0 == s3570;
+  const SBool  s3571 = false == s3570;
   const SBool  s3572 = s3562 < s1;
   const SBool  s3573 = s3562 < s3067;
   const SBool  s3574 = s3572 | s3573;
@@ -3674,7 +3679,7 @@
   const SWord8 s3590 = s3586 ? s3588 : s3589;
   const SWord8 s3591 = 1 & s3590;
   const SBool  s3592 = 0 != s3591;
-  const SBool  s3593 = 0 == s3592;
+  const SBool  s3593 = false == s3592;
   const SWord8 s3594 = (s3578 >> 1) | (s3578 << 7);
   const SWord8 s3595 = 128 | s3594;
   const SWord8 s3596 = 127 & s3594;
@@ -3693,7 +3698,7 @@
   const SWord8 s3609 = s3605 ? s3607 : s3608;
   const SWord8 s3610 = 1 & s3609;
   const SBool  s3611 = 0 != s3610;
-  const SBool  s3612 = 0 == s3611;
+  const SBool  s3612 = false == s3611;
   const SWord8 s3613 = (s3597 >> 1) | (s3597 << 7);
   const SWord8 s3614 = 128 | s3613;
   const SWord8 s3615 = 127 & s3613;
@@ -3798,7 +3803,7 @@
   const SWord8 s3714 = s3713 ? s3607 : s3608;
   const SWord8 s3715 = 1 & s3714;
   const SBool  s3716 = 0 != s3715;
-  const SBool  s3717 = 0 == s3716;
+  const SBool  s3717 = false == s3716;
   const SBool  s3718 = s3708 < s1;
   const SBool  s3719 = s3708 < s3597;
   const SBool  s3720 = s3718 | s3719;
@@ -3907,7 +3912,7 @@
   const SWord8 s3823 = s3822 ? s3588 : s3589;
   const SWord8 s3824 = 1 & s3823;
   const SBool  s3825 = 0 != s3824;
-  const SBool  s3826 = 0 == s3825;
+  const SBool  s3826 = false == s3825;
   const SBool  s3827 = s3817 < s1;
   const SBool  s3828 = s3817 < s3578;
   const SBool  s3829 = s3827 | s3828;
@@ -3929,7 +3934,7 @@
   const SWord8 s3845 = s3841 ? s3843 : s3844;
   const SWord8 s3846 = 1 & s3845;
   const SBool  s3847 = 0 != s3846;
-  const SBool  s3848 = 0 == s3847;
+  const SBool  s3848 = false == s3847;
   const SWord8 s3849 = (s3833 >> 1) | (s3833 << 7);
   const SWord8 s3850 = 128 | s3849;
   const SWord8 s3851 = 127 & s3849;
@@ -4034,7 +4039,7 @@
   const SWord8 s3950 = s3949 ? s3843 : s3844;
   const SWord8 s3951 = 1 & s3950;
   const SBool  s3952 = 0 != s3951;
-  const SBool  s3953 = 0 == s3952;
+  const SBool  s3953 = false == s3952;
   const SBool  s3954 = s3944 < s1;
   const SBool  s3955 = s3944 < s3833;
   const SBool  s3956 = s3954 | s3955;
@@ -6409,7 +6414,7 @@
   const SWord8 s6325 = s17 ? s6041 : s6324;
   const SWord8 s6326 = s12 ? s5758 : s6325;
   const SWord8 s6327 = s6 ? s5191 : s6326;
-  
+
   *hi = s4056;
   *lo = s6327;
 }
diff --git a/SBVUnitTest/GoldFiles/popCount1.gold b/SBVUnitTest/GoldFiles/popCount1.gold
--- a/SBVUnitTest/GoldFiles/popCount1.gold
+++ b/SBVUnitTest/GoldFiles/popCount1.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "popCount.h"
 
 int main(void)
 {
   const SWord8 __result = popCount(0x0123456789abcdefULL);
-  
+
   printf("popCount(0x0123456789abcdefULL) = %"PRIu8"\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "popCount.h"
 
 SWord8 popCount(const SWord64 x)
@@ -123,7 +128,7 @@
   const SWord64 s38 = 0x00000000000000ffULL & s37;
   const SWord8  s39 = table0[s38];
   const SWord8  s40 = s36 + s39;
-  
+
   return s40;
 }
 == END: "popCount.c" ==================
diff --git a/SBVUnitTest/GoldFiles/popCount2.gold b/SBVUnitTest/GoldFiles/popCount2.gold
--- a/SBVUnitTest/GoldFiles/popCount2.gold
+++ b/SBVUnitTest/GoldFiles/popCount2.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "popCount.h"
 
 int main(void)
 {
   const SWord8 __result = popCount(0x0123456789abcdefULL);
-  
+
   printf("popCount(0x0123456789abcdefULL) = %"PRIu8"\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "popCount.h"
 
 SWord8 popCount(const SWord64 x)
@@ -123,7 +128,7 @@
   const SWord64 s38 = 0x00000000000000ffULL & s37;
   const SWord8  s39 = s38 >= 256 ? 0 : table0[s38];
   const SWord8  s40 = s36 + s39;
-  
+
   return s40;
 }
 == END: "popCount.c" ==================
diff --git a/SBVUnitTest/GoldFiles/selChecked.gold b/SBVUnitTest/GoldFiles/selChecked.gold
--- a/SBVUnitTest/GoldFiles/selChecked.gold
+++ b/SBVUnitTest/GoldFiles/selChecked.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "selChecked.h"
 
 int main(void)
 {
   const SWord8 __result = selChecked(65);
-  
+
   printf("selChecked(65) = %"PRIu8"\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "selChecked.h"
 
 SWord8 selChecked(const SWord8 x)
@@ -84,7 +89,7 @@
        1, s3
   };
   const SWord8 s5 = s0 >= 2 ? 3 : table0[s0];
-  
+
   return s5;
 }
 == END: "selChecked.c" ==================
diff --git a/SBVUnitTest/GoldFiles/selUnchecked.gold b/SBVUnitTest/GoldFiles/selUnchecked.gold
--- a/SBVUnitTest/GoldFiles/selUnchecked.gold
+++ b/SBVUnitTest/GoldFiles/selUnchecked.gold
@@ -32,9 +32,12 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 
+/* The boolean type */
+typedef bool SBool;
+
 /* Unsigned bit-vectors */
-typedef uint8_t  SBool  ;
 typedef uint8_t  SWord8 ;
 typedef uint16_t SWord16;
 typedef uint32_t SWord32;
@@ -57,13 +60,14 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include <stdio.h>
 #include "selUnChecked.h"
 
 int main(void)
 {
   const SWord8 __result = selUnChecked(65);
-  
+
   printf("selUnChecked(65) = %"PRIu8"\n", __result);
 
   return 0;
@@ -74,6 +78,7 @@
 
 #include <inttypes.h>
 #include <stdint.h>
+#include <stdbool.h>
 #include "selUnChecked.h"
 
 SWord8 selUnChecked(const SWord8 x)
@@ -84,7 +89,7 @@
        1, s3
   };
   const SWord8 s5 = table0[s0];
-  
+
   return s5;
 }
 == END: "selUnChecked.c" ==================
diff --git a/SBVUnitTest/SBVUnitTest.hs b/SBVUnitTest/SBVUnitTest.hs
--- a/SBVUnitTest/SBVUnitTest.hs
+++ b/SBVUnitTest/SBVUnitTest.hs
@@ -13,15 +13,12 @@
 module Main(main) where
 
 import Control.Monad        (unless, when)
-import System.Directory     (doesDirectoryExist, findExecutable)
-import System.Environment   (getArgs, getEnv)
+import System.Directory     (doesDirectoryExist)
+import System.Environment   (getArgs)
 import System.Exit          (exitWith, ExitCode(..))
 import System.FilePath      ((</>))
-import System.Process       (readProcessWithExitCode)
 import Test.HUnit           (Test(..), Counts(..), runTestTT)
 
-import Data.List            (isPrefixOf)
-import Data.SBV             (yices, SMTSolver(..), SMTConfig(..))
 import Data.Version         (showVersion)
 import SBVTest              (SBVTestSuite(..), generateGoldCheck)
 import Paths_sbv            (getDataDir, version)
@@ -135,35 +132,6 @@
                                    putStrLn "*** Cannot run test cases, exiting."
                                    exitWith $ ExitFailure 1
 
-checkYices :: IO ()
-checkYices = do ex <- getEnv "SBV_YICES" `catch` (\_ -> return (executable (solver yices)))
-                mbP <- findExecutable ex
-                case mbP of
-                  Nothing -> do putStrLn $ "*** Cannot find default SMT solver executable for " ++ nm
-                                putStrLn $ "*** Please make sure the executable " ++ show ex
-                                putStrLn   "*** is installed and is in your path."
-                                putStrLn   "*** Cannot run test cases, exiting."
-                                exitWith $ ExitFailure 1
-                  Just p  -> do putStrLn $ "*** Using solver : " ++ nm ++ " (" ++ show p ++ ")"
-                                checkYicesVersion p
- where nm = name (solver yices)
-
-checkYicesVersion :: FilePath -> IO ()
-checkYicesVersion p =
-        do (ec, yOut, _yErr) <- readProcessWithExitCode p ["-V"] ""
-           case ec of
-             ExitFailure _ -> do putStrLn "*** Cannot determine Yices version. Please install Yices version 2.X first."
-                                 exitWith $ ExitFailure 1
-             ExitSuccess   -> do let isYices1 = "1." `isPrefixOf` yOut -- crude test; might fail..
-                                 when isYices1 $ putStrLn "*** Yices version 1.X is detected. Version 2.X is strongly recommended!"
-                                 opts <- getEnv "SBV_YICES_OPTIONS" `catch` (\_ -> return (unwords (options (solver yices))))
-                                 when (isYices1 && opts /= "-tc -smt -e") $ do
-                                           putStrLn "*** Either install Yices 2.X, or set the environment variable:"
-                                           putStrLn "***     SBV_YICES_OPTIONS=\"-tc -smt -e\""
-                                           putStrLn "*** To use Yices 1.X with SBV."
-                                           putStrLn "*** However, upgrading to Yices 2.X is highly recommended!"
-                                           exitWith $ ExitFailure 1
-
 allTargets :: [String]
 allTargets = map fst testCollection
 
@@ -176,7 +144,6 @@
         do mapM_ checkTgt targets
            putStrLn $ "*** Starting SBV unit tests..\n*** Gold files at: " ++ show gd
            checkGoldDir gd
-           checkYices
            cts <- runTestTT $ TestList $ map mkTst [c | (tc, c) <- testCollection, select tc]
            decide shouldCreate cts
   where mkTst (SBVTestSuite f) = f $ generateGoldCheck gd shouldCreate
diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs
--- a/SBVUnitTest/SBVUnitTestBuildTime.hs
+++ b/SBVUnitTest/SBVUnitTestBuildTime.hs
@@ -2,4 +2,4 @@
 module SBVUnitTestBuildTime (buildTime) where
 
 buildTime :: String
-buildTime = "Wed Dec 28 00:11:15 PST 2011"
+buildTime = "Sun Feb 12 23:26:02 PST 2012"
diff --git a/SBVUnitTest/TestSuite/Basics/Arithmetic.hs b/SBVUnitTest/TestSuite/Basics/Arithmetic.hs
--- a/SBVUnitTest/TestSuite/Basics/Arithmetic.hs
+++ b/SBVUnitTest/TestSuite/Basics/Arithmetic.hs
@@ -21,25 +21,27 @@
 -- Test suite
 testSuite :: SBVTestSuite
 testSuite = mkTestSuite $ \_ -> test $
-        genBinTest "+"                (+)
-     ++ genBinTest "-"                (-)
-     ++ genBinTest "*"                (*)
-     ++ genUnTest  "negate"           negate
-     ++ genUnTest  "abs"              abs
-     ++ genUnTest  "signum"           signum
-     ++ genBinTest ".&."              (.&.)
-     ++ genBinTest ".|."              (.|.)
-     ++ genBinTest "xor"              xor
-     ++ genUnTest  "complement"       complement
-     ++ genIntTest "shift"            shift
-     ++ genIntTest "rotate"           rotate
-     ++ genIntTest "setBit"           setBit
-     ++ genIntTest "clearBit"         clearBit
-     ++ genIntTest "complementBit"    complementBit
-     ++ genIntTest "shiftL"           shiftL
-     ++ genIntTest "shiftR"           shiftR
-     ++ genIntTest "rotateL"          rotateL
-     ++ genIntTest "rotateR"          rotateR
+        genBinTest  "+"                (+)
+     ++ genBinTest  "-"                (-)
+     ++ genBinTest  "*"                (*)
+     ++ genUnTest   "negate"           negate
+     ++ genUnTest   "abs"              abs
+     ++ genUnTest   "signum"           signum
+     ++ genBinTest  ".&."              (.&.)
+     ++ genBinTest  ".|."              (.|.)
+     ++ genBinTest  "xor"              xor
+     ++ genUnTest   "complement"       complement
+     ++ genIntTest  "shift"            shift
+     ++ genIntTest  "rotate"           rotate
+     ++ genIntTestS "setBit"           setBit
+     ++ genIntTestS "clearBit"         clearBit
+     ++ genIntTestS "complementBit"    complementBit
+     ++ genIntTest  "shift"            shift
+     ++ genIntTestS "shiftL"           shiftL
+     ++ genIntTestS "shiftR"           shiftR
+     ++ genIntTest  "rotate"           rotate
+     ++ genIntTestS "rotateL"          rotateL
+     ++ genIntTestS "rotateR"          rotateR
      ++ genBlasts
      ++ genCasts
 
@@ -85,6 +87,20 @@
   where pair (t, x, y, a) b       = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)
         mkTest (t, x, y, a, b, s) = "arithmetic-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"
         is = [-10 .. 10]
+
+genIntTestS :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]
+genIntTestS nm op = map mkTest $
+        zipWith pair [("u8",  show x, show y, x `op` y) | x <- w8s,  y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw8s,  y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("s8",  show x, show y, x `op` y) | x <- i8s,  y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si8s,  y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]]              [x `op` y | x <- siUBs, y <- [0 .. 10             ]]
+  where pair (t, x, y, a) b       = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)
+        mkTest (t, x, y, a, b, s) = "arithmetic-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"
 
 genBlasts :: [Test]
 genBlasts = map mkTest $
diff --git a/SBVUnitTest/TestSuite/CodeGeneration/PopulationCount.hs b/SBVUnitTest/TestSuite/CodeGeneration/PopulationCount.hs
--- a/SBVUnitTest/TestSuite/CodeGeneration/PopulationCount.hs
+++ b/SBVUnitTest/TestSuite/CodeGeneration/PopulationCount.hs
@@ -28,4 +28,4 @@
                   cgSetDriverValues [0x0123456789ABCDEF]
                   cgPerformRTCs b
                   x <- cgInput "x"
-                  cgReturn $ popCount x
+                  cgReturn $ popCountFast x
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,5 +1,5 @@
 Name:          sbv
-Version:       0.9.24
+Version:       1.0
 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
 Synopsis:      Symbolic bit vectors: Bit-precise verification and automatic C-code generation.
 Description:   Express properties about bit-precise Haskell programs and automatically prove
@@ -46,7 +46,8 @@
                .
                  * quick-checked
                .
-                 * used in concrete test case generation (the 'genTest' function)
+                 * used in concrete test case generation (the 'genTest' function), rendered as values in various
+                   languages, including Haskell and C.
                .
                Predicates can have both existential and universal variables. Use of
                alternating quantifiers provides considerable expressive power.
@@ -126,10 +127,7 @@
                   , Data.SBV.Examples.Uninterpreted.AUF
                   , Data.SBV.Examples.Uninterpreted.Function
   Other-modules   : Data.SBV.BitVectors.Data
-                  , Data.SBV.BitVectors.GenTest
                   , Data.SBV.BitVectors.Model
-                  , Data.SBV.BitVectors.Optimize
-                  , Data.SBV.BitVectors.Polynomial
                   , Data.SBV.BitVectors.PrettyNum
                   , Data.SBV.BitVectors.SignCast
                   , Data.SBV.BitVectors.Splittable
@@ -144,6 +142,10 @@
                   , Data.SBV.Provers.SExpr
                   , Data.SBV.Provers.Yices
                   , Data.SBV.Provers.Z3
+                  , Data.SBV.Tools.ExpectedValue
+                  , Data.SBV.Tools.GenTest
+                  , Data.SBV.Tools.Optimize
+                  , Data.SBV.Tools.Polynomial
                   , Data.SBV.Utils.Boolean
                   , Data.SBV.Utils.TDiff
                   , Data.SBV.Utils.Lib