diff --git a/CHANGES.md b/CHANGES.md
new file mode 100644
--- /dev/null
+++ b/CHANGES.md
@@ -0,0 +1,10 @@
+* Hackage: <http://hackage.haskell.org/package/sbvPlugin>
+* GitHub:  <http://github.com/LeventErkok/sbvPlugin>
+
+* Latest Hackage released version: 0.1, 2015-12-06
+
+### Version 0.1, 2015-12-06
+
+  * Basic functionality. Initial design exploration. The plugin
+    is mostly functional, but there are rough edges around
+    the details. Please report any issues you might find!
diff --git a/COPYRIGHT b/COPYRIGHT
new file mode 100644
--- /dev/null
+++ b/COPYRIGHT
@@ -0,0 +1,5 @@
+Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com)
+All rights reserved.
+
+The sbvPlugin is distributed with the BSD3 license. See the LICENSE file
+for details.
diff --git a/Data/SBV/Plugin.hs b/Data/SBV/Plugin.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Plugin.hs
@@ -0,0 +1,61 @@
+---------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Plugin
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- (The sbvPlugin is hosted at <http://github.com/LeventErkok/sbvPlugin>.
+-- Comments, bug reports, and patches are always welcome.)
+--
+-- SBVPlugin: A GHC Plugin for SBV, SMT Based Verification
+--
+-- <http://github.com/LeventErkok/sbv SBV> is a library for express properties about Haskell programs and
+-- automatically proving them using SMT solvers. The SBVPlugin allows
+-- simple annotations on Haskell functions to prove them directly during
+-- GHC compilation time.
+--
+-- Consider the following simple program:
+--
+--  > {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
+--  >
+--  > module Test where
+--  >
+--  > import Data.SBV.Plugin
+--  >
+--  > {-# ANN test theorem #-}
+--  > test :: Integer -> Integer -> Bool
+--  > test x y = x + y >= x - y
+--
+-- We have:
+--
+--  > $ ghc -c Test.hs
+--  >
+--  > [SBV] Test.hs:9:1-4 Proving "test", using Z3.
+--  > [Z3] Falsifiable. Counter-example:
+--  >   x =  0 :: Integer
+--  >   y = -1 :: Integer
+--  > [SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+--
+-- Note that the compilation will be aborted, since the theorem doesn't hold. As shown in the hint, GHC
+-- can be instructed to continue in that case, using an annotation of the form:
+--
+-- > {-# ANN test theorem {options = [IgnoreFailure]} #-}
+--
+-- The plugin should work from GHCi with no changes.  Note that when run from GHCi, the plugin will
+-- behave as if the /IgnoreFailure/ option is given on all annotations, so that failures do not stop
+-- the load process.
+---------------------------------------------------------------------------------
+module Data.SBV.Plugin(
+       -- * Entry point
+         plugin
+       -- * Annotations
+       , SBVAnnotation(..)
+       , sbv, theorem
+       -- * Plugin options
+       , SBVOption(..)
+       ) where
+
+import Data.SBV.Plugin.Plugin
+import Data.SBV.Plugin.Data
diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Plugin/Analyze.hs
@@ -0,0 +1,367 @@
+---------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Plugin.Analyze
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Walk the GHC Core, proving theorems/checking safety as they are found
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE NamedFieldPuns       #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Data.SBV.Plugin.Analyze (analyzeBind) where
+
+import GhcPlugins
+
+import Control.Monad.Reader
+import System.Exit hiding (die)
+
+import Data.IORef
+
+import Data.Char  (isAlpha, isAlphaNum)
+import Data.List  (intercalate, partition, nub, sortBy)
+import Data.Maybe (isJust, listToMaybe)
+import Data.Ord   (comparing)
+
+import qualified Data.Map as M
+
+import qualified Data.SBV           as S hiding (proveWith, proveWithAny)
+import qualified Data.SBV.Dynamic   as S
+import qualified Data.SBV.Internals as S
+
+import qualified Control.Exception as C
+
+import Data.SBV.Plugin.Common
+import Data.SBV.Plugin.Data
+
+-- | Dispatch the analyzer over bindings
+analyzeBind :: Config -> CoreBind -> CoreM ()
+analyzeBind cfg@Config{sbvAnnotation} = go
+  where go (NonRec b e) = bind (b, e)
+        go (Rec binds)  = mapM_ bind binds
+
+        bind (b, e) = mapM_ work (sbvAnnotation b)
+          where work (SBV opts)
+                 | Just s <- hasSkip opts  = liftIO $ putStrLn $ "[SBV] " ++ showSpan cfg b topLoc ++ " Skipping " ++ show (showSDoc (dflags cfg) (ppr b)) ++ ": " ++ s
+                 | Safety `elem` opts      = error "SBV: Safety pragma is not implemented yet"
+                 | Uninterpret `elem` opts = return ()
+                 | True                    = liftIO $ prove cfg opts b topLoc e
+                hasSkip opts = listToMaybe [s | Skip s <- opts]
+                topLoc       = bindSpan b
+
+-- | Prove an SBVTheorem
+prove :: Config -> [SBVOption] -> Var -> SrcSpan -> CoreExpr -> IO ()
+prove cfg@Config{isGHCi} opts b topLoc e = do
+        success <- safely $ proveIt cfg opts (topLoc, b) e
+        unless (success || isGHCi || IgnoreFailure `elem` opts) $ do
+            putStrLn $ "[SBV] Failed. (Use option '" ++ show IgnoreFailure ++ "' to continue.)" 
+            exitFailure
+
+-- | Safely execute an action, catching the exceptions, printing and returning False if something goes wrong
+safely :: IO Bool -> IO Bool
+safely a = a `C.catch` bad
+  where bad :: C.SomeException -> IO Bool
+        bad e = do print e
+                   return False
+
+instance Outputable S.Kind where
+   ppr = text . show
+
+instance Outputable Val where
+   ppr (Base s)   = text (show s)
+   ppr (Func k _) = text ("Func<" ++ show k ++ ">")
+
+-- | Returns True if proof went thru
+proveIt :: Config -> [SBVOption] -> (SrcSpan, Var) -> CoreExpr -> IO Bool
+proveIt cfg@Config{sbvAnnotation} opts (topLoc, topBind) topExpr = do
+        solverConfigs <- pickSolvers opts
+        let verbose = Verbose    `elem` opts
+            qCheck  = QuickCheck `elem` opts
+            runProver prop
+              | qCheck = Left  `fmap` S.svQuickCheck prop
+              | True   = Right `fmap` S.proveWithAny [s{S.verbose = verbose} | s <- solverConfigs] prop
+            loc = "[SBV] " ++ showSpan cfg topBind topLoc
+            slvrTag = ", using " ++ tag ++ "."
+              where tag = case solverConfigs of
+                            []     -> "no solvers"  -- can't really happen
+                            [x]    -> show x
+                            [x, y] -> show x ++ " and " ++ show y
+                            xs     -> intercalate ", " (map show (init xs)) ++ ", and " ++ show (last xs)
+        putStrLn $ "\n" ++ loc ++ (if qCheck then " QuickChecking " else " Proving ") ++ show (sh topBind) ++ slvrTag
+        (finalResult, finalUninterps) <- do
+                        rUninterps     <- newIORef []
+                        rUnms          <- newIORef []
+                        rUItys         <- newIORef []
+                        finalResult    <- runProver (res rUninterps rUnms rUItys)
+                        finalUninterps <- readIORef rUninterps
+                        return (finalResult, finalUninterps)
+        case finalResult of
+          Right (solver, sres@(S.ThmResult smtRes)) -> do
+                let success = case smtRes of
+                                S.Unsatisfiable{} -> True
+                                S.Satisfiable{}   -> False
+                                S.Unknown{}       -> False   -- conservative
+                                S.ProofError{}    -> False   -- conservative
+                                S.TimeOut{}       -> False   -- conservative
+                putStr $ "[" ++ show solver ++ "] "
+                print sres
+
+                -- If proof failed and there are uninterpreted functions, print a warning:
+                let unintFuns = [p | (p@(_, t), _) <- nub $ sortBy (comparing (fst . fst)) finalUninterps, isJust (splitFunTy_maybe t)]
+                unless (success || null unintFuns) $ do
+                        let plu | length finalUninterps > 1 = "s:"
+                                | True                      = ":"
+                            shUI (e, t) = (showSDoc (dflags cfg) (ppr (getSrcSpan e)), sh e, sh t)
+                            ls   = map shUI unintFuns
+                            len1 = maximum (0 : [length s | (s, _, _) <- ls])
+                            len2 = maximum (0 : [length s | (_, s, _) <- ls])
+                            pad n s = take n (s ++ repeat ' ')
+                            put (a, b, c) = putStrLn $ "  [" ++ pad len1 a ++ "] " ++ pad len2 b ++ " :: " ++ c
+                        putStrLn $ "[SBV] Counter-example might be bogus due to uninterpreted constant" ++ plu
+                        mapM_ put ls
+
+                return success
+          Left success -> return success
+
+  where res uis unms uitys = do
+               v <- runReaderT (symEval topExpr) Env{ curLoc  = topLoc
+                                                    , flags          = dflags        cfg
+                                                    , rUninterpreted = uis
+                                                    , rUsedNames     = unms
+                                                    , rUITypes       = uitys
+                                                    , machWordSize   = wordSize      cfg
+                                                    , envMap         = knownFuns     cfg
+                                                    , baseTCs        = knownTCs      cfg
+                                                    , specMap        = knownSpecials cfg
+                                                    , coreMap        = allBinds      cfg
+                                                    }
+               case v of
+                 Base r -> return r
+                 Func{} -> error "Impossible happened. Final result reduced to a non-base value!"
+
+        die :: SrcSpan -> String -> [String] -> a
+        die loc w es = error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es
+          where marker = "[SBV] " ++ showSpan cfg topBind loc
+                tag s = marker ++ " " ++ s
+                tab s = replicate (length marker) ' ' ++  "    " ++ s
+
+        tbd :: String -> [String] -> Eval Val
+        tbd w ws = do Env{curLoc} <- ask
+                      die curLoc w ws
+
+        sh o = showSDoc (dflags cfg) (ppr o)
+
+        -- Given an alleged theorem, first establish it has the right type, and
+        -- then go ahead and evaluate it symbolicly after applying it to sufficient
+        -- number of symbolic arguments
+        symEval :: CoreExpr -> Eval Val
+        symEval e = do let (bs, body) = collectBinders e
+                       ats <- mapM (\b -> getBaseType (getSrcSpan b) (varType b) >>= \bt -> return (b, bt)) bs
+                       let mkVar ((b, k), mbN) = do v <- S.svMkSymVar Nothing k (mbN `mplus` Just (sh b))
+                                                    return ((b, k), Base v)
+                       sArgs <- mapM (lift . mkVar) (zip ats (concat [map Just ns | Names ns <- opts] ++ repeat Nothing))
+                       local (\env -> env{envMap = foldr (uncurry M.insert) (envMap env) sArgs}) (go body)
+
+        isUninterpretedBinding :: Var -> Bool
+        isUninterpretedBinding v = any (Uninterpret `elem`) [opt | SBV opt <- sbvAnnotation v]
+
+        go :: CoreExpr -> Eval Val
+        go e = tgo (exprType e) e
+
+        -- Main symbolic evaluator:
+        tgo :: Type -> CoreExpr -> Eval Val
+
+        -- tgo t e | trace ("--> " ++ show (sh (e, t))) False = undefined
+
+        tgo t (Var v) = do Env{envMap, coreMap, specMap} <- ask
+                           k <- getBaseType (getSrcSpan v) t
+                           case (v, k) `M.lookup` envMap of
+                             Just b  -> return b
+                             Nothing -> case v `M.lookup` coreMap of
+                                           Just b  -> if isUninterpretedBinding v
+                                                      then uninterpret t v
+                                                      else go b
+                                           Nothing -> case v `M.lookup` specMap of
+                                                       Just b  -> return b
+                                                       Nothing -> uninterpret t v
+
+        tgo t e@(Lit l) = do Env{machWordSize} <- ask
+                             case l of
+                               MachChar{}        -> unint
+                               MachStr{}         -> unint
+                               MachNullAddr      -> unint
+                               MachLabel{}       -> unint
+                               MachInt      i    -> return $ Base $ S.svInteger (S.KBounded True  machWordSize) i
+                               MachInt64    i    -> return $ Base $ S.svInteger (S.KBounded True  64          ) i
+                               MachWord     i    -> return $ Base $ S.svInteger (S.KBounded False machWordSize) i
+                               MachWord64   i    -> return $ Base $ S.svInteger (S.KBounded False 64          ) i
+                               MachFloat    f    -> return $ Base $ S.svFloat   (fromRational f)
+                               MachDouble   d    -> return $ Base $ S.svDouble  (fromRational d)
+                               LitInteger   i it -> do k <- getBaseType noSrcSpan it
+                                                       return $ Base $ S.svInteger k i
+                  where unint = do Env{flags} <- ask
+                                   k  <- getBaseType noSrcSpan t
+                                   nm <- mkValidName "lit" (showSDoc flags (ppr e))
+                                   return $ Base $ S.svUninterpreted k nm Nothing []
+
+        tgo tFun (App (App (Var v) (Type t)) (Var dict))
+           | isReallyADictionary dict = do Env{envMap} <- ask
+                                           k <- getBaseType (getSrcSpan v) t
+                                           case (v, k) `M.lookup` envMap of
+                                              Just b -> return b
+                                              _      -> uninterpret tFun v
+        tgo t (App a (Type _))
+           = tgo t a
+
+        tgo _ (App f e)
+           = do func <- go f
+                arg  <- go e
+                let ok (S.KUserSort s1 _) (S.KUserSort s2 _) = s1 == s2
+                    ok k1                 k2                 = k1 == k2
+                case (func, arg) of
+                  (Func (k, _) sf, Base sv) | S.kindOf sv `ok` k -> sf sv
+                  (_,              Func{})                       -> tbd "Unsupported higher-order application" [sh f, sh e]
+                  _                                              -> error $ "[SBV] Impossible happened. Got an application with mismatched types: "
+                                                                            ++ sh [(f, func), (e, arg)]
+
+        tgo _ (Lam b body) = do
+            k <- getBaseType (getSrcSpan b) (varType b)
+            return $ Func (k, Just (sh b)) $ \s -> local (\env -> env{envMap = M.insert (b, k) (Base s) (envMap env)}) (go body)
+
+        tgo _ (Let (NonRec b e) body) = do
+            k <- getBaseType (getSrcSpan b) (varType b)
+            v <- go e
+            local (\env -> env{envMap = M.insert (b, k) v (envMap env)}) (go body)
+
+        tgo _ e@(Let _ _)
+           = tbd "Unsupported let-binding with a recursive binder" [sh e]
+
+        -- Case expressions. We take advantage of the core-invariant that each case alternative
+        -- is exhaustive; and DEFAULT (if present) is the first alternative. We turn it into a
+        -- simple if-then-else chain with the last element on the DEFAULT, or whatever comes last.
+        tgo _ e@(Case ce _b _t alts)
+           = do sce <- go ce
+                let isDefault (DEFAULT, _, _) = True
+                    isDefault _               = False
+                    (nonDefs, defs) = partition isDefault alts
+                    walk [(_, _, rhs)]        = go rhs
+                    walk ((p, _, rhs) : rest) = case sce of
+                                                   Base a -> do mr <- match a p
+                                                                case mr of
+                                                                  Just m  -> choose m (go rhs) (walk rest)
+                                                                  Nothing -> caseTooComplicated "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs]
+                                                   _      -> caseTooComplicated "with-non-base-scrutinee" []
+                    walk []                     = caseTooComplicated "with-non-exhaustive-match" []  -- can't really happen
+                walk (nonDefs ++ defs)
+           where caseTooComplicated w [] = tbd ("Unsupported case-expression (" ++ w ++ ")") [sh e]
+                 caseTooComplicated w xs = tbd ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs
+                 choose t tb fb = case S.svAsBool t of
+                                     Nothing    -> do stb <- tb
+                                                      sfb <- fb
+                                                      case (stb, sfb) of
+                                                        (Base a, Base b) -> return $ Base $ S.svIte t a b
+                                                        _                -> caseTooComplicated "with-non-base-alternatives" []
+                                     Just True  -> tb
+                                     Just False -> fb
+                 match :: S.SVal -> AltCon -> Eval (Maybe S.SVal)
+                 match a c = case c of
+                               DEFAULT    -> return $ Just S.svTrue
+                               LitAlt  l  -> do le <- go (Lit l)
+                                                case le of
+                                                  Base b -> return $ Just $ a `S.svEqual` b
+                                                  Func{} -> return Nothing
+                               DataAlt dc -> do Env{specMap} <- ask
+                                                case dataConWorkId dc `M.lookup` specMap of
+                                                  Just (Base b) -> return $ Just $ a `S.svEqual` b
+                                                  _             -> return Nothing
+
+        tgo t (Cast e _)
+           = tgo t e
+
+        tgo _ (Tick t e)
+           = local (\envMap -> envMap{curLoc = tickSpan t (curLoc envMap)}) $ go e
+
+        tgo _ e@(Type{})
+           = tbd "Unsupported type-expression" [sh e]
+
+        tgo _ e@(Coercion{})
+           = tbd "Unsupported coercion-expression" [sh e]
+
+-- | Uninterpret an expression
+uninterpret :: Type -> Var -> Eval Val
+uninterpret t v = do
+          let (args, res) = splitFunTys t
+              sp          = getSrcSpan v
+          argKs <- mapM (getBaseType sp) args
+          resK  <- getBaseType sp res
+          Env{flags, rUninterpreted} <- ask
+          uis <- liftIO $ readIORef rUninterpreted
+          nm <- case (v, t) `lookup` uis of
+                 Just nm -> return nm
+                 Nothing -> do nm <- mkValidName "expr" $ showSDoc flags (ppr v)
+                               liftIO $ modifyIORef rUninterpreted (((v, t), nm) :)
+                               return nm
+          return $ walk argKs (nm, resK) []
+  where walk []     (nm, k) args = Base $ S.svUninterpreted k nm Nothing (reverse args)
+        walk (a:as) nmk     args = Func (a, Nothing) $ \p -> return (walk as nmk (p:args))
+
+-- not every name is good, sigh
+mkValidName :: String -> String -> Eval String
+mkValidName origin origName =
+        do Env{rUsedNames} <- ask
+           usedNames <- liftIO $ readIORef rUsedNames
+           let name = if null origName || origName `elem` S.smtLibReservedNames
+                      then "sbvPlugin_" ++ origin ++ "_" ++ origName
+                      else origName
+               nm = genSym usedNames name
+           liftIO $ modifyIORef rUsedNames (nm :)
+           return $ escape nm
+  where genSym bad nm
+          | nm `elem` bad = head [nm' | i <- [(0::Int) ..], let nm' = nm ++ "_" ++ show i, nm' `notElem` bad]
+          | True          = nm
+        escape nm
+          | isAlpha (head nm) && all isGood (tail nm) = nm
+          | True                                      = "|" ++ map tr nm ++ "|"
+        isGood c = isAlphaNum c || c == '_'
+        tr '|'   = '_'
+        tr '\\'  = '_'
+        tr c     = c
+
+-- | Is this variable really a dictionary?
+isReallyADictionary :: Var -> Bool
+isReallyADictionary v = case classifyPredType (varType v) of
+                          ClassPred{} -> True
+                          EqPred{}    -> True
+                          TuplePred{} -> True
+                          IrredPred{} -> False
+
+-- | Convert a Core type to an SBV kind, if known
+-- Otherwise, create an uninterpreted kind, and return that.
+getBaseType :: SrcSpan -> Type -> Eval S.Kind
+getBaseType sp t = do
+        Env{baseTCs} <- ask
+        case grabTCs (splitTyConApp_maybe t) of
+          Just k -> case k `M.lookup` baseTCs of
+                      Just knd -> return knd
+                      Nothing  -> unknown
+          _        -> unknown
+  where -- allow one level of nesting
+        grabTCs Nothing          = Nothing
+        grabTCs (Just (top, ts)) = do as <- walk ts []
+                                      return (top, as)
+        walk []     sofar = Just $ reverse sofar
+        walk (a:as) sofar = case splitTyConApp_maybe a of
+                               Just (ac, []) -> walk as (ac:sofar)
+                               _             -> Nothing
+        -- Check if we uninterpreted this before; if so, return it, otherwise create a new one
+        unknown = do Env{flags, rUITypes} <- ask
+                     uiTypes <- liftIO $ readIORef rUITypes
+                     case t `lookup` uiTypes of
+                       Just k  -> return k
+                       Nothing -> do nm <- mkValidName "type" $ showSDoc flags (ppr t)
+                                     let k = S.KUserSort nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp)
+                                     liftIO $ modifyIORef rUITypes ((t, k) :)
+                                     return k
diff --git a/Data/SBV/Plugin/Common.hs b/Data/SBV/Plugin/Common.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Plugin/Common.hs
@@ -0,0 +1,88 @@
+---------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Plugin.Common
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Common data-structures/utilities
+-----------------------------------------------------------------------------
+
+module Data.SBV.Plugin.Common where
+
+import Control.Monad.Reader
+
+import CostCentre
+import GhcPlugins
+
+import Data.Maybe (mapMaybe)
+import qualified Data.Map as M
+
+import Data.IORef
+
+import qualified Data.SBV         as S
+import qualified Data.SBV.Dynamic as S
+
+import Data.SBV.Plugin.Data
+
+-- | Interpreter environment
+data Env = Env { curLoc         :: SrcSpan
+               , flags          :: DynFlags
+               , machWordSize   :: Int
+               , rUninterpreted :: IORef [((Var, Type), String)]
+               , rUsedNames     :: IORef [String]
+               , rUITypes       :: IORef [(Type, S.Kind)]
+               , baseTCs        :: M.Map (TyCon, [TyCon]) S.Kind
+               , envMap         :: M.Map (Var, S.Kind)    Val
+               , specMap        :: M.Map Var              Val
+               , coreMap        :: M.Map Var              CoreExpr
+               }
+
+-- | The interpreter monad
+type Eval a = ReaderT Env S.Symbolic a
+
+-- | Configuration info as we run the plugin
+data Config = Config { dflags        :: DynFlags
+                     , wordSize      :: Int
+                     , isGHCi        :: Bool
+                     , opts          :: [SBVAnnotation]
+                     , knownTCs      :: M.Map (TyCon, [TyCon]) S.Kind
+                     , knownFuns     :: M.Map (Var, S.Kind)    Val
+                     , knownSpecials :: M.Map Var Val
+                     , sbvAnnotation :: Var -> [SBVAnnotation]
+                     , allBinds      :: M.Map Var CoreExpr
+                     }
+
+-- | Given the user options, determine which solver(s) to use
+pickSolvers :: [SBVOption] -> IO [S.SMTConfig]
+pickSolvers slvrs
+  | AnySolver `elem` slvrs = S.sbvAvailableSolvers
+  | True                   = case mapMaybe (`lookup` solvers) slvrs of
+                                [] -> return [S.defaultSMTCfg]
+                                xs -> return xs
+  where solvers = [ (Z3,        S.z3)
+                  , (Yices,     S.yices)
+                  , (Boolector, S.boolector)
+                  , (CVC4,      S.cvc4)
+                  , (MathSAT,   S.mathSAT)
+                  , (ABC,       S.abc)
+                  ]
+
+-- | The values kept track of by the interpreter
+data Val = Base S.SVal
+         | Func (S.Kind, Maybe String) (S.SVal -> Eval Val)
+
+-- | Compute the span given a Tick. Returns the old-span if the tick span useless.
+tickSpan :: Tickish t -> SrcSpan -> SrcSpan
+tickSpan (ProfNote cc _ _) _ = cc_loc cc
+tickSpan (SourceNote s _)  _ = RealSrcSpan s
+tickSpan _                 s = s
+
+-- | Compute the span for a binding.
+bindSpan :: Var -> SrcSpan
+bindSpan = nameSrcSpan . varName
+
+-- | Show a GHC span in user-friendly form.
+showSpan :: Config -> Var -> SrcSpan -> String
+showSpan cfg b s = showSDoc (dflags cfg) $ if isGoodSrcSpan s then ppr s else ppr b
diff --git a/Data/SBV/Plugin/Data.hs b/Data/SBV/Plugin/Data.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Plugin/Data.hs
@@ -0,0 +1,48 @@
+---------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Plugin.Data
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Internal data-structures for the sbvPlugin
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DeriveDataTypeable #-}
+
+module Data.SBV.Plugin.Data where
+
+import Data.Data  (Data, Typeable)
+
+-- | Plugin options. Note that we allow picking multiple solvers, which
+-- will all be run in parallel. If you want to run all available solvers,
+-- use the option 'AnySolver'. The default is to error-out on failure, using
+-- the default-SMT solver picked by SBV, which is currently Z3.
+data SBVOption = IgnoreFailure  -- ^ Continue even if proof fails
+               | Skip String    -- ^ Skip the proof. Can be handy for properties that we currently do not want to focus on.
+               | Verbose        -- ^ Produce verbose output, good for debugging
+               | Safety         -- ^ Check for safety
+               | QuickCheck     -- ^ Perform quickCheck
+               | Uninterpret    -- ^ Uninterpret this binding for proof purposes
+               | Names [String] -- ^ Use these names for the arguments; need not be exhaustive
+               | Z3             -- ^ Use Z3
+               | Yices          -- ^ Use Yices
+               | Boolector      -- ^ Use Boolector
+               | CVC4           -- ^ Use CVC4
+               | MathSAT        -- ^ Use MathSAT
+               | ABC            -- ^ Use ABC
+               | AnySolver      -- ^ Use all installed solvers
+               deriving (Show, Eq, Data, Typeable)
+
+-- | The actual annotation.
+newtype SBVAnnotation = SBV {options :: [SBVOption]}
+                      deriving (Eq, Data, Typeable)
+
+-- | A property annotation, using default options.
+sbv :: SBVAnnotation
+sbv = SBV {options = []}
+
+-- | Synonym for sbv really, just looks cooler
+theorem :: SBVAnnotation
+theorem = sbv
diff --git a/Data/SBV/Plugin/Env.hs b/Data/SBV/Plugin/Env.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Plugin/Env.hs
@@ -0,0 +1,166 @@
+---------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Plugin.Env
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- The environment for mapping concrete functions/types to symbolic ones.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE MagicHash       #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Data.SBV.Plugin.Env (buildFunEnv, buildTCEnv, buildSpecialEnv) where
+
+import GhcPlugins
+import GHC.Types
+
+import qualified Data.Map            as M
+import qualified Language.Haskell.TH as TH
+
+import Data.Int
+import Data.Word
+import Data.Bits
+import Data.Maybe (fromMaybe)
+import Data.Ratio
+
+import qualified Data.SBV         as S hiding (proveWith, proveWithAny)
+import qualified Data.SBV.Dynamic as S
+
+import Data.SBV.Plugin.Common
+
+-- | Build the initial environment containing types
+buildTCEnv :: Int -> CoreM (M.Map (TyCon, [TyCon]) S.Kind)
+buildTCEnv isz = do xs <- mapM grabTyCon basics
+                    ys <- mapM grabTyApp apps
+                    return $ M.fromList $ xs ++ ys
+
+  where grab x = do Just fn <- thNameToGhcName x
+                    lookupTyCon fn
+
+        grabTyCon (x, k) = grabTyApp (x, [], k)
+
+        grabTyApp (x, as, k) = do fn   <- grab x
+                                  args <- mapM grab as
+                                  return ((fn, args), k)
+
+        basics = [ (''Bool,    S.KBool)
+                 , (''Integer, S.KUnbounded)
+                 , (''Float,   S.KFloat)
+                 , (''Double,  S.KDouble)
+                 , (''Int,     S.KBounded True isz)
+                 , (''Int8,    S.KBounded True   8)
+                 , (''Int16,   S.KBounded True  16)
+                 , (''Int32,   S.KBounded True  32)
+                 , (''Int64,   S.KBounded True  64)
+                 , (''Word8,   S.KBounded False  8)
+                 , (''Word16,  S.KBounded False 16)
+                 , (''Word32,  S.KBounded False 32)
+                 , (''Word64,  S.KBounded False 64)
+                 ]
+
+        apps =  [ (''Ratio, [''Integer], S.KReal) ]
+
+-- | Build the initial environment containing functions
+buildFunEnv :: CoreM (M.Map (Id, S.Kind) Val)
+buildFunEnv = M.fromList `fmap` mapM grabVar symFuncs
+  where grabVar (n, k, sfn) = do Just fn <- thNameToGhcName n
+                                 f <- lookupId fn
+                                 return ((f, k), sfn)
+
+-- | Special functions that have a fixed-type
+buildSpecialEnv :: Int -> CoreM (M.Map Id Val)
+buildSpecialEnv wsz = M.fromList `fmap`  mapM grabVar basics
+   where grabVar (n, sfn) = do Just fn <- thNameToGhcName n
+                               f <- lookupId fn
+                               return (f, sfn)
+
+         basics = [ ('F#,    Func  (S.KFloat,  Nothing)            (return . Base))
+                  , ('D#,    Func  (S.KDouble, Nothing)            (return . Base))
+                  , ('I#,    Func  (S.KBounded True  wsz, Nothing) (return . Base))
+                  , ('W#,    Func  (S.KBounded False wsz, Nothing) (return . Base))
+                  , ('True,  Base  S.svTrue)
+                  , ('False, Base  S.svFalse)
+                  , ('(&&),  lift2 S.KBool S.svAnd)
+                  , ('(||),  lift2 S.KBool S.svOr)
+                  , ('not,   lift1 S.KBool S.svNot)
+                  ]
+
+-- | Symbolic functions supported by the plugin; those from a class.
+symFuncs :: [(TH.Name, S.Kind, Val)]
+symFuncs =  -- equality is for all kinds
+          [(op, k, lift2 k sOp) | k <- allKinds, (op, sOp) <- [('(==), S.svEqual), ('(/=), S.svNotEqual)]]
+
+          -- arithmetic
+       ++ [(op, k, lift1 k sOp) | k <- arithKinds, (op, sOp) <- unaryOps]
+       ++ [(op, k, lift2 k sOp) | k <- arithKinds, (op, sOp) <- binaryOps]
+
+          -- literal conversions from Integer
+       ++ [(op, k, lift1Int sOp) | k <- integerKinds, (op, sOp) <- [('fromInteger, S.svInteger k)]]
+
+          -- comparisons
+       ++ [(op, k, lift2 k sOp) | k <- arithKinds, (op, sOp) <- compOps ]
+
+          -- integer div/rem
+      ++ [(op, k, lift2 k sOp) | k <- integralKinds, (op, sOp) <- [('div, S.svDivide), ('quot, S.svQuot), ('rem, S.svRem)]]
+
+         -- bit-vector
+      ++ [ (op, k, lift2 k sOp) | k <- bvKinds, (op, sOp) <- bvBinOps]
+
+ where
+       -- Bit-vectors
+       bvKinds    = [S.KBounded s sz | s <- [False, True], sz <- [8, 16, 32, 64]]
+
+       -- Those that are "integral"ish
+       integralKinds = S.KUnbounded : bvKinds
+
+       -- Those that can be converted from an Integer
+       integerKinds = S.KReal : integralKinds
+
+       -- Float kinds
+       floatKinds = [S.KFloat, S.KDouble]
+
+       -- All arithmetic kinds
+       arithKinds = floatKinds ++ integerKinds
+
+       -- Everything
+       allKinds   = S.KBool : arithKinds
+
+       -- Unary arithmetic ops
+       unaryOps   = [ ('abs,    S.svAbs)
+                    , ('negate, S.svUNeg)
+                    ]
+
+       -- Binary arithmetic ops
+       binaryOps  = [ ('(+), S.svPlus)
+                    , ('(-), S.svMinus)
+                    , ('(*), S.svTimes)
+                    , ('(/), S.svDivide)
+                    ]
+
+       -- Comparisons
+       compOps = [ ('(<),  S.svLessThan)
+                 , ('(>),  S.svGreaterThan)
+                 , ('(<=), S.svLessEq)
+                 , ('(>=), S.svGreaterEq)
+                 ]
+
+       -- Binary bit-vector ops
+       bvBinOps = [ ('(.&.), S.svAnd)
+                  , ('(.|.), S.svOr)
+                  , ('xor,   S.svXOr)
+                  ]
+
+-- | Lift a unary SBV function to the plugin value space
+lift1 :: S.Kind -> (S.SVal -> S.SVal) -> Val
+lift1 k f = Func (k, Nothing) $ return . Base . f
+
+-- | Lift a unary SBV function that takes and integer value to the plugin value space
+lift1Int :: (Integer -> S.SVal) -> Val
+lift1Int f = Func (S.KUnbounded, Nothing) $ \i -> return $ Base (f (fromMaybe (error ("Cannot extract an integer from value: " ++ show i)) (S.svAsInteger i)))
+
+-- | Lift a two argument SBV function to our the plugin value space
+lift2 :: S.Kind -> (S.SVal -> S.SVal -> S.SVal) -> Val
+lift2 k f = Func (k, Nothing) $ \a -> return $ Func (k, Nothing) $ \b -> return (Base (f a b))
diff --git a/Data/SBV/Plugin/Plugin.hs b/Data/SBV/Plugin/Plugin.hs
new file mode 100644
--- /dev/null
+++ b/Data/SBV/Plugin/Plugin.hs
@@ -0,0 +1,69 @@
+---------------------------------------------------------------------------
+-- |
+-- Module      :  Data.SBV.Plugin.Analyze
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Main entry point to the SBV Plugin
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE NamedFieldPuns #-}
+
+module Data.SBV.Plugin.Plugin(plugin) where
+
+import GhcPlugins
+import System.Exit
+
+import Data.Maybe (fromJust)
+import Data.List  (sortBy)
+import Data.Ord   (comparing)
+import Data.Bits  (bitSizeMaybe)
+
+import qualified Data.Map as M
+
+import Data.SBV.Plugin.Common
+import Data.SBV.Plugin.Env
+import Data.SBV.Plugin.Analyze (analyzeBind)
+
+-- | Entry point to the plugin
+plugin :: Plugin
+plugin = defaultPlugin {installCoreToDos = install}
+ where install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
+       install []   todos = reinitializeGlobals >> return (sbvPass : todos)
+       install opts _     = do liftIO $ putStrLn $ "[SBV] Unexpected command line options: " ++ show opts
+                               liftIO exitFailure
+
+       sbvPass = CoreDoPluginPass "SBV based analysis" pass
+
+       pass :: ModGuts -> CoreM ModGuts
+       pass guts@(ModGuts {mg_binds}) = do
+
+          df   <- getDynFlags
+          anns <- getAnnotations deserializeWithData guts
+
+          let wsz = fromJust (bitSizeMaybe (0::Int))
+
+          baseTCs      <- buildTCEnv wsz
+          baseEnv      <- buildFunEnv
+          baseSpecials <- buildSpecialEnv wsz
+
+          let cfg = Config { dflags        = df
+                           , opts          = []
+                           , wordSize      = wsz
+                           , isGHCi        = hscTarget df == HscInterpreted
+                           , knownTCs      = baseTCs
+                           , knownFuns     = baseEnv
+                           , knownSpecials = baseSpecials
+                           , sbvAnnotation = lookupWithDefaultUFM anns [] . varUnique
+                           , allBinds      = M.fromList (flattenBinds mg_binds)
+                           }
+
+          let bindLoc (NonRec b _)     = bindSpan b
+              bindLoc (Rec [])         = noSrcSpan
+              bindLoc (Rec ((b, _):_)) = bindSpan b
+
+          mapM_ (analyzeBind cfg) $ sortBy (comparing bindLoc) mg_binds
+
+          return guts
diff --git a/INSTALL b/INSTALL
new file mode 100644
--- /dev/null
+++ b/INSTALL
@@ -0,0 +1,8 @@
+The sbvPlugin can be installed simply by issuing cabal install:
+
+     cabal install sbvPlugin
+
+This will also install the SBV library if you do not already have it.
+You should also install an SMT solver, preferably the default solver
+used by SBV; i.e., Z3 from Microsoft: http://github.com/Z3Prover/z3.
+Please make sure that the "z3" executable is in your path.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+sbvPlugin: SMT based analyzer for Haskell
+
+Copyright (c) 2015, Levent Erkok (erkokl@gmail.com)
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+    * Neither the name of the developer (Levent Erkok) nor the
+      names of its contributors may be used to endorse or promote products
+      derived from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL LEVENT ERKOK BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,46 @@
+## SBVPlugin: SBV Plugin for GHC
+
+[![Hackage version](http://img.shields.io/hackage/v/sbvPlugin.svg?label=Hackage)](http://hackage.haskell.org/package/sbvPlugin)
+    [![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)](http://travis-ci.org/LeventErkok/sbvPlugin)
+
+### Example
+
+```haskell
+{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}
+
+module Test where
+
+import Data.SBV.Plugin
+
+{-# ANN test theorem #-}
+test :: Integer -> Integer -> Bool
+test x y = x + y >= x - y
+```
+
+*Note the GHC option on the very first line. Either decorate your file with
+this option, or pass `-fplugin=Data.SBV.Plugin` as an argument to GHC, either on the command line
+or via cabal. Same trick also works for GHCi.*
+
+When compiled or loaded in to ghci, we get:
+
+```
+$ ghc -c Test.hs
+
+[SBV] Test.hs:9:1-4 Proving "test", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x =  0 :: Integer
+  y = -1 :: Integer
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+```
+
+Note that the compilation will be aborted, since the theorem doesn't hold. As shown in the hint, GHC
+can be instructed to continue in that case, using an annotation of the form:
+
+```haskell
+{-# ANN test theorem {options = [IgnoreFailure]} #-}
+```
+
+### Using SBVPlugin from GHCi
+The plugin should work from GHCi with no changes.  Note that when run from GHCi, the plugin will
+behave as if the `IgnoreFailure` argument is given on all annotations, so that failures do not stop
+the load process.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal
new file mode 100644
--- /dev/null
+++ b/sbvPlugin.cabal
@@ -0,0 +1,42 @@
+Name              : sbvPlugin
+Version           : 0.1
+Category          : Formal methods, Theorem provers, Math, SMT, Symbolic Computation
+Synopsis          : Analyze Haskell expressions using SBV/SMT
+Description       : GHC plugin for analyzing expressions using SMT solvers, based
+                    on the <http://hackage.haskell.org/package/sbv SBV> package.
+                    .
+                    See "Data.SBV.Plugin" for a quick example.
+License           : BSD3
+License-file      : LICENSE
+Stability         : Experimental
+Author            : Levent Erkok
+Homepage          : http://github.com/LeventErkok/sbvPlugin
+Bug-reports       : http://github.com/LeventErkok/sbvPlugin/issues
+Maintainer        : Levent Erkok (erkokl@gmail.com)
+Build-Type        : Simple
+Cabal-Version     : >= 1.14
+Data-Files        : tests/GoldFiles/*.hs.golden
+Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md
+
+source-repository head
+    type:       git
+    location:   git://github.com/LeventErkok/sbvPlugin.git
+
+Library
+  default-language: Haskell2010
+  ghc-options     : -Wall
+  Exposed-modules : Data.SBV.Plugin
+  build-depends   : base >= 4.8 && < 5, ghc, ghc-prim, containers, sbv >= 5.6, mtl, template-haskell
+  Other-modules   : Data.SBV.Plugin.Analyze
+                  , Data.SBV.Plugin.Data
+                  , Data.SBV.Plugin.Common
+                  , Data.SBV.Plugin.Env
+                  , Data.SBV.Plugin.Plugin
+
+Test-Suite sbvPluginTests
+  type            : exitcode-stdio-1.0
+  default-language: Haskell2010
+  ghc-options     : -Wall
+  Build-depends   : base >= 4.8 && < 5, sbvPlugin, tasty, tasty-golden, filepath, process, directory
+  Hs-Source-Dirs  : tests
+  main-is         : Run.hs
diff --git a/tests/GoldFiles/T00.hs.golden b/tests/GoldFiles/T00.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T00.hs.golden
@@ -0,0 +1,8 @@
+
+[SBV] tests/T00.hs:12:1 Proving "f", using Z3.
+[Z3] Q.E.D.
+
+[SBV] tests/T00.hs:16:1 Proving "g", using Z3.
+[Z3] Falsifiable. Counter-example:
+  _x =     0 :: Int8
+  _y = False :: Bool
diff --git a/tests/GoldFiles/T01.hs.golden b/tests/GoldFiles/T01.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T01.hs.golden
@@ -0,0 +1,7 @@
+
+[SBV] tests/T01.hs:9:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x =  40959.98499298095 :: Double
+  y = -73732.00109529495 :: Double
+  z =  257.9890136271454 :: Double
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T02.hs.golden b/tests/GoldFiles/T02.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T02.hs.golden
@@ -0,0 +1,5 @@
+
+[SBV] tests/T02.hs:9:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x = 1 :: Integer
+  y = 0 :: Integer
diff --git a/tests/GoldFiles/T03.hs.golden b/tests/GoldFiles/T03.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T03.hs.golden
@@ -0,0 +1,3 @@
+
+[SBV] tests/T03.hs:10:1 Proving "f", using Z3.
+[Z3] Q.E.D.
diff --git a/tests/GoldFiles/T04.hs.golden b/tests/GoldFiles/T04.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T04.hs.golden
@@ -0,0 +1,3 @@
+
+[SBV] tests/T04.hs:10:1 Proving "f", using Z3.
+[Z3] Q.E.D.
diff --git a/tests/GoldFiles/T05.hs.golden b/tests/GoldFiles/T05.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T05.hs.golden
@@ -0,0 +1,5 @@
+
+[SBV] tests/T05.hs:9:1 Proving "f", using CVC4 and Yices.
+[Yices] Falsifiable. Counter-example:
+  x =  0 :: Integer
+  y = -1 :: Integer
diff --git a/tests/GoldFiles/T06.hs.golden b/tests/GoldFiles/T06.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T06.hs.golden
@@ -0,0 +1,5 @@
+
+[SBV] tests/T06.hs:10:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x = -128 :: Int8
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T07.hs.golden b/tests/GoldFiles/T07.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T07.hs.golden
@@ -0,0 +1,5 @@
+
+[SBV] tests/T07.hs:9:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x = NaN :: Double
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T08.hs.golden b/tests/GoldFiles/T08.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T08.hs.golden
@@ -0,0 +1,5 @@
+
+[SBV] tests/T08.hs:9:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x = 0.0 :: Double
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T09.hs.golden b/tests/GoldFiles/T09.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T09.hs.golden
@@ -0,0 +1,3 @@
+
+[SBV] tests/T09.hs:10:1 QuickChecking "f", using Z3.
+(0 tests)         (1 test)        (2 tests)         (3 tests)         (4 tests)         (5 tests)         (6 tests)         (7 tests)         (8 tests)         (9 tests)         (10 tests)          (11 tests)          (12 tests)          (13 tests)          (14 tests)          (15 tests)          (16 tests)          (17 tests)          (18 tests)          (19 tests)          (20 tests)          (21 tests)          (22 tests)          (23 tests)          (24 tests)          (25 tests)          (26 tests)          (27 tests)          (28 tests)          (29 tests)          (30 tests)          (31 tests)          (32 tests)          (33 tests)          (34 tests)          (35 tests)          (36 tests)          (37 tests)          (38 tests)          (39 tests)          (40 tests)          (41 tests)          (42 tests)          (43 tests)          (44 tests)          (45 tests)          (46 tests)          (47 tests)          (48 tests)          (49 tests)          (50 tests)          (51 tests)          (52 tests)          (53 tests)          (54 tests)          (55 tests)          (56 tests)          (57 tests)          (58 tests)          (59 tests)          (60 tests)          (61 tests)          (62 tests)          (63 tests)          (64 tests)          (65 tests)          (66 tests)          (67 tests)          (68 tests)          (69 tests)          (70 tests)          (71 tests)          (72 tests)          (73 tests)          (74 tests)          (75 tests)          (76 tests)          (77 tests)          (78 tests)          (79 tests)          (80 tests)          (81 tests)          (82 tests)          (83 tests)          (84 tests)          (85 tests)          (86 tests)          (87 tests)          (88 tests)          (89 tests)          (90 tests)          (91 tests)          (92 tests)          (93 tests)          (94 tests)          (95 tests)          (96 tests)          (97 tests)          (98 tests)          (99 tests)          +++ OK, passed 100 tests.
diff --git a/tests/GoldFiles/T10.hs.golden b/tests/GoldFiles/T10.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T10.hs.golden
@@ -0,0 +1,3 @@
+
+[SBV] tests/T10.hs:12:1 Proving "f", using Z3.
+[Z3] Q.E.D.
diff --git a/tests/GoldFiles/T11.hs.golden b/tests/GoldFiles/T11.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T11.hs.golden
@@ -0,0 +1,5 @@
+
+[SBV] tests/T11.hs:15:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x = 11 :: Integer
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T12.hs.golden b/tests/GoldFiles/T12.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T12.hs.golden
@@ -0,0 +1,6 @@
+
+[SBV] tests/T12.hs:9:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  i =     2 :: Integer
+  b = False :: Bool
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T13.hs.golden b/tests/GoldFiles/T13.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T13.hs.golden
@@ -0,0 +1,7 @@
+
+[SBV] tests/T13.hs:9:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  i =     2 :: Integer
+  d =   0.0 :: Double
+  b = False :: Bool
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T14.hs.golden b/tests/GoldFiles/T14.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T14.hs.golden
@@ -0,0 +1,5 @@
+
+[SBV] tests/T14.hs:10:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x = 1.0 :: Real
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T15.hs.golden b/tests/GoldFiles/T15.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T15.hs.golden
@@ -0,0 +1,51 @@
+
+[SBV] tests/T15.hs:11:1 Proving "f", using Z3.
+** Starting symbolic simulation..
+** Generated symbolic trace:
+SORTS
+  Age
+INPUTS
+  s0 :: Age, aliasing "age"
+CONSTANTS
+  s_2 = False :: Bool
+  s_1 = True :: Bool
+TABLES
+ARRAYS
+UNINTERPRETED CONSTANTS
+  [uninterpreted] ds_d6XY :: SInt64
+USER GIVEN CODE SEGMENTS
+AXIOMS
+DEFINE
+  s1 :: SInt64 = [uninterpreted] ds_d6XY
+CONSTRAINTS
+ASSERTIONS
+OUTPUTS
+  s_1
+** Translating to SMT-Lib..
+** Checking Theoremhood..
+** Generated SMTLib program:
+; Automatically generated by SBV. Do not edit.
+(set-option :produce-models true)
+; has user-defined sorts, no logic specified.
+; --- uninterpreted sorts ---
+(declare-sort Age 0)  ; N.B. Uninterpreted: originating from sbvPlugin: <no location info>
+; --- literal constants ---
+(define-fun s_2 () Bool false)
+(define-fun s_1 () Bool true)
+; --- skolem constants ---
+(declare-fun s0 () Age) ; tracks user variable "age"
+; --- constant tables ---
+; --- skolemized tables ---
+; --- arrays ---
+; --- uninterpreted constants ---
+(declare-fun ds_d6XY () (_ BitVec 64))
+; --- user given axioms ---
+; --- formula ---
+(assert ; no quantifiers
+   (let ((s1 ds_d6XY))
+   (not s_1)))
+** Calling: "z3 -nw -in -smt2"
+** Z3 output:
+unsat
+** Done..
+[Z3] Q.E.D.
diff --git a/tests/GoldFiles/T16.hs.golden b/tests/GoldFiles/T16.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T16.hs.golden
@@ -0,0 +1,62 @@
+
+[SBV] tests/T16.hs:11:1 Proving "f", using Z3.
+** Starting symbolic simulation..
+** Generated symbolic trace:
+SORTS
+  Age
+INPUTS
+  s0 :: Age, aliasing "age"
+CONSTANTS
+  s_2 = False :: Bool
+  s_1 = True :: Bool
+  s2 = 1 :: Int64
+TABLES
+ARRAYS
+UNINTERPRETED CONSTANTS
+  [uninterpreted] ds_d79t :: SInt64
+USER GIVEN CODE SEGMENTS
+AXIOMS
+DEFINE
+  s1 :: SInt64 = [uninterpreted] ds_d79t
+  s3 :: SInt64 = s1 + s2
+  s4 :: SBool = s1 == s3
+CONSTRAINTS
+ASSERTIONS
+OUTPUTS
+  s4
+** Translating to SMT-Lib..
+** Checking Theoremhood..
+** Generated SMTLib program:
+; Automatically generated by SBV. Do not edit.
+(set-option :produce-models true)
+; has user-defined sorts, no logic specified.
+; --- uninterpreted sorts ---
+(declare-sort Age 0)  ; N.B. Uninterpreted: originating from sbvPlugin: <no location info>
+; --- literal constants ---
+(define-fun s_2 () Bool false)
+(define-fun s_1 () Bool true)
+(define-fun s2 () (_ BitVec 64) #x0000000000000001)
+; --- skolem constants ---
+(declare-fun s0 () Age) ; tracks user variable "age"
+; --- constant tables ---
+; --- skolemized tables ---
+; --- arrays ---
+; --- uninterpreted constants ---
+(declare-fun ds_d79t () (_ BitVec 64))
+; --- user given axioms ---
+; --- formula ---
+(assert ; no quantifiers
+   (let ((s1 ds_d79t))
+   (let ((s3 (bvadd s1 s2)))
+   (let ((s4 (= s1 s3)))
+   (not s4)))))
+** Calling: "z3 -nw -in -smt2"
+** Sending the following model extraction commands:
+(get-value (s0))
+** Z3 output:
+sat
+((s0 Age!val!0))
+** Done..
+[Z3] Falsifiable. Counter-example:
+  age = Age!val!0 :: Age
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T17.hs.golden b/tests/GoldFiles/T17.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T17.hs.golden
@@ -0,0 +1,7 @@
+
+[SBV] tests/T17.hs:13:1 Proving "f", using Z3.
+[Z3] Falsifiable. Counter-example:
+  x = 0 :: Int64
+[SBV] Counter-example might be bogus due to uninterpreted constant:
+  [tests/T17.hs:9:1] g :: Int -> Int
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T18.hs.golden b/tests/GoldFiles/T18.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T18.hs.golden
@@ -0,0 +1,63 @@
+
+[SBV] tests/T18.hs:11:1 Proving "f", using Z3.
+** Starting symbolic simulation..
+** Generated symbolic trace:
+SORTS
+  Age
+INPUTS
+  s0 :: Age, aliasing "a"
+  s1 :: Age, aliasing "b"
+CONSTANTS
+  s_2 = False :: Bool
+  s_1 = True :: Bool
+TABLES
+ARRAYS
+UNINTERPRETED CONSTANTS
+  [uninterpreted] |==| :: Age -> Age -> SBool
+USER GIVEN CODE SEGMENTS
+AXIOMS
+DEFINE
+  s2 :: SBool = s0 [uninterpreted] |==| s1
+CONSTRAINTS
+ASSERTIONS
+OUTPUTS
+  s2
+** Translating to SMT-Lib..
+** Checking Theoremhood..
+** Generated SMTLib program:
+; Automatically generated by SBV. Do not edit.
+(set-option :produce-models true)
+; has user-defined sorts, no logic specified.
+; --- uninterpreted sorts ---
+(declare-sort Age 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T18.hs:11:3
+; --- literal constants ---
+(define-fun s_2 () Bool false)
+(define-fun s_1 () Bool true)
+; --- skolem constants ---
+(declare-fun s0 () Age) ; tracks user variable "a"
+(declare-fun s1 () Age) ; tracks user variable "b"
+; --- constant tables ---
+; --- skolemized tables ---
+; --- arrays ---
+; --- uninterpreted constants ---
+(declare-fun |==| (Age Age) Bool)
+; --- user given axioms ---
+; --- formula ---
+(assert ; no quantifiers
+   (let ((s2 (|==| s0 s1)))
+   (not s2)))
+** Calling: "z3 -nw -in -smt2"
+** Sending the following model extraction commands:
+(get-value (s0))
+(get-value (s1))
+** Z3 output:
+sat
+((s0 Age!val!0))
+((s1 Age!val!1))
+** Done..
+[Z3] Falsifiable. Counter-example:
+  a = Age!val!0 :: Age
+  b = Age!val!1 :: Age
+[SBV] Counter-example might be bogus due to uninterpreted constant:
+  [<no location info>] == :: Age -> Age -> Bool
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T19.hs.golden b/tests/GoldFiles/T19.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T19.hs.golden
@@ -0,0 +1,65 @@
+
+[SBV] tests/T19.hs:9:1 Proving "f", using Z3.
+** Starting symbolic simulation..
+** Generated symbolic trace:
+SORTS
+  |[Char]|
+INPUTS
+  s0 :: |[Char]|, aliasing "s"
+CONSTANTS
+  s_2 = False :: Bool
+  s_1 = True :: Bool
+TABLES
+ARRAYS
+UNINTERPRETED CONSTANTS
+  [uninterpreted] reverse :: |[Char]| -> |[Char]|
+  [uninterpreted] |==| :: |[Char]| -> |[Char]| -> SBool
+USER GIVEN CODE SEGMENTS
+AXIOMS
+DEFINE
+  s1 :: |[Char]| = [uninterpreted] reverse s0
+  s2 :: |[Char]| = [uninterpreted] reverse s1
+  s3 :: SBool = s2 [uninterpreted] |==| s0
+CONSTRAINTS
+ASSERTIONS
+OUTPUTS
+  s3
+** Translating to SMT-Lib..
+** Checking Theoremhood..
+** Generated SMTLib program:
+; Automatically generated by SBV. Do not edit.
+(set-option :produce-models true)
+; has user-defined sorts, no logic specified.
+; --- uninterpreted sorts ---
+(declare-sort |[Char]| 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T19.hs:9:3
+; --- literal constants ---
+(define-fun s_2 () Bool false)
+(define-fun s_1 () Bool true)
+; --- skolem constants ---
+(declare-fun s0 () |[Char]|) ; tracks user variable "s"
+; --- constant tables ---
+; --- skolemized tables ---
+; --- arrays ---
+; --- uninterpreted constants ---
+(declare-fun reverse (|[Char]|) |[Char]|)
+(declare-fun |==| (|[Char]| |[Char]|) Bool)
+; --- user given axioms ---
+; --- formula ---
+(assert ; no quantifiers
+   (let ((s1 (reverse s0)))
+   (let ((s2 (reverse s1)))
+   (let ((s3 (|==| s2 s0)))
+   (not s3)))))
+** Calling: "z3 -nw -in -smt2"
+** Sending the following model extraction commands:
+(get-value (s0))
+** Z3 output:
+sat
+((s0 |[Char]!val!0|))
+** Done..
+[Z3] Falsifiable. Counter-example:
+  s = |[Char]!val!0| :: |[Char]|
+[SBV] Counter-example might be bogus due to uninterpreted constants:
+  [<no location info>] ==      :: [Char] -> [Char] -> Bool
+  [<no location info>] reverse :: [Char] -> [Char]
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T20.hs.golden b/tests/GoldFiles/T20.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T20.hs.golden
@@ -0,0 +1,1 @@
+[SBV] tests/T20.hs:10:1 Skipping "f": Don't want to prove this now.
diff --git a/tests/GoldFiles/T21.hs.golden b/tests/GoldFiles/T21.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T21.hs.golden
@@ -0,0 +1,72 @@
+
+[SBV] tests/T21.hs:9:1 Proving "f", using Z3.
+** Starting symbolic simulation..
+** Generated symbolic trace:
+SORTS
+  Char
+  String
+INPUTS
+  s0 :: Char, aliasing "c"
+  s1 :: String, aliasing "s"
+CONSTANTS
+  s_2 = False :: Bool
+  s_1 = True :: Bool
+TABLES
+ARRAYS
+UNINTERPRETED CONSTANTS
+  [uninterpreted] |==_0| :: String -> String -> SBool
+  [uninterpreted] |==| :: Char -> Char -> SBool
+USER GIVEN CODE SEGMENTS
+AXIOMS
+DEFINE
+  s2 :: SBool = s0 [uninterpreted] |==| s0
+  s3 :: SBool = s1 [uninterpreted] |==_0| s1
+  s4 :: SBool = s2 & s3
+CONSTRAINTS
+ASSERTIONS
+OUTPUTS
+  s4
+** Translating to SMT-Lib..
+** Checking Theoremhood..
+** Generated SMTLib program:
+; Automatically generated by SBV. Do not edit.
+(set-option :produce-models true)
+; has user-defined sorts, no logic specified.
+; --- uninterpreted sorts ---
+(declare-sort Char 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T21.hs:9:3
+(declare-sort String 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T21.hs:9:5
+; --- literal constants ---
+(define-fun s_2 () Bool false)
+(define-fun s_1 () Bool true)
+; --- skolem constants ---
+(declare-fun s0 () Char) ; tracks user variable "c"
+(declare-fun s1 () String) ; tracks user variable "s"
+; --- constant tables ---
+; --- skolemized tables ---
+; --- arrays ---
+; --- uninterpreted constants ---
+(declare-fun |==_0| (String String) Bool)
+(declare-fun |==| (Char Char) Bool)
+; --- user given axioms ---
+; --- formula ---
+(assert ; no quantifiers
+   (let ((s2 (|==| s0 s0)))
+   (let ((s3 (|==_0| s1 s1)))
+   (let ((s4 (and s2 s3)))
+   (not s4)))))
+** Calling: "z3 -nw -in -smt2"
+** Sending the following model extraction commands:
+(get-value (s0))
+(get-value (s1))
+** Z3 output:
+sat
+((s0 Char!val!0))
+((s1 String!val!0))
+** Done..
+[Z3] Falsifiable. Counter-example:
+  c =   Char!val!0 :: Char
+  s = String!val!0 :: String
+[SBV] Counter-example might be bogus due to uninterpreted constants:
+  [<no location info>] == :: String -> String -> Bool
+  [<no location info>] == :: Char -> Char -> Bool
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T22.hs.golden b/tests/GoldFiles/T22.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T22.hs.golden
@@ -0,0 +1,65 @@
+
+[SBV] tests/T22.hs:9:1 Proving "f", using Z3.
+** Starting symbolic simulation..
+** Generated symbolic trace:
+SORTS
+  String
+INPUTS
+  s0 :: String, aliasing "s"
+CONSTANTS
+  s_2 = False :: Bool
+  s_1 = True :: Bool
+TABLES
+ARRAYS
+UNINTERPRETED CONSTANTS
+  [uninterpreted] reverse :: String -> String
+  [uninterpreted] |==| :: String -> String -> SBool
+USER GIVEN CODE SEGMENTS
+AXIOMS
+DEFINE
+  s1 :: String = [uninterpreted] reverse s0
+  s2 :: String = [uninterpreted] reverse s1
+  s3 :: SBool = s2 [uninterpreted] |==| s0
+CONSTRAINTS
+ASSERTIONS
+OUTPUTS
+  s3
+** Translating to SMT-Lib..
+** Checking Theoremhood..
+** Generated SMTLib program:
+; Automatically generated by SBV. Do not edit.
+(set-option :produce-models true)
+; has user-defined sorts, no logic specified.
+; --- uninterpreted sorts ---
+(declare-sort String 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T22.hs:9:3
+; --- literal constants ---
+(define-fun s_2 () Bool false)
+(define-fun s_1 () Bool true)
+; --- skolem constants ---
+(declare-fun s0 () String) ; tracks user variable "s"
+; --- constant tables ---
+; --- skolemized tables ---
+; --- arrays ---
+; --- uninterpreted constants ---
+(declare-fun reverse (String) String)
+(declare-fun |==| (String String) Bool)
+; --- user given axioms ---
+; --- formula ---
+(assert ; no quantifiers
+   (let ((s1 (reverse s0)))
+   (let ((s2 (reverse s1)))
+   (let ((s3 (|==| s2 s0)))
+   (not s3)))))
+** Calling: "z3 -nw -in -smt2"
+** Sending the following model extraction commands:
+(get-value (s0))
+** Z3 output:
+sat
+((s0 String!val!0))
+** Done..
+[Z3] Falsifiable. Counter-example:
+  s = String!val!0 :: String
+[SBV] Counter-example might be bogus due to uninterpreted constants:
+  [<no location info>] ==      :: [Char] -> [Char] -> Bool
+  [<no location info>] reverse :: [Char] -> [Char]
+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
diff --git a/tests/GoldFiles/T23.hs.golden b/tests/GoldFiles/T23.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T23.hs.golden
@@ -0,0 +1,3 @@
+
+[SBV] tests/T23.hs:9:1 Proving "f", using Z3.
+[Z3] Q.E.D.
diff --git a/tests/GoldFiles/T24.hs.golden b/tests/GoldFiles/T24.hs.golden
new file mode 100644
--- /dev/null
+++ b/tests/GoldFiles/T24.hs.golden
@@ -0,0 +1,3 @@
+
+[SBV] tests/T24.hs:10:1 Proving "f", using Z3.
+[Z3] Q.E.D.
diff --git a/tests/Run.hs b/tests/Run.hs
new file mode 100644
--- /dev/null
+++ b/tests/Run.hs
@@ -0,0 +1,41 @@
+module Main(main) where
+
+import Control.Monad (void)
+
+import Data.Char (isDigit)
+
+import Test.Tasty
+import Test.Tasty.Golden
+
+import System.Directory
+import System.FilePath
+import System.Process
+
+main :: IO ()
+main = do tests <- findTests
+          defaultMain (testGroup "Tests" [unitTests tests])
+  where unitTests = testGroup "Unit tests" . map (runTest . takeBaseName)
+
+findTests :: IO [FilePath]
+findTests = do allEntries <- getDirectoryContents "tests"
+               let testFile f = let b = takeBaseName f
+                                    e = takeExtension f
+                                in e == ".hs" && case b of
+                                                  'T':xs -> all isDigit xs
+                                                  _      -> False
+               return $ filter testFile allEntries
+
+runTest :: String -> TestTree
+runTest f = goldenVsFile f gld out act
+  where (inp, hi, o, gld, out) = fileNames f
+        act = do void $ system $ unwords ["ghc", "-c", inp, ">", out, "2>&1"]
+                 void $ system $ unwords ["/bin/rm", "-f", hi, o]
+
+fileNames :: FilePath -> (FilePath, FilePath, FilePath, FilePath, FilePath)
+fileNames fp = (inp, hi, o, gld, out)
+  where f   = takeBaseName fp
+        inp = "tests" </> f <.> "hs"
+        hi  = "tests" </> f <.> "hi"
+        o   = "tests" </> f <.> "o"
+        gld = "tests/GoldFiles" </> f <.> "hs.golden"
+        out = "tests/GoldFiles" </> f <.> "hs.current"