diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs
index 4a4fd8e9c..3b9ef5a99 100644
--- a/Data/SBV/Control/Utils.hs
+++ b/Data/SBV/Control/Utils.hs
@@ -38,7 +38,6 @@ module Data.SBV.Control.Utils (
      , timeout, queryDebug, retrieveResponse, recoverKindedValue, runProofOn, executeQuery
      ) where
 
-import Control.Exception (finally)
 import Data.List  (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort, isPrefixOf, isSuffixOf)
 
 import Data.Char      (isPunctuation, isSpace, isDigit)
@@ -1899,12 +1898,7 @@ executeQuery queryContext (QueryT userQuery) = do
 
                   liftIO $ writeIORef (runMode st) $ SMTMode qc IRun isSAT cfg
 
-                  lift $ join $ liftIO $
-                    finally (extractIO $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT userQuery) $ do
-                      qs <- readIORef $ rQueryState st
-                      case qs of
-                        Nothing                         -> return ()
-                        Just QueryState{queryTerminate} -> queryTerminate
+                  lift $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT userQuery
 
         -- Already in a query, in theory we can just continue, but that causes use-case issues
         -- so we reject it. TODO: Review if we should actually support this. The issue arises with
diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs
index 5d430b745..e40e077b4 100644
--- a/Data/SBV/Core/Symbolic.hs
+++ b/Data/SBV/Core/Symbolic.hs
@@ -1967,6 +1967,13 @@ runSymbolicInState st (SymbolicT c) = do
                  = contextMismatchError (sbvContext st) ctx Nothing Nothing
 
    mapM_ check $ nub $ G.universeBi res
+
+   -- Clean-up after ourselves
+   qs <- liftIO $ readIORef $ rQueryState st
+   case qs of
+     Nothing                         -> return ()
+     Just QueryState{queryTerminate} -> liftIO queryTerminate
+
    return (r, res)
 
 -- | Grab the program from a running symbolic simulation state.