diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,8 +1,44 @@
 * Hackage: <http://hackage.haskell.org/package/sbv>
 * GitHub:  <http://leventerkok.github.com/sbv/>
 
-* Latest Hackage released version: 7.7, 2018-04-29
+* Latest Hackage released version: 7.8, 2018-05-18
 
+### Version 7.8, Released 2018-05-18
+
+  * Fix printing of min-bounds for signed 32/64 bit numbers: These
+    are tricky since C does not allow -min_value as a valid literal!
+    Instead we use the macros provided in stdint.h. Thanks to Matt
+    Peddie for reporting this corner case.
+
+  * Fix translation of the "abs" function, to make sure we use
+    the correct variant. Thanks to Matt Peddie for reporting.
+
+  * Fix handling of tables and arrays in pushed-contexts. Previously,
+    we used initializers to get table/array values stored properly.
+    However, this trick does not work if we are in a pushed-context;
+    since a pop can forget the corresponding assignments. SBV now
+    handles this corner case properly, by using tracker assertions
+    to keep track of what array values must be restored at each pop.
+    Thanks to Martin Brain on the SMTLib mailing list for the
+    suggestion. (See https://github.com/LeventErkok/sbv/issues/374
+    for details.)
+
+  * Fix corner case in ite branch equality with float/double arguments,
+    where we were previously confusing +/-0 as equal to each other.
+    Thanks to Matt Peddie for reporting.
+
+  * Add a call 'cgOverwriteFiles', which suppresses code-generation
+    prompts for overwriting files and quiets the prompts during
+    code generation. Thanks to Matt Peddie for the suggestion.
+
+  * Add support for uninterpreted function introductions in the query
+    mode. Previously, this was only allowed before the query started,
+    now we fully support uninterpreted functions in all modes.
+
+  * New example: Documentation/SBV/Examples/Puzzles/HexPuzzle.hs,
+    showing how to code cover properties using SBV, using a form
+    of bounded model checking.
+
 ### Version 7.7, Released 2018-04-29
 
   * Add support for Symbolic characters ('SChar') and strings ('SString'.)
@@ -1183,8 +1219,7 @@
 
 ### Version 2.9, 2013-01-02
 
-  * Add support for the CVC4 SMT solver from New York University and
-    the University of Iowa. <http://cvc4.cs.nyu.edu/>.
+  * Add support for the CVC4 SMT solver from Stanford: <http://cvc4.cs.stanford.edu/web/>
     NB. Z3 remains the default solver for SBV. To use CVC4, use the
     *With variants of the interface (i.e., proveWith, satWith, ..)
     by passing cvc4 as the solver argument. (Similarly, use 'yices'
diff --git a/Data/SBV.hs b/Data/SBV.hs
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -90,7 +90,7 @@
 --
 --   * ABC from University of Berkeley: <http://www.eecs.berkeley.edu/~alanmi/abc/>
 --
---   * CVC4 from New York University and University of Iowa: <http://cvc4.cs.nyu.edu/>
+--   * CVC4 from Stanford: <http://cvc4.cs.stanford.edu/web/>
 --
 --   * Boolector from Johannes Kepler University: <http://fmv.jku.at/boolector/>
 --
@@ -142,9 +142,9 @@
   -- ** Algebraic reals
   -- $algReals
   , SReal, AlgReal, sRealToSInteger
-  -- ** Strings and Regular Expressions
+  -- ** Characters, Strings and Regular Expressions
   -- $strings
-  , SString, SChar, (.++), (.!!)
+  , SChar, SString, (.++), (.!!)
   -- * Arrays of symbolic values
   , SymArray(..), SArray, SFunArray, mkSFunArray
 
@@ -702,9 +702,10 @@
 -}
 
 {- $strings
-Support for strings (intial version contributed by Joel Burget) adds support for QF_S logic,
-described here: <https://rise4fun.com/z3/tutorialcontent/sequences>. Note that this logic
-is still not part of official SMTLib (as of March 2018), so it should be considered
+Support for characters, strings, and regular expressions (intial version contributed by Joel Burget)
+adds support for QF_S logic, described here: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>
+and here: <https://rise4fun.com/z3/tutorialcontent/sequences>. Note
+that this logic is still not part of official SMTLib (as of March 2018), so it should be considered
 experimental.
 
 See "Data.SBV.Char", "Data.SBV.String", "Data.SBV.RegExp" for further related functions.
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
@@ -30,7 +30,7 @@
 import Data.SBV.Core.Data
 import Data.SBV.Compilers.CodeGen
 
-import Data.SBV.Utils.PrettyNum   (shex, showCFloat, showCDouble)
+import Data.SBV.Utils.PrettyNum   (chex, showCFloat, showCDouble)
 
 import GHC.Stack
 
@@ -53,7 +53,7 @@
 compileToC mbDirName nm f = compileToC' nm f >>= renderCgPgmBundle mbDirName
 
 -- | Lower level version of 'compileToC', producing a 'CgPgmBundle'
-compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
+compileToC' :: String -> SBVCodeGen () -> IO (CgConfig, CgPgmBundle)
 compileToC' nm f = do rands <- randoms `fmap` newStdGen
                       codeGen SBVToC (defaultCgConfig { cgDriverVals = rands }) nm f
 
@@ -71,7 +71,7 @@
 compileToCLib mbDirName libName comps = compileToCLib' libName comps >>= renderCgPgmBundle mbDirName
 
 -- | Lower level version of 'compileToCLib', producing a 'CgPgmBundle'
-compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
+compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO (CgConfig, CgPgmBundle)
 compileToCLib' libName comps = mergeToLib libName `fmap` mapM (uncurry compileToC') comps
 
 ---------------------------------------------------------------------------
@@ -223,12 +223,12 @@
 showSizedConst i   (False,  1) = text (if i == 0 then "false" else "true")
 showSizedConst i   (False,  8) = integer i
 showSizedConst i   (True,   8) = integer i
-showSizedConst i t@(False, 16) = text (shex False True t i) P.<> text "U"
-showSizedConst i t@(True,  16) = text (shex False True t i)
-showSizedConst i t@(False, 32) = text (shex False True t i) P.<> text "UL"
-showSizedConst i t@(True,  32) = text (shex False True t i) P.<> text "L"
-showSizedConst i t@(False, 64) = text (shex False True t i) P.<> text "ULL"
-showSizedConst i t@(True,  64) = text (shex False True t i) P.<> text "LL"
+showSizedConst i t@(False, 16) = text $ chex False True t i
+showSizedConst i t@(True,  16) = text $ chex False True t i
+showSizedConst i t@(False, 32) = text $ chex False True t i
+showSizedConst i t@(True,  32) = text $ chex False True t i
+showSizedConst i t@(False, 64) = text $ chex False True t i
+showSizedConst i t@(True,  64) = text $ chex False True t i
 showSizedConst i   (True,  1)  = die $ "Signed 1-bit value " ++ show i
 showSizedConst i   (s, sz)     = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz
 
@@ -735,11 +735,21 @@
                         in protectDiv0 k "/" z a b
         p Rem  [a, b] = protectDiv0 (kindOf (head opArgs)) "%" a a b
         p UNeg [a]    = parens (text "-" <+> a)
-        p Abs  [a]    = let f = case kindOf (head opArgs) of
-                                  KFloat  -> text "fabsf"
-                                  KDouble -> text "fabs"
-                                  _       -> text "abs"
-                        in f P.<> parens a
+        p Abs  [a]    = let f KFloat             = text "fabsf" P.<> parens a
+                            f KDouble            = text "fabs"  P.<> parens a
+                            f (KBounded False _) = text "/* unsigned, skipping call to abs */" <+> a
+                            f (KBounded True 32) = text "labs"  P.<> parens a
+                            f (KBounded True 64) = text "llabs" P.<> parens a
+                            f KUnbounded         = case cgInteger cfg of
+                                                     Nothing -> f $ KBounded True 32 -- won't matter, it'll be rejected later
+                                                     Just i  -> f $ KBounded True i
+                            f KReal              = case cgReal cfg of
+                                                     Nothing           -> f KDouble -- won't matter, it'll be rejected later
+                                                     Just CgFloat      -> f KFloat
+                                                     Just CgDouble     -> f KDouble
+                                                     Just CgLongDouble -> text "fabsl" P.<> parens a
+                            f _                  = text "abs" P.<> parens a
+                        in f (kindOf (head opArgs))
         -- for And/Or, translate to boolean versions if on boolean kind
         p And [a, b] | kindOf (head opArgs) == KBool = a <+> text "&&" <+> b
         p Or  [a, b] | kindOf (head opArgs) == KBool = a <+> text "||" <+> b
@@ -837,15 +847,17 @@
         l     = maximum (0 : map length ss)
         pad s = replicate (l - length s) ' ' ++ s
 
--- | Merge a bunch of bundles to generate code for a library
-mergeToLib :: String -> [CgPgmBundle] -> CgPgmBundle
-mergeToLib libName bundles
+-- | Merge a bunch of bundles to generate code for a library. For the final
+-- config, we simply return the first config we receive, or the default if none.
+mergeToLib :: String -> [(CgConfig, CgPgmBundle)] -> (CgConfig, CgPgmBundle)
+mergeToLib libName cfgBundles
   | length nubKinds /= 1
   = error $  "Cannot merge programs with differing SInteger/SReal mappings. Received the following kinds:\n"
           ++ unlines (map show nubKinds)
   | True
-  = CgPgmBundle bundleKind $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake]
-  where kinds       = [k | CgPgmBundle k _ <- bundles]
+  = (finalCfg, CgPgmBundle bundleKind $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake])
+  where bundles     = map snd cfgBundles
+        kinds       = [k | CgPgmBundle k _ <- bundles]
         nubKinds    = nub kinds
         bundleKind  = head nubKinds
         files       = concat [fs | CgPgmBundle _ fs <- bundles]
@@ -860,6 +872,9 @@
         libHInclude = text "#include" <+> text (show (libName ++ ".h"))
         libMake     = ("Makefile", (CgMakefile mkFlags, [genLibMake anyDriver libName sourceNms mkFlags]))
         libDriver   = (libName ++ "_driver.c", (CgDriver, mergeDrivers libName libHInclude (zip (map takeBaseName sourceNms) drivers)))
+        finalCfg    = case cfgBundles of
+                        []         -> defaultCgConfig
+                        ((c, _):_) -> c
 
 -- | Create a Makefile for the library
 genLibMake :: Bool -> String -> [String] -> [String] -> Doc
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
@@ -28,7 +28,7 @@
 
         -- * Settings
         , cgPerformRTCs, cgSetDriverValues
-        , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert
+        , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert, cgOverwriteFiles
         , cgIntegerSize, cgSRealType, CgSRealType(..)
 
         -- * Infrastructure
@@ -62,24 +62,26 @@
 
 -- | 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)
-        , cgReal          :: Maybe CgSRealType  -- ^ Type to use for representing SReal (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
-        , cgIgnoreAsserts :: Bool               -- ^ If 'True', will ignore 'sAssert' calls
+          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)
+        , cgReal               :: Maybe CgSRealType  -- ^ Type to use for representing SReal (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
+        , cgIgnoreAsserts      :: Bool               -- ^ If 'True', will ignore 'sAssert' calls
+        , cgOverwriteGenerated :: Bool               -- ^ If 'True', will overwrite the generated files without prompting.
         }
 
 -- | 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
-                           , cgReal          = Nothing
-                           , cgDriverVals    = []
-                           , cgGenDriver     = True
-                           , cgGenMakefile   = True
-                           , cgIgnoreAsserts = False
+defaultCgConfig = CgConfig { cgRTC                = False
+                           , cgInteger            = Nothing
+                           , cgReal               = Nothing
+                           , cgDriverVals         = []
+                           , cgGenDriver          = True
+                           , cgGenMakefile        = True
+                           , cgIgnoreAsserts      = False
+                           , cgOverwriteGenerated = False
                            }
 
 -- | Abstraction of target language values
@@ -88,25 +90,25 @@
 
 -- | Code-generation state
 data CgState = CgState {
-          cgInputs       :: [(String, CgVal)]
-        , cgOutputs      :: [(String, CgVal)]
-        , cgReturns      :: [CgVal]
-        , cgPrototypes   :: [String]    -- extra stuff that goes into the header
-        , cgDecls        :: [String]    -- extra stuff that goes into the top of the file
-        , cgLDFlags      :: [String]    -- extra options that go to the linker
-        , cgFinalConfig  :: CgConfig
+          cgInputs         :: [(String, CgVal)]
+        , cgOutputs        :: [(String, CgVal)]
+        , cgReturns        :: [CgVal]
+        , cgPrototypes     :: [String]    -- extra stuff that goes into the header
+        , cgDecls          :: [String]    -- extra stuff that goes into the top of the file
+        , cgLDFlags        :: [String]    -- extra options that go to the linker
+        , cgFinalConfig    :: CgConfig
         }
 
 -- | Initial configuration for code-generation
 initCgState :: CgState
 initCgState = CgState {
-          cgInputs        = []
-        , cgOutputs       = []
-        , cgReturns       = []
-        , cgPrototypes    = []
-        , cgDecls         = []
-        , cgLDFlags       = []
-        , cgFinalConfig   = defaultCgConfig
+          cgInputs         = []
+        , cgOutputs        = []
+        , cgReturns        = []
+        , cgPrototypes     = []
+        , cgDecls          = []
+        , cgLDFlags        = []
+        , cgFinalConfig    = defaultCgConfig
         }
 
 -- | The code-generation monad. Allows for precise layout of input values
@@ -184,6 +186,11 @@
                                        new = if null old then ss else old ++ [""] ++ ss
                                    in s { cgPrototypes = new })
 
+-- | If passed 'True', then we will not ask the user if we're overwriting files as we generate
+-- the C code. Otherwise, we'll prompt.
+cgOverwriteFiles :: Bool -> SBVCodeGen ()
+cgOverwriteFiles b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgOverwriteGenerated = b } })
+
 -- | Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
 cgAddDecl :: [String] -> SBVCodeGen ()
 cgAddDecl ss = modify' (\s -> s { cgDecls = cgDecls s ++ ss })
@@ -313,7 +320,7 @@
 
 -- | Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection
 -- of makefiles, source code, headers, etc.
-codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle
+codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO (CgConfig, CgPgmBundle)
 codeGen l cgConfig nm (SBVCodeGen comp) = do
    (((), st'), res) <- runSymbolic CodeGen $ runStateT comp initCgState { cgFinalConfig = cgConfig }
    let st = st' { cgInputs       = reverse (cgInputs st')
@@ -323,29 +330,38 @@
        dupNames = allNamedVars \\ nub allNamedVars
    unless (null dupNames) $
         error $ "SBV.codeGen: " ++ show nm ++ " has following argument names duplicated: " ++ unwords dupNames
-   return $ translate l (cgFinalConfig st) nm st res
 
+   return (cgFinalConfig st, translate l (cgFinalConfig st) nm st res)
+
 -- | Render a code-gen bundle to a directory or to stdout
-renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()
-renderCgPgmBundle Nothing        bundle                = print bundle
-renderCgPgmBundle (Just dirName) (CgPgmBundle _ files) = do
+renderCgPgmBundle :: Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO ()
+renderCgPgmBundle Nothing        (_  , bundle)              = print bundle
+renderCgPgmBundle (Just dirName) (cfg, CgPgmBundle _ files) = do
+
         b <- doesDirectoryExist dirName
-        unless b $ do putStrLn $ "Creating directory " ++ show dirName ++ ".."
+        unless b $ do unless overWrite $ putStrLn $ "Creating directory " ++ show dirName ++ ".."
                       createDirectoryIfMissing True dirName
+
         dups <- filterM (\fn -> doesFileExist (dirName </> fn)) (map fst files)
-        goOn <- case dups of
-                  [] -> return True
-                  _  -> do putStrLn $ "Code generation would override the following " ++ (if length dups == 1 then "file:" else "files:")
-                           mapM_ (\fn -> putStrLn ('\t' : fn)) dups
-                           putStr "Continue? [yn] "
-                           hFlush stdout
-                           resp <- getLine
-                           return $ map toLower resp `isPrefixOf` "yes"
+
+        goOn <- case (overWrite, dups) of
+                  (True, _) -> return True
+                  (_,   []) -> return True
+                  _         -> do putStrLn $ "Code generation would overwrite the following " ++ (if length dups == 1 then "file:" else "files:")
+                                  mapM_ (\fn -> putStrLn ('\t' : fn)) dups
+                                  putStr "Continue? [yn] "
+                                  hFlush stdout
+                                  resp <- getLine
+                                  return $ map toLower resp `isPrefixOf` "yes"
+
         if goOn then do mapM_ renderFile files
-                        putStrLn "Done."
+                        unless overWrite $ putStrLn "Done."
                 else putStrLn "Aborting."
-  where renderFile (f, (_, ds)) = do let fn = dirName </> f
-                                     putStrLn $ "Generating: " ++ show fn ++ ".."
+
+  where overWrite = cgOverwriteGenerated cfg
+
+        renderFile (f, (_, ds)) = do let fn = dirName </> f
+                                     unless overWrite $ putStrLn $ "Generating: " ++ show fn ++ ".."
                                      writeFile fn (render' (vcat ds))
 
 -- | An alternative to Pretty's 'render', which might have "leading" white-space in empty lines. This version
diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs
--- a/Data/SBV/Control/Query.hs
+++ b/Data/SBV/Control/Query.hs
@@ -33,8 +33,11 @@
 import Control.Monad            (unless, when, zipWithM)
 import Control.Monad.State.Lazy (get)
 
-import Data.IORef    (readIORef)
+import Data.IORef (readIORef)
 
+import qualified Data.Map    as M
+import qualified Data.IntMap as IM
+
 import Data.List     (unzip3, intercalate, nubBy, sortBy)
 import Data.Maybe    (listToMaybe, catMaybes)
 import Data.Function (on)
@@ -438,6 +441,37 @@
 getAssertionStackDepth :: Query Int
 getAssertionStackDepth = queryAssertionStackDepth <$> getQueryState
 
+-- | Upon a pop, we need to restore all arrays and tables. See: https://github.com/LeventErkok/sbv/issues/374
+restoreTablesAndArrays :: Query ()
+restoreTablesAndArrays = do st <- get
+                            qs <- getQueryState
+
+                            case queryTblArrPreserveIndex qs of
+                              Nothing       -> return ()
+                              Just (tc, ac) -> do tCount <- M.size  <$> (io . readIORef) (rtblMap   st)
+                                                  aCount <- IM.size <$> (io . readIORef) (rArrayMap st)
+
+                                                  let tInits = [ "table"  ++ show i ++ "_initializer" | i <- [tc .. tCount - 1]]
+                                                      aInits = [ "array_" ++ show i ++ "_initializer" | i <- [ac .. aCount - 1]]
+                                                      inits  = tInits ++ aInits
+
+                                                  case inits of
+                                                    []  -> return ()   -- Nothing to do
+                                                    [x] -> send True $ "(assert " ++ x ++ ")"
+                                                    xs  -> send True $ "(assert (and " ++ unwords xs ++ "))"
+
+-- | Upon a push, record the cut-off point for table and array restoration, if we haven't already
+recordTablesAndArrayCutOff :: Query ()
+recordTablesAndArrayCutOff = do st <- get
+                                qs <- getQueryState
+
+                                case queryTblArrPreserveIndex qs of
+                                  Just _  -> return () -- already recorded, nothing to do
+                                  Nothing -> do tCount <- M.size  <$> (io . readIORef) (rtblMap   st)
+                                                aCount <- IM.size <$> (io . readIORef) (rArrayMap st)
+
+                                                modifyQueryState $ \s -> s {queryTblArrPreserveIndex = Just (tCount, aCount)}
+
 -- | Run the query in a new assertion stack. That is, we push the context, run the query
 -- commands, and pop it back.
 inNewAssertionStack :: Query a -> Query a
@@ -452,6 +486,7 @@
  | i <= 0 = error $ "Data.SBV: push requires a strictly positive level argument, received: " ++ show i
  | True   = do depth <- getAssertionStackDepth
                send True $ "(push " ++ show i ++ ")"
+               recordTablesAndArrayCutOff
                modifyQueryState $ \s -> s{queryAssertionStackDepth = depth + i}
 
 -- | Pop the context, exiting a new one. Pops multiple levels if /n/ > 1. It's an error to pop levels that don't exist.
@@ -470,6 +505,7 @@
                                                   , "*** Request this as a feature for the underlying solver!"
                                                   ]
                              else do send True $ "(pop " ++ show i ++ ")"
+                                     restoreTablesAndArrays
                                      modifyQueryState $ \s -> s{queryAssertionStackDepth = depth - i}
    where shl 1 = "one level"
          shl n = show n ++ " levels"
diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs
--- a/Data/SBV/Control/Utils.hs
+++ b/Data/SBV/Control/Utils.hs
@@ -34,6 +34,7 @@
      , runProofOn
      ) where
 
+import Data.Maybe (isJust)
 import Data.List  (sortBy, elemIndex, partition, groupBy, tails)
 
 import Data.Char     (isPunctuation, isSpace, chr)
@@ -126,8 +127,8 @@
 io = liftIO
 
 -- | Sync-up the external solver with new context we have generated
-syncUpSolver :: IncState -> Query ()
-syncUpSolver is = do
+syncUpSolver :: Bool -> IncState -> Query ()
+syncUpSolver afterAPush is = do
         cfg <- getConfig
         ls  <- io $ do let swap  (a, b)        = (b, a)
                            swapc ((_, a), b)   = (b, a)
@@ -138,8 +139,9 @@
                        cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rNewConsts is)
                        arrs  <- IMap.toAscList <$> readIORef (rNewArrs is)
                        tbls  <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef (rNewTbls is)
+                       uis   <- Map.toAscList <$> readIORef (rNewUIs is)
                        as    <- readIORef (rNewAsgns is)
-                       return $ toIncSMTLib cfg inps ks cnsts arrs tbls as cfg
+                       return $ toIncSMTLib afterAPush cfg inps ks cnsts arrs tbls uis as cfg
         mapM_ (send True) $ mergeSExpr ls
 
 -- | Retrieve the query context
@@ -169,7 +171,11 @@
 inNewContext :: (State -> IO a) -> Query a
 inNewContext act = do st <- get
                       (is, r) <- io $ withNewIncState st act
-                      syncUpSolver is
+                      mbQS <- io . readIORef . queryState $ st
+                      let afterAPush = case mbQS of
+                                         Nothing -> False
+                                         Just qs -> isJust (queryTblArrPreserveIndex qs)
+                      syncUpSolver afterAPush is
                       return r
 
 -- | Similar to 'freshVar', except creates unnamed variable.
diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs
--- a/Data/SBV/Core/Data.hs
+++ b/Data/SBV/Core/Data.hs
@@ -477,7 +477,7 @@
 --
 --    * Internally handled by the library and not mapped to SMT-Lib
 --
---    * Reading an uninitialized value is considered an error (will throw exception)
+--    * Reading an uninitialized value is considered an error (will throw exception). See `mkSFunArray` on how to avoid this.
 --
 --    * Cannot check for equality (internally represented as functions)
 --
@@ -491,6 +491,13 @@
   show (SFunArray _) = "SFunArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">"
 
 -- | Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use `newArray`.)
+-- A simple way to create an array such that reading an unintialized value is assigned a free variable is
+-- to simply use an uninterpreted function. That is, use:
+--
+--  @ mkSFunArray (uninterpret "initial") @
+--
+-- Note that this will ensure all uninitialized reads to the same location will return the same value,
+-- without constraining them otherwise; with different indexes containing different values.
 mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
 mkSFunArray = SFunArray
 
diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs
--- a/Data/SBV/Core/Model.hs
+++ b/Data/SBV/Core/Model.hs
@@ -71,12 +71,6 @@
 
 import Data.SBV.Utils.Boolean
 
-mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW
-mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b)
-
-mkSymOp :: Op -> State -> Kind -> SW -> SW -> IO SW
-mkSymOp = mkSymOpSC (const (const Nothing))
-
 -- Symbolic-Word class instances
 
 -- | Generate a finite symbolic bitvector, named
@@ -1313,7 +1307,6 @@
    -- Default implementation for 'symbolicMerge' if the type is 'Generic'
    default symbolicMerge :: (G.Generic a, GMergeable (G.Rep a)) => Bool -> SBool -> a -> a -> a
    symbolicMerge = symbolicMergeDefault
-
 
 -- | If-then-else. This is by definition 'symbolicMerge' with both
 -- branches forced. This is typically the desired behavior, but also
diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs
--- a/Data/SBV/Core/Operations.hs
+++ b/Data/SBV/Core/Operations.hs
@@ -37,6 +37,8 @@
   , svRotateLeft, svRotateRight
   , svBlastLE, svBlastBE
   , svAddConstant, svIncrement, svDecrement
+  -- Utils
+  , mkSymOp
   )
   where
 
@@ -47,6 +49,7 @@
 import Data.SBV.Core.Kind
 import Data.SBV.Core.Concrete
 import Data.SBV.Core.Symbolic
+import Data.SBV.Utils.Numeric (fpIsEqualObjectH)
 
 import Data.Ratio
 
@@ -480,11 +483,19 @@
 svSymbolicMerge k force t a b
   | Just r <- svAsBool t
   = if r then a else b
-  | force, rationalSBVCheck a b, areConcretelyEqual a b
+  | force, rationalSBVCheck a b, sameResult a b
   = a
   | True
   = SVal k $ Right $ cache c
-  where c st = do swt <- svToSW st t
+  where
+        -- Be careful with +/-0 here! See https://github.com/LeventErkok/sbv/issues/382
+        sameResult (SVal _ (Left c1)) (SVal _ (Left c2)) = c1 == c2 && floatCheck (cwVal c1) (cwVal c2)
+        sameResult _                       _             = False
+        floatCheck (CWFloat  f1) (CWFloat  f2)           = f1 `fpIsEqualObjectH` f2
+        floatCheck (CWDouble d1) (CWDouble d2)           = d1 `fpIsEqualObjectH` d2
+        floatCheck _            _                        = True
+
+        c st = do swt <- svToSW st t
                   case () of
                     () | swt == trueSW  -> svToSW st a       -- these two cases should never be needed as we expect symbolicMerge to be
                     () | swt == falseSW -> svToSW st b       -- called with symbolic tests, but just in case..
@@ -819,6 +830,52 @@
    where c st = do swa <- svToSW st a
                    opS st k swa
 
+{- A note on constant folding.
+
+There are cases where we miss out on certain constant foldings. On May 8 2018, Matt Peddie pointed this
+out, as the C code he was getting had redundancies. I was aware that could be missing constant foldings
+due to missed out optimizations, or some other code snafu, but till Matt pointed it out I haven't realized
+that we could be hiding constants inside an if-then-else. The example is:
+
+     proveWith z3{verbose=True} $ \x -> 0 .< ite (x .== (x::SWord8)) 1 (2::SWord8)
+
+If you try this, you'll see that it generates (shortened):
+
+    (define-fun s1 () (_ BitVec 8) #x00)
+    (define-fun s2 () (_ BitVec 8) #x01)
+    (define-fun s3 () Bool (bvult s1 s2))
+
+But clearly we have all the info for s3 to be computed! The issue here is that the reduction of @x .== x@ to @true@
+happens after we start computing the if-then-else, hence we are already committed to an SW at that point. The call
+to ite eventually recognizes this, but at that point it picks up the now constants from SW's, missing the constant
+folding opportunity.
+
+We can fix this, by looking up the constants table in liftSW2, like this:
+
+
+    liftSW2 :: (CW -> CW -> Bool) -> (CW -> CW -> CW) -> (State -> Kind -> SW -> SW -> IO SW) -> Kind -> SVal -> SVal -> Cached SW
+    liftSW2 okCW opCW opS k a b = cache c
+      where c st = do sw1 <- svToSW st a
+                      sw2 <- svToSW st b
+                      cmap <- readIORef (rconstMap st)
+                      let cw1  = [cw | ((_, cw), sw) <- M.toList cmap, sw == sw1]
+                          cw2  = [cw | ((_, cw), sw) <- M.toList cmap, sw == sw2]
+                      case (cw1, cw2) of
+                        ([x], [y]) | okCW x y -> newConst st $ opCW x y
+                        _                     -> opS st k sw1 sw2
+
+(with obvious modifications to call sites to get the proper arguments.)
+
+But this means that we have to grab the constant list for every symbolicly lifted operation, also do the
+same for other places, etc.; for the rare opportunity of catching a @x .== x@ optimization. Even then, the
+constants for the branches would still be generated. (i.e., in the above example we would still generate
+@s1@ and @s2@, but would skip @s3@.)
+
+It seems to me that the price to pay is rather high, as this is hardly the most common case; so we're opting
+here to ignore these cases.
+
+See https://github.com/LeventErkok/sbv/issues/379 for some further discussion.
+-}
 liftSW2 :: (State -> Kind -> SW -> SW -> IO SW) -> Kind -> SVal -> SVal -> Cached SW
 liftSW2 opS k a b = cache c
   where c st = do sw1 <- svToSW st a
@@ -833,9 +890,11 @@
 liftSym2B _   okCW opCR opCI opCF opCD opCC opCS opUI (SVal _ (Left a)) (SVal _ (Left b)) | okCW a b = svBool (liftCW2 opCR opCI opCF opCD opCC opCS opUI a b)
 liftSym2B opS _    _    _    _    _    _    _    _    a                 b                            = SVal KBool $ Right $ liftSW2 opS KBool a b
 
+-- | Create a symbolic two argument operation; with shortcut optimizations
 mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW
 mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b)
 
+-- | Create a symbolic two argument operation; no shortcut optimizations
 mkSymOp :: Op -> State -> Kind -> SW -> SW -> IO SW
 mkSymOp = mkSymOpSC (const (const Nothing))
 
@@ -892,11 +951,6 @@
 isConcreteMin (SVal _ (Left (CW (KBounded True  w) (CWInteger n)))) = n == - bit (w - 1)
 isConcreteMin (SVal _ (Left (CW KBool              (CWInteger n)))) = n == 0
 isConcreteMin _                                                     = False
-
--- | Predicate for optimizing conditionals.
-areConcretelyEqual :: SVal -> SVal -> Bool
-areConcretelyEqual (SVal _ (Left a)) (SVal _ (Left b)) = a == b
-areConcretelyEqual _                       _           = False
 
 -- | Most operations on concrete rationals require a compatibility check to avoid faulting
 -- on algebraic reals.
diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs
--- a/Data/SBV/Core/Symbolic.hs
+++ b/Data/SBV/Core/Symbolic.hs
@@ -439,6 +439,7 @@
                              , queryTerminate           :: IO ()
                              , queryTimeOutValue        :: Maybe Int
                              , queryAssertionStackDepth :: Int
+                             , queryTblArrPreserveIndex :: Maybe (Int, Int)
                              }
 
 -- | A query is a user-guided mechanism to directly communicate and extract results from the solver.
@@ -619,6 +620,7 @@
                          , rNewConsts :: IORef CnstMap
                          , rNewArrs   :: IORef ArrayMap
                          , rNewTbls   :: IORef TableMap
+                         , rNewUIs    :: IORef UIMap
                          , rNewAsgns  :: IORef SBVPgm
                          }
 
@@ -630,12 +632,14 @@
         nc  <- newIORef Map.empty
         am  <- newIORef IMap.empty
         tm  <- newIORef Map.empty
+        ui  <- newIORef Map.empty
         pgm <- newIORef (SBVPgm S.empty)
         return IncState { rNewInps   = is
                         , rNewKinds  = ks
                         , rNewConsts = nc
                         , rNewArrs   = am
                         , rNewTbls   = tm
+                        , rNewUIs    = ui
                         , rNewAsgns  = pgm
                         }
 
@@ -764,18 +768,24 @@
 newUninterpreted st nm t mbCode
   | null nm || not enclosed && (not (isAlpha (head nm)) || not (all validChar (tail nm)))
   = error $ "Bad uninterpreted constant name: " ++ show nm ++ ". Must be a valid identifier."
-  | True = do
-        uiMap <- readIORef (rUIMap st)
-        case nm `Map.lookup` uiMap of
-          Just t' -> when (t /= t') $ error $  "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n"
-                                            ++ "      Current type      : " ++ show t ++ "\n"
-                                            ++ "      Previously used at: " ++ show t'
-          Nothing -> do modifyState st rUIMap (Map.insert nm t) $ noInteractive [ "Uninterpreted function introduction:"
-                                                                                , "  Named:  " ++ nm
-                                                                                , "  Type :  " ++ show t
-                                                                                ]
-                        when (isJust mbCode) $ modifyState st rCgMap (Map.insert nm (fromJust mbCode)) (return ())
-  where validChar x = isAlphaNum x || x `elem` "_"
+  | True = do uiMap <- readIORef (rUIMap st)
+              case nm `Map.lookup` uiMap of
+                Just t' -> checkType t' (return ())
+                Nothing -> do modifyState st rUIMap (Map.insert nm t)
+                                        $ modifyIncState st rNewUIs (\newUIs -> case nm `Map.lookup` newUIs of
+                                                                                  Just t' -> checkType t' newUIs
+                                                                                  Nothing -> Map.insert nm t newUIs)
+
+                              -- No need to record the code in interactive mode: CodeGen doesn't use interactive
+                              when (isJust mbCode) $ modifyState st rCgMap (Map.insert nm (fromJust mbCode)) (return ())
+  where checkType t' cont
+          | t /= t' = error $  "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n"
+                            ++ "      Current type      : " ++ show t ++ "\n"
+                            ++ "      Previously used at: " ++ show t'
+          | True    = cont
+
+
+        validChar x = isAlphaNum x || x `elem` "_"
         enclosed    = head nm == '|' && last nm == '|' && length nm > 2 && not (any (`elem` "|\\") (tail (init nm)))
 
 -- | Add a new sAssert based constraint
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
@@ -784,6 +784,7 @@
                                                  , queryTerminate           = cleanUp
                                                  , queryTimeOutValue        = Nothing
                                                  , queryAssertionStackDepth = 0
+                                                 , queryTblArrPreserveIndex = Nothing
                                                  }
                                  qsp = queryState ctx
 
diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs
--- a/Data/SBV/SMT/SMTLib.hs
+++ b/Data/SBV/SMT/SMTLib.hs
@@ -30,9 +30,9 @@
                                       SMTLib2 -> toSMTLib2
 
 -- | Convert to SMT-Lib, in an incremental query context.
-toIncSMTLib :: SMTConfig -> SMTLibIncConverter [String]
-toIncSMTLib SMTConfig{smtLibVersion} = case smtLibVersion of
-                                         SMTLib2 -> toIncSMTLib2
+toIncSMTLib :: Bool -> SMTConfig -> SMTLibIncConverter [String]
+toIncSMTLib afterAPush SMTConfig{smtLibVersion} = case smtLibVersion of
+                                                     SMTLib2 -> toIncSMTLib2 afterAPush
 
 -- | Convert to SMTLib-2 format
 toSMTLib2 :: SMTLibConverter SMTLibPgm
@@ -67,6 +67,6 @@
                  where quantifiers = map fst (fst qinps)
 
 -- | Convert to SMTLib-2 format
-toIncSMTLib2 :: SMTLibIncConverter [String]
+toIncSMTLib2 :: Bool -> SMTLibIncConverter [String]
 toIncSMTLib2 = cvt SMTLib2
   where cvt SMTLib2 = SMT2.cvtInc
diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs
--- a/Data/SBV/SMT/SMTLib2.hs
+++ b/Data/SBV/SMT/SMTLib2.hs
@@ -13,7 +13,7 @@
 module Data.SBV.SMT.SMTLib2(cvt, cvtInc) where
 
 import Data.Bits  (bit)
-import Data.List  (intercalate, partition)
+import Data.List  (intercalate, partition, unzip3)
 
 import qualified Data.Foldable as F (toList)
 import qualified Data.Map      as M
@@ -110,7 +110,7 @@
              ++ [ "; --- optimization tracker variables ---" | not (null trackerVars) ]
              ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType [] s ++ ") ; tracks " ++ nm | (s, nm) <- trackerVars]
              ++ [ "; --- constant tables ---" ]
-             ++ concatMap constTable constTables
+             ++ concatMap (constTable False) constTables
              ++ [ "; --- skolemized tables ---" ]
              ++ map (skolemTable (unwords (map swType foralls))) skolemTables
              ++ [ "; --- arrays ---" ]
@@ -128,6 +128,10 @@
                 ]
              ++ map mkAssign postQuantifierAssigns
 
+             ++ concat arrayDelayeds
+
+             ++ concat arraySetups
+
              ++ delayedAsserts delayedEqualities
 
              ++ finalAssert
@@ -152,8 +156,8 @@
 
         (constTables, skolemTables) = ([(t, d) | (t, Left d) <- allTables], [(t, d) | (t, Right d) <- allTables])
         allTables = [(t, genTableData rm skolemMap (not (null foralls), forallArgs) (map fst consts) t) | t <- tbls]
-        (arrayConstants, allArrayDelayeds) = unzip $ map (declArray (not (null foralls)) (map fst consts) skolemMap) arrs
-        delayedEqualities = concatMap snd skolemTables ++ concat allArrayDelayeds
+        (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray False (not (null foralls)) (map fst consts) skolemMap) arrs
+        delayedEqualities = concatMap snd skolemTables
 
         delayedAsserts []              = []
         delayedAsserts ds@(deH : deTs)
@@ -249,8 +253,8 @@
               body (c:cs) i = "(ite (= x " ++ c ++ ") " ++ show i ++ " " ++ body cs (i+1) ++ ")"
 
 -- | Convert in a query context
-cvtInc :: SMTLibIncConverter [String]
-cvtInc inps ks consts arrs tbls (SBVPgm asgnsSeq) cfg =
+cvtInc :: Bool -> SMTLibIncConverter [String]
+cvtInc afterAPush inps ks consts arrs tbls uis (SBVPgm asgnsSeq) cfg =
             -- sorts
                concatMap declSort [(s, dt) | KUserSort s dt <- Set.toList ks]
             -- constants
@@ -259,12 +263,16 @@
             ++ map declInp inps
             -- arrays
             ++ concat arrayConstants
+            -- uninterpreteds
+            ++ concatMap declUI uis
             -- tables
-            ++ concatMap constTable allTables
+            ++ concatMap (constTable afterAPush) allTables
             -- expressions
             ++ map  (declDef cfg skolemMap tableMap) (F.toList asgnsSeq)
             -- delayed equalities
-            ++ concatMap asrt arrayDelayeds
+            ++ concat arrayDelayeds
+            -- array setups
+            ++ concat arraySetups
   where -- NB. The below setting of skolemMap to empty is OK, since we do
         -- not support queries in the context of skolemized variables
         skolemMap = M.empty
@@ -273,14 +281,12 @@
 
         declInp (s, _) = "(declare-fun " ++ show s ++ " () " ++ swType s ++ ")"
 
-        (arrayConstants, arrayDelayeds) = unzip $ map (declArray False (map fst consts) skolemMap) arrs
+        (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray afterAPush False (map fst consts) skolemMap) arrs
 
         allTables = [(t, either id id (genTableData rm skolemMap (False, []) (map fst consts) t)) | t <- tbls]
         tableMap  = IM.fromList $ map mkTable allTables
           where mkTable (((t, _, _), _), _) = (t, "table" ++ show t)
 
-        asrt = map (\s -> "(assert " ++ s ++ ")")
-
 declDef :: SMTConfig -> SkolemMap -> TableMap -> (SW, SBVExpr) -> String
 declDef cfg skolemMap tableMap (s, expr) =
         case expr of
@@ -304,12 +310,30 @@
 declAx :: (String, [String]) -> String
 declAx (nm, ls) = (";; -- user given axiom: " ++ nm ++ "\n") ++ intercalate "\n" ls
 
-constTable :: (((Int, Kind, Kind), [SW]), [String]) -> [String]
-constTable (((i, ak, rk), _elts), is) = decl : map wrap is
+constTable :: Bool -> (((Int, Kind, Kind), [SW]), [String]) -> [String]
+constTable afterAPush (((i, ak, rk), _elts), is) = decl : zipWith wrap [(0::Int)..] is ++ setup
   where t       = "table" ++ show i
         decl    = "(declare-fun " ++ t ++ " (" ++ smtType ak ++ ") " ++ smtType rk ++ ")"
-        wrap  s = "(assert " ++ s ++ ")"
 
+        -- Arrange for initializers
+        mkInit idx   = "table" ++ show i ++ "_initializer_" ++ show (idx :: Int)
+        initializer  = "table" ++ show i ++ "_initializer"
+        wrap index s
+          | afterAPush = "(define-fun " ++ mkInit index ++ " () Bool " ++ s ++ ")"
+          | True       = "(assert " ++ s ++ ")"
+        lis          = length is
+        setup
+          | not afterAPush = []
+          | lis == 0       = [ "(define-fun " ++ initializer ++ " () Bool true) ; no initializiation needed"
+                             ]
+          | lis == 1       = [ "(define-fun " ++ initializer ++ " () Bool " ++ mkInit 0 ++ ")"
+                             , "(assert " ++ initializer ++ ")"
+                             ]
+          | True           = [ "(define-fun " ++ initializer ++ " () Bool (and " ++ unwords (map mkInit [0..lis - 1]) ++ "))"
+                             , "(assert " ++ initializer ++ ")"
+                             ]
+
+
 skolemTable :: String -> (((Int, Kind, Kind), [SW]), [String]) -> String
 skolemTable qsIn (((i, ak, rk), _elts), _) = decl
   where qs   = if null qsIn then "" else qsIn ++ " "
@@ -335,8 +359,8 @@
 -- we might have to skolemize those. Implement this properly.
 -- The difficulty is with the Mutate/Merge: We have to postpone an init if
 -- the components are themselves postponed, so this cannot be implemented as a simple map.
-declArray :: Bool -> [SW] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String])
-declArray quantified consts skolemMap (i, (_, (aKnd, bKnd), ctx)) = (adecl : map (wrap . snd) pre, map snd post)
+declArray :: Bool -> Bool -> [SW] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String])
+declArray afterAPush quantified consts skolemMap (i, (_, (aKnd, bKnd), ctx)) = (adecl : zipWith wrap [(0::Int)..] (map snd pre), zipWith wrap [lpre..] (map snd post), setup)
   where topLevel = not quantified || case ctx of
                                        ArrayFree         -> True
                                        ArrayMutate _ a b -> all (`elem` consts) [a, b]
@@ -353,7 +377,25 @@
                     ArrayFree         -> []
                     ArrayMutate j a b -> [(all (`elem` consts) [a, b], "(= " ++ nm ++ " (store array_" ++ show j ++ " " ++ ssw a ++ " " ++ ssw b ++ "))")]
                     ArrayMerge  t j k -> [(t `elem` consts,            "(= " ++ nm ++ " (ite " ++ ssw t ++ " array_" ++ show j ++ " array_" ++ show k ++ "))")]
-        wrap s = "(assert " ++ s ++ ")"
+
+        -- Arrange for initializers
+        mkInit idx    = "array_" ++ show i ++ "_initializer_" ++ show (idx :: Int)
+        initializer   = "array_" ++ show i ++ "_initializer"
+        wrap index s
+          | afterAPush = "(define-fun " ++ mkInit index ++ " () Bool " ++ s ++ ")"
+          | True       = "(assert " ++ s ++ ")"
+        lpre          = length pre
+        lAll          = lpre + length post
+        setup
+          | not afterAPush = []
+          | lAll == 0      = [ "(define-fun " ++ initializer ++ " () Bool true) ; no initializiation needed"
+                             ]
+          | lAll == 1      = [ "(define-fun " ++ initializer ++ " () Bool " ++ mkInit 0 ++ ")"
+                             , "(assert " ++ initializer ++ ")"
+                             ]
+          | True           = [ "(define-fun " ++ initializer ++ " () Bool (and " ++ unwords (map mkInit [0..lAll - 1]) ++ "))"
+                             , "(assert " ++ initializer ++ ")"
+                             ]
 
 swType :: SW -> String
 swType s = smtType (kindOf s)
diff --git a/Data/SBV/SMT/Utils.hs b/Data/SBV/SMT/Utils.hs
--- a/Data/SBV/SMT/Utils.hs
+++ b/Data/SBV/SMT/Utils.hs
@@ -57,6 +57,7 @@
                           -> [(SW, CW)]                  -- ^ constants
                           -> [(Int, ArrayInfo)]          -- ^ newly created arrays
                           -> [((Int, Kind, Kind), [SW])] -- ^ newly created tables
+                          -> [(String, SBVType)]         -- ^ newly created uninterpreted functions/constants
                           -> SBVPgm                      -- ^ assignments
                           -> SMTConfig                   -- ^ configuration
                           -> a
diff --git a/Data/SBV/Tools/CodeGen.hs b/Data/SBV/Tools/CodeGen.hs
--- a/Data/SBV/Tools/CodeGen.hs
+++ b/Data/SBV/Tools/CodeGen.hs
@@ -16,7 +16,7 @@
           SBVCodeGen
 
         -- ** Setting code-generation options
-        , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile
+        , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile, cgOverwriteFiles
 
         -- ** Designating inputs
         , cgInput, cgInputArr
diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs
--- a/Data/SBV/Tools/GenTest.hs
+++ b/Data/SBV/Tools/GenTest.hs
@@ -225,7 +225,7 @@
         mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}"
         v cw = case kindOf cw of
                   KBool           -> if cwToBool cw then "true " else "false"
-                  KBounded sgn sz -> let CWInteger w = cwVal cw in shex  False True (sgn, sz) w
+                  KBounded sgn sz -> let CWInteger w = cwVal cw in chex  False True (sgn, sz) w
                   KUnbounded      -> let CWInteger w = cwVal cw in shexI False True           w
                   KFloat          -> let CWFloat w   = cwVal cw in showCFloat w
                   KDouble         -> let CWDouble w  = cwVal cw in showCDouble w
diff --git a/Data/SBV/Utils/PrettyNum.hs b/Data/SBV/Utils/PrettyNum.hs
--- a/Data/SBV/Utils/PrettyNum.hs
+++ b/Data/SBV/Utils/PrettyNum.hs
@@ -14,7 +14,7 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 
 module Data.SBV.Utils.PrettyNum (
-        PrettyNum(..), readBin, shex, shexI, sbin, sbinI
+        PrettyNum(..), readBin, shex, chex, shexI, sbin, sbinI
       , showCFloat, showCDouble, showHFloat, showHDouble
       , showSMTFloat, showSMTDouble, smtRoundingMode, cwToSMTLib, mkSkolemZero
       ) where
@@ -129,6 +129,33 @@
        pre | shPre = "0x"
            | True  = ""
        l = (size + 3) `div` 4
+
+-- | Show as hexadecimal, but for C programs. We have to be careful about
+-- printing min-bounds, since C does some funky casting, possibly losing
+-- the sign bit. In those cases, we use the defined constants in <stdint.h>.
+-- We also properly append the necessary suffixes as needed.
+chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
+chex shType shPre (signed, size) a
+   | Just s <- (signed, size, fromIntegral a) `lookup` specials
+   = s
+   | True
+   = shex shType shPre (signed, size) a ++ suffix
+  where specials :: [((Bool, Int, Integer), String)]
+        specials = [ ((True,  8, fromIntegral (minBound :: Int8)),  "INT8_MIN" )
+                   , ((True, 16, fromIntegral (minBound :: Int16)), "INT16_MIN")
+                   , ((True, 32, fromIntegral (minBound :: Int32)), "INT32_MIN")
+                   , ((True, 64, fromIntegral (minBound :: Int64)), "INT64_MIN")
+                   ]
+        suffix = case (signed, size) of
+                   (False, 16) -> "U"
+
+                   (False, 32) -> "UL"
+                   (True,  32) -> "L"
+
+                   (False, 64) -> "ULL"
+                   (True,  64) -> "LL"
+
+                   _           -> ""
 
 -- | Show as a hexadecimal value, integer version. Almost the same as shex above
 -- except we don't have a bit-length so the length of the string will depend
diff --git a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs
new file mode 100644
--- /dev/null
+++ b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs
@@ -0,0 +1,141 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Documentation.SBV.Examples.Puzzles.HexPuzzle
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- A solution to the hexagon solver puzzle: <http://www5.cadence.com/2018ClubVQuiz_LP.html>
+-- In case the above URL goes dead, here's an ASCII rendering of the problem.
+--
+-- We're given a board, with 19 hexagon cells. The cells are arranged as follows:
+--
+-- @
+--                     01  02  03
+--                   04  05  06  07
+--                 08  09  10  11  12
+--                   13  14  15  16
+--                     17  18  19
+-- @
+--
+--   - Each cell has a color, one of @BLACK@, @BLUE@, @GREEN@, or @RED@.
+--
+--   - At each step, you get to press one of the center buttons. That is,
+--     one of 5, 6, 9, 10, 11, 14, or 15.
+--
+--   - Pressing a button that is currently colored @BLACK@ has no effect.
+--
+--   - Otherwise (i.e., if the pressed button is not @BLACK@), then colors
+--     rotate clockwise around that button. For instance if you press 15
+--     when it is not colored @BLACK@, then 11 moves to 16, 16 moves to 19,
+--     19 moves to 18, 18 moves to 14, 14 moves to 10, and 10 moves to 11.
+--
+--   - Note that by "move," we mean the colors move: We still refer to the buttons
+--     with the same number after a move.
+--
+-- You are given an initial board coloring, and a final one. Your goal is
+-- to find a minimal sequence of button presses that will turn the original board
+-- to the final one.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE DeriveDataTypeable  #-}
+{-# LANGUAGE DeriveAnyClass      #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Documentation.SBV.Examples.Puzzles.HexPuzzle where
+
+import Data.SBV
+import Data.SBV.Control
+
+-- | Colors we're allowed
+data Color = Black | Blue | Green | Red
+
+-- | Make 'Color' a symbolic value.
+mkSymbolicEnumeration ''Color
+
+-- | Give symbolic colors a name for convenience.
+type SColor = SBV Color
+
+-- | Use 8-bit words for button numners, even though we only have 1 to 19.
+type Button  = Word8
+
+-- | Symbolic version of button.
+type SButton = SBV Button
+
+-- | The grid is an array mapping each button to its color.
+type Grid = SFunArray Button Color
+
+-- | Given a button press, and the current grid, compute the next grid.
+-- If the button is "unpressable", i.e., if it is not one of the center
+-- buttons or it is currently colored black, we return the grid unchanged.
+next :: SButton -> Grid -> Grid
+next b g = ite (readArray g b .== literal Black) g
+         $ ite (b .==  5)                        (rot [ 1,  2,  6, 10,  9,  4])
+         $ ite (b .==  6)                        (rot [ 2,  3,  7, 11, 10,  5])
+         $ ite (b .==  9)                        (rot [ 4,  5, 10, 14, 13,  8])
+         $ ite (b .== 10)                        (rot [ 5,  6, 11, 15, 14,  9])
+         $ ite (b .== 11)                        (rot [ 6,  7, 12, 16, 15, 10])
+         $ ite (b .== 14)                        (rot [ 9, 10, 15, 18, 17, 13])
+         $ ite (b .== 15)                        (rot [10, 11, 16, 19, 18, 14]) g
+  where rot xs = foldr (\(i, c) a -> writeArray a (literal i) c) g (zip new cur)
+          where cur = map (readArray g . literal) xs
+                new = tail xs ++ [head xs]
+
+-- | Iteratively search at increasing depths of button-presses to see if we can
+-- transform from the initial board position to a final board position.
+search :: [Color] -> [Color] -> IO ()
+search initial final = runSMT $ do setLogic Logic_ALL
+                                   query $ loop (0 :: Int) initGrid []
+
+  where initGrid = foldr (\(i, c) a -> writeArray a (literal i) (literal c)) (mkSFunArray (uninterpret "initGrid")) (zip [1..] initial)
+
+        loop i g sofar = do io $ putStrLn $ "Searching at depth: " ++ show i
+
+                            -- Go into a new context, and see if we've reached a solution:
+                            push 1
+                            constrain $ map (readArray g . literal) [1..19] .== map literal final
+                            cs <- checkSat
+
+                            case cs of
+                              Unk   -> error $ "Solver said Unknown, depth: " ++ show i
+
+                              Unsat -> do -- It didn't work out. Pop and try again with one more move:
+                                          pop 1
+                                          b <- freshVar ("press_" ++ show i)
+                                          constrain $ b `sElem` map literal [5, 6, 9, 10, 11, 14, 15]
+                                          loop (i+1) (next b g) (sofar ++ [b])
+
+                              Sat   -> do vs <- mapM getValue sofar
+                                          io $ putStrLn $ "Found: " ++ show vs
+                                          findOthers sofar vs
+
+        findOthers vs = go
+                where go curVals = do constrain $ bOr $ zipWith (\v c -> v ./= literal c) vs curVals
+                                      cs <- checkSat
+                                      case cs of
+                                       Unk   -> error $ "Unknown!"
+                                       Unsat -> io $ putStrLn $ "There are no more solutions."
+                                       Sat   -> do newVals <- mapM getValue vs
+                                                   io $ putStrLn $ "Found: " ++ show newVals
+                                                   go newVals
+
+-- | A particular example run. We have:
+--
+-- >>> example
+-- Searching at depth: 0
+-- Searching at depth: 1
+-- Searching at depth: 2
+-- Searching at depth: 3
+-- Searching at depth: 4
+-- Searching at depth: 5
+-- Searching at depth: 6
+-- Found: [10,10,9,11,14,6]
+-- Found: [10,10,11,9,14,6]
+-- There are no more solutions.
+example :: IO ()
+example = search initBoard finalBoard
+   where initBoard  = [Black, Black, Black, Red, Blue, Green, Red, Black, Green, Green, Green, Black, Red, Green, Green, Red, Black, Black, Black]
+         finalBoard = [Black, Red, Black, Black, Green, Green, Black, Red, Green, Blue, Green, Red, Black, Green, Green, Black, Black, Red, Black]
diff --git a/SBVTestSuite/GoldFiles/queryArrays6.gold b/SBVTestSuite/GoldFiles/queryArrays6.gold
new file mode 100644
--- /dev/null
+++ b/SBVTestSuite/GoldFiles/queryArrays6.gold
@@ -0,0 +1,79 @@
+** Calling: z3 -nw -in -smt2
+[GOOD] ; Automatically generated by SBV. Do not edit.
+[GOOD] (set-option :print-success true)
+[GOOD] (set-option :global-declarations true)
+[GOOD] (set-option :smtlib2_compliant true)
+[GOOD] (set-option :diagnostic-output-channel "stdout")
+[GOOD] (set-option :produce-models true)
+[GOOD] (set-logic ALL) ; has non-bitvector arrays, using catch-all.
+[GOOD] ; --- uninterpreted sorts ---
+[GOOD] ; --- literal constants ---
+[GOOD] (define-fun s_2 () Bool false)
+[GOOD] (define-fun s_1 () Bool true)
+[GOOD] ; --- skolem constants ---
+[GOOD] ; --- constant tables ---
+[GOOD] ; --- skolemized tables ---
+[GOOD] ; --- arrays ---
+[GOOD] (declare-fun array_0 () (Array Int Int))
+[GOOD] ; --- uninterpreted constants ---
+[GOOD] ; --- user given axioms ---
+[GOOD] ; --- formula ---
+[GOOD] (assert s_1)
+[GOOD] (push 1)
+[GOOD] (define-fun s0 () Int 1)
+[GOOD] (define-fun s2 () Int 5)
+[GOOD] (declare-fun array_1 () (Array Int Int))
+[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s0)))
+[GOOD] (define-fun s1 () Int (select array_1 s0))
+[GOOD] (define-fun s3 () Bool (= s1 s2))
+[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)
+[GOOD] (assert array_1_initializer)
+[GOOD] (assert s3)
+[SEND] (check-sat)
+[RECV] unsat
+[GOOD] (pop 1)
+[GOOD] (assert array_1_initializer)
+[GOOD] (declare-fun s4 () Int)
+[GOOD] (define-fun s6 () Int 3)
+[GOOD] (define-fun s5 () Bool (>= s4 s0))
+[GOOD] (define-fun s7 () Bool (< s4 s6))
+[GOOD] (define-fun s8 () Bool (and s5 s7))
+[GOOD] (assert s8)
+[GOOD] (push 1)
+[GOOD] (declare-fun array_2 () (Array Int Int))
+[GOOD] (define-fun s9 () Int (+ s1 s4))
+[GOOD] (define-fun s10 () Int (select array_2 s0))
+[GOOD] (define-fun s11 () Bool (= s2 s10))
+[GOOD] (define-fun array_2_initializer_0 () Bool (= array_2 (store array_1 s0 s9)))
+[GOOD] (define-fun array_2_initializer () Bool array_2_initializer_0)
+[GOOD] (assert array_2_initializer)
+[GOOD] (assert s11)
+[SEND] (check-sat)
+[RECV] unsat
+[GOOD] (pop 1)
+[GOOD] (assert (and array_1_initializer array_2_initializer))
+[GOOD] (declare-fun s12 () Int)
+[GOOD] (define-fun s13 () Bool (>= s12 s0))
+[GOOD] (define-fun s14 () Bool (< s12 s6))
+[GOOD] (define-fun s15 () Bool (and s13 s14))
+[GOOD] (assert s15)
+[GOOD] (push 1)
+[GOOD] (declare-fun array_3 () (Array Int Int))
+[GOOD] (define-fun s16 () Int (+ s10 s12))
+[GOOD] (define-fun s17 () Int (select array_3 s0))
+[GOOD] (define-fun s18 () Bool (= s2 s17))
+[GOOD] (define-fun array_3_initializer_0 () Bool (= array_3 (store array_2 s0 s16)))
+[GOOD] (define-fun array_3_initializer () Bool array_3_initializer_0)
+[GOOD] (assert array_3_initializer)
+[GOOD] (assert s18)
+[SEND] (check-sat)
+[RECV] sat
+[SEND] (get-value (s4))
+[RECV] ((s4 2))
+[SEND] (get-value (s12))
+[RECV] ((s12 2))
+*** Solver   : Z3
+*** Exit code: ExitSuccess
+
+ FINAL:[2,2]
+DONE!
diff --git a/SBVTestSuite/GoldFiles/tgen_c.gold b/SBVTestSuite/GoldFiles/tgen_c.gold
--- a/SBVTestSuite/GoldFiles/tgen_c.gold
+++ b/SBVTestSuite/GoldFiles/tgen_c.gold
@@ -41,16 +41,16 @@
 } CTestTestVector;
 
 CTestTestVector CTest[] = {
-      {{0xfcbe0fdb, 0xd321df04}, {0xcfdfeedf, 0x299c30d7, 0x0f03046c}}
-    , {{0x7e037b43, 0xf66d083b}, {0x7470837e, 0x87967308, 0x042e8071}}
-    , {{0xce482a70, 0x66b7c768}, {0x34fff1d8, 0x67906308, 0xdc5e4d80}}
-    , {{0xec1eda04, 0x465a32a9}, {0x32790cad, 0xa5c4a75b, 0xa45ab4a4}}
-    , {{0x61f89467, 0x00d8fb06}, {0x62d18f6d, 0x611f9961, 0x3c3c776a}}
-    , {{0x30e2d88c, 0x10ea31cd}, {0x41cd0a59, 0x1ff8a6bf, 0x4112341c}}
-    , {{0x4bf1b3fd, 0x2124dc8b}, {0x6d169088, 0x2accd772, 0xdf7e265f}}
-    , {{0x96885656, 0x60a8c5ca}, {0xf7311c20, 0x35df908c, 0x9a744ddc}}
-    , {{0xc2bac856, 0xe5a9367c}, {0xa863fed2, 0xdd1191da, 0xe7812da8}}
-    , {{0x8b10b4f2, 0xf010d50f}, {0x7b218a01, 0x9affdfe3, 0x3ba7f42e}}
+      {{0xfcbe0fdbUL, 0xd321df04UL}, {0xcfdfeedfUL, 0x299c30d7UL, 0x0f03046cUL}}
+    , {{0x7e037b43UL, 0xf66d083bUL}, {0x7470837eUL, 0x87967308UL, 0x042e8071UL}}
+    , {{0xce482a70UL, 0x66b7c768UL}, {0x34fff1d8UL, 0x67906308UL, 0xdc5e4d80UL}}
+    , {{0xec1eda04UL, 0x465a32a9UL}, {0x32790cadUL, 0xa5c4a75bUL, 0xa45ab4a4UL}}
+    , {{0x61f89467UL, 0x00d8fb06UL}, {0x62d18f6dUL, 0x611f9961UL, 0x3c3c776aUL}}
+    , {{0x30e2d88cUL, 0x10ea31cdUL}, {0x41cd0a59UL, 0x1ff8a6bfUL, 0x4112341cUL}}
+    , {{0x4bf1b3fdUL, 0x2124dc8bUL}, {0x6d169088UL, 0x2accd772UL, 0xdf7e265fUL}}
+    , {{0x96885656UL, 0x60a8c5caUL}, {0xf7311c20UL, 0x35df908cUL, 0x9a744ddcUL}}
+    , {{0xc2bac856UL, 0xe5a9367cUL}, {0xa863fed2UL, 0xdd1191daUL, 0xe7812da8UL}}
+    , {{0x8b10b4f2UL, 0xf010d50fUL}, {0x7b218a01UL, 0x9affdfe3UL, 0x3ba7f42eUL}}
 };
 
 int CTestLength = 10;
diff --git a/SBVTestSuite/TestSuite/Arrays/Query.hs b/SBVTestSuite/TestSuite/Arrays/Query.hs
--- a/SBVTestSuite/TestSuite/Arrays/Query.hs
+++ b/SBVTestSuite/TestSuite/Arrays/Query.hs
@@ -26,6 +26,7 @@
     , goldenCapturedIO "queryArrays3" $ t q3
     , goldenCapturedIO "queryArrays4" $ t q4
     , goldenCapturedIO "queryArrays5" $ t q5
+    , goldenCapturedIO "queryArrays6" $ t q6
     ]
     where t tc goldFile = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just goldFile} tc
                              appendFile goldFile ("\n FINAL:" ++ show r ++ "\nDONE!\n")
@@ -99,5 +100,21 @@
                      Sat   -> do av <- getValue a
                                  vv <- getValue v
                                  return $ Just (av, vv)
+
+q6 :: Symbolic [Integer]
+q6 = do (a :: SArray Integer Integer) <- newArray "a"
+
+        query $ loop (writeArray a 1 1) []
+
+  where loop a sofar = do push 1
+                          constrain $ readArray a 1 .== 5
+                          cs <- checkSat
+                          case cs of
+                            Unk   -> error "Unknown"
+                            Unsat -> do pop 1
+                                        d <- freshVar $ "d" ++ show (length sofar)
+                                        constrain $ d .>= 1 &&& d .< 3
+                                        loop (writeArray a 1 (readArray a 1 + d)) (sofar ++ [d])
+                            Sat   -> mapM getValue sofar
 
 {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
diff --git a/SBVTestSuite/TestSuite/BitPrecise/Legato.hs b/SBVTestSuite/TestSuite/BitPrecise/Legato.hs
--- a/SBVTestSuite/TestSuite/BitPrecise/Legato.hs
+++ b/SBVTestSuite/TestSuite/BitPrecise/Legato.hs
@@ -33,11 +33,11 @@
                        flagC   <- free "flagC"
                        flagZ   <- free "flagZ"
                        output $ legatoIsCorrect (mkSFunArray (const 0)) (addrX, x) (addrY, y) addrLow (regX, regA, flagC, flagZ)
-       legatoC = compileToC' "legatoMult" $ do
+       legatoC = snd <$> compileToC' "legatoMult" (do
                     cgSetDriverValues [87, 92]
                     cgPerformRTCs True
                     x <- cgInput "x"
                     y <- cgInput "y"
                     let (hi, lo) = runLegato (0, x) (1, y) 2 (initMachine (mkSFunArray (const 0)) (0, 0, false, false))
                     cgOutput "hi" hi
-                    cgOutput "lo" lo
+                    cgOutput "lo" lo)
diff --git a/SBVTestSuite/TestSuite/BitPrecise/MergeSort.hs b/SBVTestSuite/TestSuite/BitPrecise/MergeSort.hs
--- a/SBVTestSuite/TestSuite/BitPrecise/MergeSort.hs
+++ b/SBVTestSuite/TestSuite/BitPrecise/MergeSort.hs
@@ -21,7 +21,7 @@
 tests = testGroup "BitPrecise.MergeSort" [
    goldenVsStringShow "merge" mergeC
  ]
- where mergeC = compileToC' "merge" $ do
+ where mergeC = snd <$> compileToC' "merge" (do
                    cgSetDriverValues [10, 6, 4, 82, 71]
                    xs <- cgInputArr 5 "xs"
-                   cgOutputArr "ys" (mergeSort xs)
+                   cgOutputArr "ys" (mergeSort xs))
diff --git a/SBVTestSuite/TestSuite/CodeGeneration/AddSub.hs b/SBVTestSuite/TestSuite/CodeGeneration/AddSub.hs
--- a/SBVTestSuite/TestSuite/CodeGeneration/AddSub.hs
+++ b/SBVTestSuite/TestSuite/CodeGeneration/AddSub.hs
@@ -21,11 +21,11 @@
 tests = testGroup "CodeGen.addSub" [
    goldenVsStringShow "addSub" code
  ]
- where code = compileToC' "addSub" $ do
+ where code = snd <$> compileToC' "addSub" (do
                 cgSetDriverValues [76, 92]
                 cgPerformRTCs True
                 x <- cgInput "x"
                 y <- cgInput "y"
                 let (s, d) = addSub x y
                 cgOutput "sum" s
-                cgOutput "dif" d
+                cgOutput "dif" d)
diff --git a/SBVTestSuite/TestSuite/CodeGeneration/CRC_USB5.hs b/SBVTestSuite/TestSuite/CodeGeneration/CRC_USB5.hs
--- a/SBVTestSuite/TestSuite/CodeGeneration/CRC_USB5.hs
+++ b/SBVTestSuite/TestSuite/CodeGeneration/CRC_USB5.hs
@@ -22,7 +22,7 @@
    goldenVsStringShow "crcUSB5_1" $ genC crcUSB
  , goldenVsStringShow "crcUSB5_2" $ genC crcUSB'
  ]
- where genC f = compileToC' "crcUSB5" $ do
+ where genC f = snd <$> compileToC' "crcUSB5" (do
                    cgSetDriverValues [0xFEDC]
                    msg <- cgInput "msg"
-                   cgReturn $ f msg
+                   cgReturn $ f msg)
diff --git a/SBVTestSuite/TestSuite/CodeGeneration/CgTests.hs b/SBVTestSuite/TestSuite/CodeGeneration/CgTests.hs
--- a/SBVTestSuite/TestSuite/CodeGeneration/CgTests.hs
+++ b/SBVTestSuite/TestSuite/CodeGeneration/CgTests.hs
@@ -24,18 +24,18 @@
  , goldenVsStringShow "selUnchecked" $ genSelect False "selUnChecked"
  , goldenVsStringShow "codeGen1"       foo
  ]
- where genSelect b n = compileToC' n $ do
+ where genSelect b n = snd <$> compileToC' n (do
                          cgSetDriverValues [65]
                          cgPerformRTCs b
                          let sel :: SWord8 -> SWord8
                              sel x = select [1, x+2] 3 x
                          x <- cgInput "x"
-                         cgReturn $ sel x
-       foo = compileToC' "foo" $ do
+                         cgReturn $ sel x)
+       foo = snd <$> compileToC' "foo" (do
                         cgSetDriverValues $ repeat 0
                         (x::SInt16)    <- cgInput "x"
                         (ys::[SInt64]) <- cgInputArr 45 "xArr"
                         cgOutput "z" (5 :: SWord16)
                         cgOutputArr "zArr" (replicate 7 (x+1))
                         cgOutputArr "yArr" ys
-                        cgReturn (x*2)
+                        cgReturn (x*2))
diff --git a/SBVTestSuite/TestSuite/CodeGeneration/Fibonacci.hs b/SBVTestSuite/TestSuite/CodeGeneration/Fibonacci.hs
--- a/SBVTestSuite/TestSuite/CodeGeneration/Fibonacci.hs
+++ b/SBVTestSuite/TestSuite/CodeGeneration/Fibonacci.hs
@@ -22,7 +22,7 @@
    goldenVsStringShow "fib1" $ tst [12] "fib1" (fib1 64)
  , goldenVsStringShow "fib2" $ tst [20] "fib2" (fib2 64)
  ]
- where tst vs nm f = compileToC' nm $ do cgPerformRTCs True
-                                         cgSetDriverValues vs
-                                         n <- cgInput "n"
-                                         cgReturn $ f n
+ where tst vs nm f = snd <$> compileToC' nm (do cgPerformRTCs True
+                                                cgSetDriverValues vs
+                                                n <- cgInput "n"
+                                                cgReturn $ f n)
diff --git a/SBVTestSuite/TestSuite/CodeGeneration/Floats.hs b/SBVTestSuite/TestSuite/CodeGeneration/Floats.hs
--- a/SBVTestSuite/TestSuite/CodeGeneration/Floats.hs
+++ b/SBVTestSuite/TestSuite/CodeGeneration/Floats.hs
@@ -20,7 +20,7 @@
 tests = testGroup "CodeGeneration.Floats" [
    goldenVsStringShow "floats_cgen" code
  ]
- where code  = compileToCLib' "floatCodeGen" cases
+ where code  = snd <$> compileToCLib' "floatCodeGen" cases
 
        setup = do cgSRealType CgLongDouble
                   cgIntegerSize 64
diff --git a/SBVTestSuite/TestSuite/CodeGeneration/GCD.hs b/SBVTestSuite/TestSuite/CodeGeneration/GCD.hs
--- a/SBVTestSuite/TestSuite/CodeGeneration/GCD.hs
+++ b/SBVTestSuite/TestSuite/CodeGeneration/GCD.hs
@@ -21,8 +21,8 @@
 tests = testGroup "CodeGeneration.GCD" [
    goldenVsStringShow "gcd" gcdC
  ]
- where gcdC = compileToC' "sgcd" $ do
+ where gcdC = snd <$> compileToC' "sgcd" (do
                 cgSetDriverValues [55,154]
                 x <- cgInput "x"
                 y <- cgInput "y"
-                cgReturn $ sgcd x y
+                cgReturn $ sgcd x y)
diff --git a/SBVTestSuite/TestSuite/CodeGeneration/PopulationCount.hs b/SBVTestSuite/TestSuite/CodeGeneration/PopulationCount.hs
--- a/SBVTestSuite/TestSuite/CodeGeneration/PopulationCount.hs
+++ b/SBVTestSuite/TestSuite/CodeGeneration/PopulationCount.hs
@@ -19,8 +19,8 @@
 -- Test suite
 tests :: TestTree
 tests = testGroup "CodeGeneration.PopulationCount" [
-   goldenVsStringShow "popCount1" $ genC False
- , goldenVsStringShow "popCount2" $ genC True
+   goldenVsStringShow "popCount1" $ snd <$> genC False
+ , goldenVsStringShow "popCount2" $ snd <$> genC True
  ]
  where genC b = compileToC' "popCount" $ do
                   cgSetDriverValues [0x0123456789ABCDEF]
diff --git a/SBVTestSuite/TestSuite/CodeGeneration/Uninterpreted.hs b/SBVTestSuite/TestSuite/CodeGeneration/Uninterpreted.hs
--- a/SBVTestSuite/TestSuite/CodeGeneration/Uninterpreted.hs
+++ b/SBVTestSuite/TestSuite/CodeGeneration/Uninterpreted.hs
@@ -21,7 +21,6 @@
 tests = testGroup "CodeGeneration.Uninterpreted" [
    goldenVsStringShow "cgUninterpret"  genC
  ]
- where genC = compileToC' "tstShiftLeft" $ do
-                  cgSetDriverValues [1, 2, 3]
-                  [x, y, z] <- cgInputArr 3 "vs"
-                  cgReturn $ tstShiftLeft x y z
+ where genC = snd <$> compileToC' "tstShiftLeft" (do cgSetDriverValues [1, 2, 3]
+                                                     [x, y, z] <- cgInputArr 3 "vs"
+                                                     cgReturn $ tstShiftLeft x y z)
diff --git a/SBVTestSuite/TestSuite/Crypto/AES.hs b/SBVTestSuite/TestSuite/Crypto/AES.hs
--- a/SBVTestSuite/TestSuite/Crypto/AES.hs
+++ b/SBVTestSuite/TestSuite/Crypto/AES.hs
@@ -19,9 +19,9 @@
 -- Test suite
 tests :: TestTree
 tests = testGroup "Crypto.AES" [
-   goldenVsStringShow "aes128Enc" $ compileToC'    "aes128Enc" (aes128EncDec True)
- , goldenVsStringShow "aes128Dec" $ compileToC'    "aes128Dec" (aes128EncDec False)
- , goldenVsStringShow "aes128Lib" $ compileToCLib' "aes128Lib" aes128Comps
+   goldenVsStringShow "aes128Enc" $ snd <$> compileToC'    "aes128Enc" (aes128EncDec True)
+ , goldenVsStringShow "aes128Dec" $ snd <$> compileToC'    "aes128Dec" (aes128EncDec False)
+ , goldenVsStringShow "aes128Lib" $ snd <$> compileToCLib' "aes128Lib" aes128Comps
  ]
  where aes128EncDec d = do pt  <- cgInputArr 4 "pt"
                            key <- cgInputArr 4 "key"
diff --git a/SBVTestSuite/Utils/SBVTestFramework.hs b/SBVTestSuite/Utils/SBVTestFramework.hs
--- a/SBVTestSuite/Utils/SBVTestFramework.hs
+++ b/SBVTestSuite/Utils/SBVTestFramework.hs
@@ -53,9 +53,9 @@
 import Data.SBV
 import Data.SBV.Control
 
-import Data.Char (chr, ord, isDigit)
-
-import Data.Maybe(fromMaybe, catMaybes)
+import Data.Char  (chr, ord, isDigit)
+import Data.List  (zip3)
+import Data.Maybe (fromMaybe, catMaybes)
 
 import System.FilePath ((</>), (<.>))
 
@@ -127,15 +127,34 @@
          cmp x y
           | cleanUp x == cleanUp y = return Nothing
           | True                   = return $ Just $ unlines $ [ "Discrepancy found. Expected: " ++ ref
-                                                                 , "============================================"
-                                                                 ]
-                                                              ++ lines xs
-                                                              ++ [ "Got: " ++ new
-                                                                 , "============================================"
-                                                                 ]
-                                                              ++ lines ys
+                                                               , "============================================"
+                                                               ]
+                                                            ++ lxs
+                                                            ++ [ "Got: " ++ new
+                                                               , "============================================"
+                                                               ]
+                                                            ++ lys
+                                                            ++ [ "Diff: "
+                                                               , "============================================"
+                                                               ]
+                                                            ++ diff
           where xs = map (chr . fromIntegral) $ BS.unpack x
                 ys = map (chr . fromIntegral) $ BS.unpack y
+
+                lxs = lines xs
+                lys = lines ys
+
+                diffLen = length lxs `max` length lys
+                diff    = concatMap pick $ zip3 [1..diffLen] (lxs ++ repeat "") (lys ++ repeat "")
+
+                pick (i, expected, got)
+                  | expected == got
+                  = []
+                  | True
+                  = [ "== Line " ++ show i ++ " =="
+                    , "  Expected: " ++ show expected
+                    , "  Got     : " ++ show got
+                    ]
 
          -- deal with insane Windows \r stuff
          cleanUp = BS.filter (/= slashr)
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,5 +1,5 @@
 Name:          sbv
-Version:       7.7
+Version:       7.8
 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
 Synopsis:      SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
 Description:   Express properties about Haskell programs and automatically prove them using SMT
@@ -16,7 +16,7 @@
 Bug-reports:   http://github.com/LeventErkok/sbv/issues
 Maintainer:    Levent Erkok (erkokl@gmail.com)
 Build-Type:    Simple
-Cabal-Version: >= 1.14
+Cabal-Version: 1.14
 Data-Files: SBVTestSuite/GoldFiles/*.gold
 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md
 
@@ -95,6 +95,7 @@
                   , Documentation.SBV.Examples.Puzzles.DogCatMouse
                   , Documentation.SBV.Examples.Puzzles.Euler185
                   , Documentation.SBV.Examples.Puzzles.Fish
+                  , Documentation.SBV.Examples.Puzzles.HexPuzzle
                   , Documentation.SBV.Examples.Puzzles.MagicSquare
                   , Documentation.SBV.Examples.Puzzles.NQueens
                   , Documentation.SBV.Examples.Puzzles.SendMoreMoney