diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,7 +1,12 @@
 * Hackage: <http://hackage.haskell.org/package/sbvPlugin>
 * GitHub:  <http://github.com/LeventErkok/sbvPlugin>
 
-* Latest Hackage released version: 0.8, 2017-01-12
+* Latest Hackage released version: 0.9, 2017-07-19
+
+### Version 0.9, 2017-07-19
+
+  * Sync-up with recent modifications to SBV. No user visible changes.
+  * Bump up sbv dependence to >= 7.0
 
 ### Version 0.8, 2017-01-12
 
diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs
--- a/Data/SBV/Plugin/Analyze.hs
+++ b/Data/SBV/Plugin/Analyze.hs
@@ -88,7 +88,7 @@
             topLoc = varSpan topBind
             loc = "[SBV] " ++ showSpan (flags cfgEnv) topLoc
             slvrTag = ", using " ++ tag ++ "."
-              where tag = case solverConfigs of
+              where tag = case map (S.name . S.solver) solverConfigs of
                             []     -> "no solvers"  -- can't really happen
                             [x]    -> show x
                             [x, y] -> show x ++ " and " ++ show y
@@ -99,13 +99,13 @@
                         finalUninterps <- readIORef (rUninterpreted cfgEnv)
                         return (finalResult, finalUninterps)
         case finalResult of
-          Right (solver, sres@(S.ThmResult smtRes)) -> do
+          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
+                                S.SatExtField{}   -> False   -- conservative
                 putStr $ "[" ++ show solver ++ "] "
                 print sres
 
@@ -450,7 +450,7 @@
                    Nothing -> "Kind: " ++ sh k
                    Just t  -> "Type: " ++ sh t
 
-       sym (KBase k) nm  = do v <- lift $ S.svMkSymVar Nothing k nm
+       sym (KBase k) nm  = do v <- lift $ ask >>= liftIO . S.svMkSymVar Nothing k nm
                               return (Base v)
 
        sym (KTup ks) nm = do let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. length ks]
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,9 +1,7 @@
 ## SBVPlugin: SBV Plugin for GHC
 
-[![Hackage version](http://budueba.com/hackage/sbvPlugin)]
-		   (http://hackage.haskell.org/package/sbvPlugin)
-[![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)]
-                (http://travis-ci.org/LeventErkok/sbvPlugin)
+[![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
 
@@ -54,9 +52,9 @@
 test x y = x == y -- clearly not True!
 ```
 
-The above, for instance, tells the plugin to ignore failed commands (`IgnoreFailure`). This would be useful when you
-have a failing theorem that you are still working on, to make sure GHC continues compilation instead of stopping at
-that point.
+The above, for instance, tells the plugin to ignore failed proofs (`IgnoreFailure`). This is useful when you
+have a failing theorem that you are still working on, to make sure GHC continues compilation instead of stopping
+compilation and erroring out at that point.
 
 ### Available options
 
diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal
--- a/sbvPlugin.cabal
+++ b/sbvPlugin.cabal
@@ -1,5 +1,5 @@
 Name              : sbvPlugin
-Version           : 0.8
+Version           : 0.9
 Category          : Formal methods, Theorem provers, Math, SMT, Symbolic Computation
 Synopsis          : Formally prove properties of Haskell programs using SBV/SMT
 Description       : GHC plugin for proving properties over Haskell functions using SMT solvers, based
@@ -30,7 +30,7 @@
                   , Data.SBV.Plugin.Examples.MergeSort
                   , Data.SBV.Plugin.Examples.MicroController
                   , Data.SBV.Plugin.Examples.BitTricks
-  build-depends   : base >= 4.9 && < 5, ghc, ghc-prim, containers, sbv >= 5.14, mtl, template-haskell
+  build-depends   : base >= 4.9 && < 5, ghc, ghc-prim, containers, sbv >= 7.0, mtl, template-haskell
   Other-modules   : Data.SBV.Plugin.Analyze
                   , Data.SBV.Plugin.Common
                   , Data.SBV.Plugin.Env