Merge pull request #116 from GaloisInc/dgb_1618937981-0

Refactor SMTLib2 response parsing and handling
2024-11-29 05:45:01 +03:00 · 2021-04-28 08:29:08 -07:00 · 2021-04-28 08:29:08 -07:00 · eb057c82d1
commit eb057c82d1
parent 2b4273c818 74ee60155b
53 changed files with 2344 additions and 406 deletions
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@ -45,11 +45,6 @@ jobs:
      - name: Cabal update
        shell: bash
        run: nix-shell -p cabal-install --run 'cabal update'
-      - name: Cabal check
-        shell: bash
-        run: |
-          cd what4
-          nix-shell -p cabal-install --run 'cabal check'
      - name: Setup Environment Vars
        run: |
          GHC=haskell.compiler.ghc$(echo ${{ matrix.ghc }} | sed -e s,\\.,,g)
@ -90,7 +85,7 @@ jobs:
        # LD_LIBRARY_PATH manipulation may be removed for all steps.
        run: |
          cd what4
-          $NS 'LD_LIBRARY_PATH="$ZLIB_LOC:$LD_LIBRARY_PATH" cabal configure -fSTPTestDisable -fdRealTestDisable -fsolverTests --extra-lib-dirs="$ZLIB_LOC"'
+          $NS 'LD_LIBRARY_PATH="$ZLIB_LOC:$LD_LIBRARY_PATH" cabal configure --enable-tests -fSTPTestDisable -fdRealTestDisable -fsolverTests --extra-lib-dirs="$ZLIB_LOC"'
      - name: Build
        shell: bash
        run: |
--- a/what4/src/What4/Config.hs
+++ b/what4/src/What4/Config.hs
@ -87,6 +87,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 module What4.Config
  ( -- * Names of properties
@ -100,6 +101,9 @@ module What4.Config
    -- * Option settings
  , OptionSetting(..)
  , Opt(..)
+  , setUnicodeOpt
+  , setIntegerOpt
+  , setBoolOpt

    -- * Defining option styles
  , OptionStyle(..)
@ -112,6 +116,9 @@ module What4.Config
  , optWarn
  , optErr
  , checkOptSetResult
+  , OptSetFailure(..)
+  , OptGetFailure(..)
+  , OptCreateFailure(..)

    -- ** Option style templates
  , Bound(..)
@ -136,6 +143,8 @@ module What4.Config
  , optV
  , optU
  , optUV
+  , copyOpt
+  , deprecatedOpt

    -- * Building and manipulating configurations
  , Config
@ -157,29 +166,26 @@ module What4.Config
  , verbosityLogger
  ) where

-#if !MIN_VERSION_base(4,13,0)
-import Control.Monad.Fail( MonadFail )
-#endif
-
-import           Control.Applicative (Const(..))
+import           Control.Applicative ( Const(..), (<|>) )
 import           Control.Concurrent.MVar
-import           Control.Exception
 import           Control.Lens ((&))
-import           Control.Monad.Identity
+import qualified Control.Lens.Combinators as LC
+import           Control.Monad.Catch
 import           Control.Monad.IO.Class
+import           Control.Monad.Identity
 import           Control.Monad.Writer.Strict hiding ((<>))
-import           Data.Kind
-import           Data.Maybe
-import           Data.Typeable
 import           Data.Foldable (toList)
+import           Data.Kind
 import           Data.List.NonEmpty (NonEmpty(..))
+import           Data.Map (Map)
+import qualified Data.Map.Strict as Map
+import           Data.Maybe
+import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
 import           Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import           Data.Set (Set)
 import qualified Data.Set as Set
-import           Data.Map (Map)
-import qualified Data.Map.Strict as Map
 import           Data.Text (Text)
 import qualified Data.Text as Text
 import           Data.Void
@ -305,6 +311,12 @@ data OptionSetting (tp :: BaseType) =
  }


+instance Show (OptionSetting tp) where
+  show = (<> " option setting") .
+         LC.cons '\'' . flip LC.snoc '\'' .
+         show . optionSettingName
+instance ShowF OptionSetting
+
 -- | An option defines some metadata about how a configuration option behaves.
 --   It contains a base type representation, which defines the runtime type
 --   that is expected for setting and querying this option at runtime.
@ -427,7 +439,7 @@ realWithRangeOptSty lo hi = realOptSty & set_opt_onset vf
        vf _ (ConcreteReal x)
          | checkBound lo hi x = return optOK
          | otherwise          = return $ optErr $
-                                 prettyRational x <+> "out of range, expected real value in "
+                                 prettyRational x <+> "out of range, expected real value in"
                                                  <+> docInterval lo hi

 -- | Option style for real-valued options with a lower bound
@ -447,7 +459,7 @@ integerWithRangeOptSty lo hi = integerOptSty & set_opt_onset vf
        vf _ (ConcreteInteger x)
          | checkBound lo hi x = return optOK
          | otherwise          = return $ optErr $
-                                 pretty x <+> "out of range, expected integer value in "
+                                 pretty x <+> "out of range, expected integer value in"
                                          <+> docInterval lo hi

 -- | Option style for integer-valued options with a lower bound
@ -469,9 +481,9 @@ enumOptSty elts = stringOptSty & set_opt_onset vf
        vf _ (ConcreteString (UnicodeLiteral x))
         | x `Set.member` elts = return optOK
         | otherwise = return $ optErr $
-                            "invalid setting" <+> dquotes (pretty x) <+>
-                            ", expected one of:" <+>
-                            align (sep (map pretty $ Set.toList elts))
+                            "invalid setting" <+> dquotes (pretty x) <>
+                            ", expected one of these enums:" <+>
+                            align (sep (punctuate comma (map pretty $ Set.toList elts)))

 -- | A configuration syle for options that must be one of a fixed set of text values.
 --   Associated with each string is a validation/callback action that will be run
@ -488,12 +500,73 @@ listOptSty values =  stringOptSty & set_opt_onset vf
        vf _ (ConcreteString (UnicodeLiteral x)) =
         fromMaybe
          (return $ optErr $
-            "invalid setting" <+> dquotes (pretty x) <+>
-            ", expected one of:" <+>
+            "invalid setting" <+> dquotes (pretty x) <>
+            ", expected one from this list:" <+>
            align (sep (map (pretty . fst) $ Map.toList values)))
          (Map.lookup x values)


+-- | Used as a wrapper for an option that has been deprecated. If the
+-- option is actually set (as opposed to just using the default value)
+-- then this will emit an OptionSetResult warning that time, optionally
+-- mentioning the replacement option (if specified).
+--
+-- There are three cases of deprecation:
+-- 1. Removing an option that no longer applies
+-- 2. Changing the name or heirarchical position of an option.
+-- 3. #2 and also changing the type.
+-- 4. Replacing an option by multiple new options (e.g. split url option
+--    into hostname and port options)
+--
+-- In the case of #1, the option will presumably be ignored by the
+-- code and the warnings are provided to allow the user to clean the
+-- option from their configurations.
+--
+-- In the case of #2, the old option and the new option will share the
+-- same value storage: changes to one can be seen via the other and
+-- vice versa.  The code can be switched over to reference the new
+-- option entirely, and user configurations setting the old option
+-- will still work until they have been updated and the definition of
+-- the old option is removed entirely.
+--
+--   NOTE: in order to support #2, the newer option should be declared
+--   (via 'insertOption') *before* the option it deprecates.
+--
+-- In the case of #3, it is not possible to share storage space, so
+-- during the deprecation period, the code using the option config
+-- value must check both locations and decide which value to utilize.
+--
+-- Case #4 is an enhanced form of #3 and #2, and is generally treated
+-- as #3, but adds the consideration that deprecation warnings will
+-- need to advise about multiple new options.  The inverse of #4
+-- (multiple options being combined to a single newer option) is just
+-- treated as separate deprecations.
+--
+--   NOTE: in order to support #4, the newer options should all be
+--   declared (via 'insertOption') *before* the options they deprecate.
+--
+-- Nested deprecations are valid, and replacement warnings are
+-- automatically transitive to the newest options.
+--
+-- Any user-supplied value for the old option will result in warnings
+-- emitted to the OptionSetResult for all four cases.  Code should
+-- ensure that these warnings are appropriately communicated to the
+-- user to allow configuration updates to occur.
+--
+-- Note that for #1 and #2, the overhead burden of continuing to
+-- define the deprecated option is very small, so actual removal of
+-- the older config can be delayed indefinitely.
+
+deprecatedOpt :: [ConfigDesc] -> ConfigDesc -> ConfigDesc
+deprecatedOpt newerOpt (ConfigDesc o sty desc oldRepl) =
+  let -- note: description and setter not modified here in case this
+      -- is called again to declare additional replacements (viz. case
+      -- #2 above).  These will be modified in the 'insertOption' function.
+      newRepl :: Maybe [ConfigDesc]
+      newRepl = (newerOpt <>) <$> (oldRepl <|> Just [])
+  in ConfigDesc o sty desc newRepl
+
+
 -- | A configuration style for options that are expected to be paths to an executable
 --   image.  Configuration options with this style generate a warning message if set to a
 --   value that cannot be resolved to an absolute path to an executable file in the
@ -517,7 +590,14 @@ executablePathOptSty = stringOptSty & set_opt_onset vf
 --   an @OptionStyle@ describing the sort of option it is, and an optional
 --   help message describing the semantics of this option.
 data ConfigDesc where
-  ConfigDesc :: ConfigOption tp -> OptionStyle tp -> Maybe (Doc Void) -> ConfigDesc
+  ConfigDesc :: ConfigOption tp  -- describes option name and type
+             -> OptionStyle tp   -- option validators, help info, type and default
+             -> Maybe (Doc Void) -- help text
+             -> Maybe [ConfigDesc] -- Deprecation and newer replacements
+             -> ConfigDesc
+
+instance Show ConfigDesc where
+  show (ConfigDesc o _ _ _) = show o

 -- | The most general method for constructing a normal `ConfigDesc`.
 mkOpt :: ConfigOption tp     -- ^ Fixes the name and the type of this option
@ -525,7 +605,7 @@ mkOpt :: ConfigOption tp     -- ^ Fixes the name and the type of this option
      -> Maybe (Doc Void)    -- ^ Help text
      -> Maybe (ConcreteVal tp) -- ^ A default value for this option
      -> ConfigDesc
-mkOpt o sty h def = ConfigDesc o sty{ opt_default_value = def } h
+mkOpt o sty h def = ConfigDesc o sty{ opt_default_value = def } h Nothing

 -- | Construct an option using a default style with a given initial value
 opt :: Pretty help
@ -582,13 +662,28 @@ optUV o vf h = mkOpt o (defaultOpt (configOptionType o)
                       Nothing -> return optOK
                       Just z  -> return $ optErr $ pretty z

+-- | The copyOpt creates a duplicate ConfigDesc under a different
+-- name.  This is typically used to taking a common operation and
+-- modify the prefix to apply it to a more specialized role
+-- (e.g. solver.strict_parsing --> solver.z3.strict_parsing).  The
+-- style and help text of the input ConfigDesc are preserved, but any
+-- deprecation is discarded.
+copyOpt :: (Text -> Text) -> ConfigDesc -> ConfigDesc
+copyOpt modName (ConfigDesc o@(ConfigOption ty _) sty h _) =
+  let newName = case splitPath (modName (configOptionText o)) of
+        Just ps -> ps
+        Nothing -> error "new config option must not be empty"
+  in ConfigDesc (ConfigOption ty newName) sty h Nothing
+
+
+
 ------------------------------------------------------------------------
 -- ConfigState

 data ConfigLeaf where
  ConfigLeaf ::
    !(OptionStyle tp)              {- Style for this option -} ->
-    MVar (Maybe (ConcreteVal tp)) {- State of the option -} ->
+    MVar (Maybe (ConcreteVal tp))  {- State of the option -} ->
    Maybe (Doc Void)               {- Help text for the option -} ->
    ConfigLeaf

@ -619,7 +714,8 @@ adjustConfigTrie     [] f (Just (ConfigTrie x m)) = g <$> f x
 adjustConfigMap :: Functor t => Text -> [Text] -> (Maybe ConfigLeaf -> t (Maybe ConfigLeaf)) -> ConfigMap -> t ConfigMap
 adjustConfigMap a as f = Map.alterF (adjustConfigTrie as f) a

-- | Traverse an entire @ConfigMap@.  The first argument is
+-- | Traverse an entire @ConfigMap@.  The first argument is the
+-- reversed heirarchical location of the starting map entry location.
 traverseConfigMap ::
  Applicative t =>
  [Text] {- ^ A REVERSED LIST of the name segments that represent the context from the root to the current @ConfigMap@. -} ->
@ -650,19 +746,145 @@ traverseSubtree ps0 f = go ps0 []
  where
  go     [] revPath = traverseConfigMap revPath f
  go (p:ps) revPath = Map.alterF (traverse g) p
-     where g (ConfigTrie x m) = ConfigTrie x <$> go ps (p:revPath) m
+     where g (ConfigTrie x m) = ConfigTrie <$> here x <*> go ps (p:revPath) m
+           here = traverse (f (reverse (p:revPath)))


-- | Add an option to the given @ConfigMap@.
-insertOption :: (MonadIO m, MonadFail m) => ConfigDesc -> ConfigMap -> m ConfigMap
-insertOption (ConfigDesc (ConfigOption _tp (p:|ps)) sty h) m = adjustConfigMap p ps f m
+-- | Add an option to the given @ConfigMap@ or throws an
+-- 'OptCreateFailure' exception on error.
+--
+-- Inserting an option multiple times is idempotent under equivalency
+-- modulo the opt_onset in the option's style, otherwise it is an
+-- error.
+insertOption :: (MonadIO m, MonadThrow m)
+             => ConfigMap -> ConfigDesc -> m ConfigMap
+insertOption m d@(ConfigDesc o@(ConfigOption _tp (p:|ps)) sty h newRepls) =
+  adjustConfigMap p ps f m
  where
-  f Nothing  =
-       do ref <- liftIO (newMVar (opt_default_value sty))
-          return (Just (ConfigLeaf sty ref h))
-  f (Just _) = fail ("Option " ++ showPath ++ " already exists")
+  f Nothing =
+    let addOnSetWarning warning oldSty =
+          let newSty = set_opt_onset depF oldSty
+              oldVF = opt_onset oldSty
+              depF oldV newV =
+                do v <- oldVF oldV newV
+                   return (v <> optWarn warning)
+          in newSty
+        deprHelp depMsg ontoHelp =
+          let hMod oldHelp = vsep [ oldHelp, "*** DEPRECATED! ***", depMsg ]
+          in hMod <$> ontoHelp
+        newRefs tySep = hsep . punctuate comma .
+                        map (\(n, ConfigLeaf s _ _) -> optRef tySep n s)
+        optRef tySep nm s = hcat [ pretty (show nm), tySep
+                                 , pretty (show (opt_type s))
+                                 ]
+    in case newRepls of
+         -- not deprecated
+         Nothing ->
+           do ref <- liftIO (newMVar (opt_default_value sty))
+              return (Just (ConfigLeaf sty ref h))

-  showPath = Text.unpack (Text.intercalate "." (p:ps))
+         -- deprecation case #1 (removal)
+         Just [] ->
+           do ref <- liftIO (newMVar (opt_default_value sty))
+              let sty' = addOnSetWarning
+                         ("DEPRECATED CONFIG OPTION WILL BE IGNORED: " <>
+                           pretty (show o) <>
+                           " (no longer valid)")
+                         sty
+                  hmsg = "Option '" <> pretty (show o) <> "' is no longer valid."
+              return (Just (ConfigLeaf sty' ref (deprHelp hmsg h)))
+
+         Just n -> do
+           let newer =
+                 let returnFnd fnd loc lf =
+                       if name loc == fnd
+                       then Const [Just (fnd, lf)]
+                       else Const [Nothing]
+                     name parts = Text.intercalate "." parts
+                     lookupNewer (ConfigDesc (ConfigOption _ (t:|ts)) _sty _h new2) =
+                       case new2 of
+                         Nothing -> getConst $ traverseConfigMap [] (returnFnd (name (t:ts))) m
+                         Just n2 -> concat (lookupNewer <$> n2)
+                 in lookupNewer <$> n
+               chkMissing opts =
+                 if not (null opts) && null (catMaybes opts)
+                 then throwM $ OptCreateFailure d $
+                      "replacement options must be inserted into" <>
+                      " Config before this deprecated option"
+                 else return opts
+           newOpts <- catMaybes . concat <$> mapM chkMissing newer
+
+           case newOpts of
+
+             -- deprecation case #1 (removal)
+             [] ->
+               do ref <- liftIO (newMVar (opt_default_value sty))
+                  let sty' = addOnSetWarning
+                             ("DEPRECATED CONFIG OPTION WILL BE IGNORED: " <>
+                              pretty (show o) <>
+                              " (no longer valid)")
+                             sty
+                      hmsg = "Option '" <> pretty (show o) <> "' is no longer valid."
+                  return (Just (ConfigLeaf sty' ref (deprHelp hmsg h)))
+
+             -- deprecation case #2 (renamed)
+             ((nm, ConfigLeaf sty' v _):[])
+               | Just Refl <- testEquality (opt_type sty) (opt_type sty') ->
+                 do let updSty = addOnSetWarning
+                                 ("DEPRECATED CONFIG OPTION USED: " <>
+                                  pretty (show o) <>
+                                  " (renamed to: " <> pretty nm <> ")")
+                        hmsg = "Suggest replacing '" <> pretty (show o) <>
+                               "' with '" <> pretty nm <> "'."
+                    return (Just (ConfigLeaf (updSty sty) v (deprHelp hmsg h)))
+
+             -- deprecation case #3 (renamed and re-typed)
+             (new1:[]) ->
+               do ref <- liftIO (newMVar (opt_default_value sty))
+                  let updSty = addOnSetWarning
+                               ("DEPRECATED CONFIG OPTION USED: " <>
+                                optRef "::" o sty <>
+                                " (changed to: " <>
+                                newRefs "::" [new1] <>
+                                "); this value may be ignored")
+                      hmsg = "Suggest converting '" <>
+                             optRef " of type " o sty <>
+                             " to " <>
+                             newRefs " of type " [new1]
+                  return (Just (ConfigLeaf (updSty sty) ref (deprHelp hmsg h)))
+
+             -- deprecation case #4 (split to multiple options)
+             newMulti ->
+               do ref <- liftIO (newMVar (opt_default_value sty))
+                  let updSty = addOnSetWarning
+                               ("DEPRECATED CONFIG OPTION USED: " <>
+                                optRef "::" o sty <>
+                                " (replaced by: " <>
+                                newRefs "::" newMulti <>
+                                "); this value may be ignored")
+                      hmsg = "Suggest converting " <>
+                             optRef " of type " o sty <>
+                             " to: " <> (newRefs " of type " newMulti)
+                  return (Just (ConfigLeaf (updSty sty) ref (deprHelp hmsg h)))
+
+  f (Just existing@(ConfigLeaf sty' _ h')) =
+    case testEquality (opt_type sty) (opt_type sty') of
+      Just Refl ->
+        if and [ show (opt_help sty) == show (opt_help sty')
+               , opt_default_value sty == opt_default_value sty'
+               -- Note opt_onset in sty is ignored/dropped
+               , show h == show h'
+               ]
+        then return $ Just existing
+        else throwM $ OptCreateFailure d "already exists"
+      Nothing -> throwM $ OptCreateFailure d
+                 (pretty $ "already exists with type " <> show (opt_type sty'))
+
+data OptCreateFailure = OptCreateFailure ConfigDesc (Doc Void)
+instance Exception OptCreateFailure
+instance Show OptCreateFailure where
+  show (OptCreateFailure cfgdesc msg) =
+    "Failed to create option " <> show cfgdesc <> ": " <> show msg


 ------------------------------------------------------------------------
@ -682,13 +904,14 @@ initialConfig initVerbosity ts = do
   extendConfig (builtInOpts initVerbosity ++ ts) cfg
   return cfg

-- | Extend an existing configuration with new options.  An error will be
--   raised if any of the given options clash with options that already exists.
+-- | Extend an existing configuration with new options.  An
+--   'OptCreateFailure' exception will be raised if any of the given
+--   options clash with options that already exists.
 extendConfig :: [ConfigDesc]
             -> Config
             -> IO ()
 extendConfig ts (Config cfg) =
-  modifyMVar_ cfg (\m -> foldM (flip insertOption) m ts)
+  modifyMVar_ cfg (\m -> foldM insertOption m ts)

 -- | Verbosity of the simulator.  This option controls how much
 --   informational and debugging output is generated.
@ -726,24 +949,44 @@ class Opt (tp :: BaseType) (a :: Type) | tp -> a where
  trySetOpt :: OptionSetting tp -> a -> IO OptionSetResult

  -- | Set the value of an option.  Return any generated warnings.
-  --   Throw an exception if a validation error occurs.
+  --   Throws an OptSetFailure exception if a validation error occurs.
  setOpt :: OptionSetting tp -> a -> IO [Doc Void]
-  setOpt x v = trySetOpt x v >>= checkOptSetResult
+  setOpt x v = trySetOpt x v >>= checkOptSetResult x

  -- | Get the current value of an option.  Throw an exception
  --   if the option is not currently set.
  getOpt :: OptionSetting tp -> IO a
-  getOpt x = maybe (fail msg) return =<< getMaybeOpt x
-    where msg = "Option is not set: " ++ show (optionSettingName x)
+  getOpt x = maybe (throwM $ OptGetFailure (OSet $ Some x) "not set") return
+             =<< getMaybeOpt x

 -- | Throw an exception if the given @OptionSetResult@ indidcates
 --   an error.  Otherwise, return any generated warnings.
-checkOptSetResult :: OptionSetResult -> IO [Doc Void]
-checkOptSetResult res =
+checkOptSetResult :: OptionSetting tp -> OptionSetResult -> IO [Doc Void]
+checkOptSetResult optset res =
  case optionSetError res of
-    Just msg -> fail (show msg)
+    Just msg -> throwM $ OptSetFailure (Some optset) msg
    Nothing -> return (toList (optionSetWarnings res))

+data OptSetFailure = OptSetFailure (Some OptionSetting) (Doc Void)
+instance Exception OptSetFailure
+instance Show OptSetFailure where
+  show (OptSetFailure optset msg) =
+    "Failed to set " <> show optset <> ": " <> show msg
+
+data OptRef = OName Text | OSet (Some OptionSetting) | OCfg (Some ConfigOption)
+instance Show OptRef where
+  show = \case
+    OName t -> show t
+    OSet (Some s) -> show s
+    OCfg (Some c) -> show c
+
+data OptGetFailure = OptGetFailure OptRef (Doc Void)
+instance Exception OptGetFailure
+instance Show OptGetFailure where
+  show (OptGetFailure optref msg) =
+    "Failed to get " <> (show optref) <> ": " <> show msg
+
+
 instance Opt (BaseStringType Unicode) Text where
  getMaybeOpt x = fmap (fromUnicodeLit . fromConcreteString) <$> getOption x
  trySetOpt x v = setOption x (ConcreteString (UnicodeLiteral v))
@ -756,6 +999,47 @@ instance Opt BaseBoolType Bool where
  getMaybeOpt x = fmap fromConcreteBool <$> getOption x
  trySetOpt x v = setOption x (ConcreteBool v)

+instance Opt BaseRealType Rational where
+  getMaybeOpt x = fmap fromConcreteReal <$> getOption x
+  trySetOpt x v = setOption x (ConcreteReal v)
+
+-- | Given a unicode text value, set the named option to that value or
+-- generate an OptSetFailure exception if the option is not a unicode
+-- text valued option.
+setUnicodeOpt :: Some OptionSetting -> Text -> IO [Doc Void]
+setUnicodeOpt (Some optset) val =
+  let tyOpt = configOptionType (optionSettingName optset)
+  in case testEquality tyOpt (BaseStringRepr UnicodeRepr) of
+       Just Refl -> setOpt optset val
+       Nothing ->
+         checkOptSetResult optset $ optErr $
+         "option type is a" <+> pretty tyOpt <+> "but given a text string"
+
+-- | Given an integer value, set the named option to that value or
+-- generate an OptSetFailure exception if the option is not an integer
+-- valued option.
+setIntegerOpt :: Some OptionSetting -> Integer -> IO [Doc Void]
+setIntegerOpt (Some optset) val =
+  let tyOpt = configOptionType (optionSettingName optset)
+  in case testEquality tyOpt BaseIntegerRepr of
+       Just Refl -> setOpt optset val
+       Nothing ->
+         checkOptSetResult optset $ optErr $
+         "option type is a" <+> pretty tyOpt <+> "but given an integer"
+
+-- | Given a boolean value, set the named option to that value or
+-- generate an OptSetFailure exception if the option is not a boolean
+-- valued option.
+setBoolOpt :: Some OptionSetting -> Bool -> IO [Doc Void]
+setBoolOpt (Some optset) val =
+  let tyOpt = configOptionType (optionSettingName optset)
+  in case testEquality tyOpt BaseBoolRepr of
+       Just Refl -> setOpt optset val
+       Nothing ->
+         checkOptSetResult optset $ optErr $
+         "option type is a" <+> pretty tyOpt <+> "but given a boolean"
+
+
 -- | Given a @ConfigOption@ name, produce an @OptionSetting@
 --   object for accessing and setting the value of that option.
 --
@ -768,7 +1052,7 @@ getOptionSetting ::
 getOptionSetting o@(ConfigOption tp (p:|ps)) (Config cfg) =
   readMVar cfg >>= getConst . adjustConfigMap p ps f
 where
-  f Nothing  = Const (fail $ "Option not found: " ++ show o)
+  f Nothing  = Const (throwM $ OptGetFailure (OCfg $ Some o) "not found")
  f (Just x) = Const (leafToSetting x)

  leafToSetting (ConfigLeaf sty ref _h)
@ -781,8 +1065,11 @@ getOptionSetting o@(ConfigOption tp (p:|ps)) (Config cfg) =
             let new = if (isJust (optionSetError res)) then old else (Just v)
             new `seq` return (new, res)
      }
-    | otherwise = fail ("Type mismatch retrieving option " ++ show o ++
-                         "\nExpected: " ++ show tp ++ " but found " ++ show (opt_type sty))
+    | otherwise = throwM $ OptGetFailure (OCfg $ Some o)
+                  (pretty $ "Type mismatch: " <>
+                    "expected '" <> show tp <>
+                    "' but found '" <> show (opt_type sty) <> "'"
+                  )

 -- | Given a text name, produce an @OptionSetting@
 --   object for accessing and setting the value of that option.
@ -794,10 +1081,12 @@ getOptionSettingFromText ::
  IO (Some OptionSetting)
 getOptionSettingFromText nm (Config cfg) =
   case splitPath nm of
-     Nothing -> fail "Illegal empty name for option"
+     Nothing -> throwM $ OptGetFailure (OName "") "Illegal empty name for option"
     Just (p:|ps) -> readMVar cfg >>= (getConst . adjustConfigMap p ps (f (p:|ps)))
  where
-  f (p:|ps) Nothing  = Const (fail $ "Option not found: " ++ (Text.unpack (Text.intercalate "." (p:ps))))
+  f (p:|ps) Nothing  = Const (throwM $ OptGetFailure
+                              (OName (Text.intercalate "." (p:ps)))
+                              "not found")
  f path (Just x) = Const (leafToSetting path x)

  leafToSetting path (ConfigLeaf sty ref _h) = return $
@ -815,6 +1104,12 @@ getOptionSettingFromText nm (Config cfg) =
 data ConfigValue where
  ConfigValue :: ConfigOption tp -> ConcreteVal tp -> ConfigValue

+instance Pretty ConfigValue where
+  pretty (ConfigValue option val) =
+    ppSetting (configOptionNameParts option) (Just val)
+    <+> "::" <+> pretty (configOptionType option)
+
+
 -- | Given the name of a subtree, return all
 --   the currently-set configurtion values in that subtree.
 --
@ -825,9 +1120,10 @@ getConfigValues ::
  IO [ConfigValue]
 getConfigValues prefix (Config cfg) =
  do m <- readMVar cfg
-     let ps = Text.splitOn "." prefix
+     let ps = dropWhile Text.null $ Text.splitOn "." prefix
         f :: [Text] -> ConfigLeaf -> WriterT (Seq ConfigValue) IO ConfigLeaf
-         f [] _ = fail $ "getConfigValues: illegal empty option name"
+         f [] _ = throwM $ OptGetFailure (OName prefix)
+                  "illegal empty option prefix name"
         f (p:path) l@(ConfigLeaf sty ref _h) =
            do liftIO (readMVar ref) >>= \case
                 Just x  -> tell (Seq.singleton (ConfigValue (ConfigOption (opt_type sty) (p:|path)) x))
@ -845,7 +1141,7 @@ ppOption :: [Text] -> OptionStyle tp -> Maybe (ConcreteVal tp) -> Maybe (Doc Voi
 ppOption nm sty x help =
  vcat
  [ group $ fillCat [ppSetting nm x, indent 2 (opt_help sty)]
-  , maybe mempty (indent 2) help
+  , maybe mempty (indent 4) help
  ]

 ppConfigLeaf :: [Text] -> ConfigLeaf -> IO (Doc Void)
@ -854,7 +1150,7 @@ ppConfigLeaf nm (ConfigLeaf sty ref help) =
     return $ ppOption nm sty x help

 -- | Given the name of a subtree, compute help text for
--   all the options avaliable in that subtree.
+--   all the options available in that subtree.
 --
 --   If the subtree name is empty, the entire tree will be traversed.
 configHelp ::
@ -863,7 +1159,7 @@ configHelp ::
  IO [Doc Void]
 configHelp prefix (Config cfg) =
  do m <- readMVar cfg
-     let ps = Text.splitOn "." prefix
+     let ps = dropWhile Text.null $ Text.splitOn "." prefix
         f :: [Text] -> ConfigLeaf -> WriterT (Seq (Doc Void)) IO ConfigLeaf
         f nm leaf = do d <- liftIO (ppConfigLeaf nm leaf)
                        tell (Seq.singleton d)
--- a/what4/src/What4/Protocol/Online.hs
+++ b/what4/src/What4/Protocol/Online.hs
@ -18,6 +18,8 @@ module What4.Protocol.Online
  ( OnlineSolver(..)
  , AnOnlineSolver(..)
  , SolverProcess(..)
+  , solverStdin
+  , solverResponse
  , SolverGoalTimeout(..)
  , getGoalTimeoutInSeconds
  , ErrorBehavior(..)
@ -134,12 +136,6 @@ data SolverProcess scope solver = SolverProcess
  , solverHandle :: !ProcessHandle
    -- ^ Handle to the solver process

-  , solverStdin :: !(Streams.OutputStream Text)
-    -- ^ Standard in for the solver process.
-
-  , solverResponse :: !(Streams.InputStream Text)
-    -- ^ Wrap the solver's stdout, for easier parsing of responses.
-
  , solverErrorBehavior :: !ErrorBehavior
    -- ^ Indicate this solver's behavior following an error response

@ -176,6 +172,15 @@ data SolverProcess scope solver = SolverProcess
  }


+-- | Standard input stream for the solver process.
+solverStdin :: (SolverProcess t solver) -> (Streams.OutputStream Text)
+solverStdin = connHandle . solverConn
+
+-- | The solver's stdout, for easier parsing of responses.
+solverResponse :: (SolverProcess t solver) -> (Streams.InputStream Text)
+solverResponse = connInputHandle . solverConn
+
+
 -- | An impolite way to shut down a solver.  Prefer to use
 --   `shutdownSolverProcess`, unless the solver is unresponsive
 --   or in some unrecoverable error state.
@ -396,7 +401,7 @@ getUnsatAssumptions proc =
     unless (supportedFeatures conn `hasProblemFeature` useUnsatAssumptions) $
       fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce UNSAT assumption lists"
     addCommandNoAck conn (getUnsatAssumptionsCommand conn)
-     smtUnsatAssumptionsResult conn (solverResponse proc)
+     smtUnsatAssumptionsResult conn conn

 -- | After an unsatisfiable check-sat command, compute a set of the named assertions
 --   that (together with all the unnamed assertions) form an unsatisfiable core.
@ -407,14 +412,13 @@ getUnsatCore proc =
     unless (supportedFeatures conn `hasProblemFeature` useUnsatCores) $
       fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce UNSAT cores"
     addCommandNoAck conn (getUnsatCoreCommand conn)
-     smtUnsatCoreResult conn (solverResponse proc)
+     smtUnsatCoreResult conn conn

 -- | Get the sat result from a previous SAT command.
 getSatResult :: SMTReadWriter s => SolverProcess t s -> IO (SatResult () ())
 getSatResult yp = do
  let ph = solverHandle yp
-  let err_reader = solverStderr yp
-  sat_result <- tryJust filterAsync (smtSatResult yp (solverResponse yp))
+  sat_result <- tryJust filterAsync (smtSatResult yp (solverConn yp))
  case sat_result of
    Right ok -> return ok

@ -422,7 +426,7 @@ getSatResult yp = do
       do -- Interrupt process
          terminateProcess ph

-          txt <- readAllLines err_reader
+          txt <- readAllLines $ solverStderr yp

          -- Wait for process to end
          ec <- waitForProcess ph
--- a/what4/src/What4/Protocol/SExp.hs
+++ b/what4/src/What4/Protocol/SExp.hs
@ -13,6 +13,7 @@ returned by SMT solvers.
 module What4.Protocol.SExp
  ( SExp(..)
  , parseSExp
+  , parseSExpBody
  , stringToSExp
  , parseNextWord
  , asAtomList
@ -61,16 +62,29 @@ isTokenChar c = not (isSpace c)
 readToken :: Parser Text
 readToken = takeWhile1 isTokenChar

+-- | Parses an SExp.  If the input is a string (recognized by the
+-- 'readString' argument), return that as an 'SString'; if the input
+-- is a single token, return that as an 'SAtom'.
+
 parseSExp ::
  Parser Text {- ^ A parser for string literals -} ->
  Parser SExp
 parseSExp readString = do
  skipSpaceOrNewline
-  msum [ char '(' *> skipSpaceOrNewline *> (SApp <$> many (parseSExp readString)) <* skipSpaceOrNewline <* char ')'
+  msum [ char '(' *> parseSExpBody readString
       , SString <$> readString
       , SAtom <$> readToken
       ]

+-- | Parses the body of an SExp after the opening '(' has already been
+-- parsed.
+
+parseSExpBody ::
+  Parser Text {- ^ A parser for string literals -} ->
+  Parser SExp
+parseSExpBody readString =
+  skipSpaceOrNewline *> (SApp <$> many (parseSExp readString)) <* skipSpaceOrNewline <* char ')'
+
 stringToSExp :: MonadFail m =>
  Parser Text {- ^ A parser for string literals -} ->
  String ->
@ -96,4 +110,4 @@ asAtomList (SApp xs) = go xs
  go [] = Just []
  go (SAtom a:ys) = (a:) <$> go ys
  go _ = Nothing
-asAtomList _ = Nothing
+asAtomList _ = Nothing
--- a/what4/src/What4/Protocol/SMTLib2.hs
+++ b/what4/src/What4/Protocol/SMTLib2.hs
@ -47,6 +47,7 @@ module What4.Protocol.SMTLib2
  , nameResult
  , setProduceModels
  , smtLibEvalFuns
+  , smtlib2Options
    -- * Logic
  , SMT2.Logic(..)
  , SMT2.qf_bv
@ -90,7 +91,6 @@ import Control.Monad.Fail( MonadFail )
 import           Control.Applicative
 import           Control.Exception
 import           Control.Monad.State.Strict
-import qualified Data.Attoparsec.Text as AT
 import qualified Data.BitVector.Sized as BV
 import qualified Data.Bits as Bits
 import           Data.ByteString (ByteString)
@ -121,7 +121,6 @@ import           Numeric.Natural
 import qualified System.Exit as Exit
 import qualified System.IO as IO
 import qualified System.IO.Streams as Streams
-import qualified System.IO.Streams.Attoparsec.Text as Streams
 import           Data.Versions (Version(..))
 import qualified Data.Versions as Versions
 import qualified Prettyprinter as PP
@ -130,6 +129,7 @@ import           LibBF( bfToBits )
 import           Prelude hiding (writeFile)

 import           What4.BaseTypes
+import qualified What4.Config as CFG
 import qualified What4.Expr.Builder as B
 import           What4.Expr.GroundEval
 import qualified What4.Interface as I
@ -139,6 +139,7 @@ import           What4.Protocol.ReadDecimal
 import           What4.Protocol.SExp
 import           What4.Protocol.SMTLib2.Syntax (Term, term_app, un_app, bin_app)

+import           What4.Protocol.SMTLib2.Response
 import qualified What4.Protocol.SMTLib2.Syntax as SMT2 hiding (Term)
 import qualified What4.Protocol.SMTWriter as SMTWriter
 import           What4.Protocol.SMTWriter hiding (assume, Term)
@ -154,6 +155,10 @@ all_supported :: SMT2.Logic
 all_supported = SMT2.allSupported
 {-# DEPRECATED all_supported "Use allSupported" #-}

+
+smtlib2Options :: [CFG.ConfigDesc]
+smtlib2Options = smtParseOptions
+
 ------------------------------------------------------------------------
 -- Floating point

@ -565,6 +570,8 @@ newWriter :: a
              --   (may be the @nullInput@ stream if no responses are expected)
          -> AcknowledgementAction t (Writer a)
             -- ^ Action to run for consuming acknowledgement messages
+          -> ResponseStrictness
+             -- ^ Be strict in parsing SMT solver responses?
          -> String
             -- ^ Name of solver for reporting purposes.
          -> Bool
@ -577,13 +584,13 @@ newWriter :: a
          -> B.SymbolVarBimap t
             -- ^ Variable bindings for names.
          -> IO (WriterConn t (Writer a))
-newWriter _ h in_h ack solver_name permitDefineFun arithOption quantSupport bindings = do
+newWriter _ h in_h ack isStrict solver_name permitDefineFun arithOption quantSupport bindings = do
  r <- newIORef Set.empty
  let initWriter =
        Writer
        { declaredTuples = r
        }
-  conn <- newWriterConn h in_h ack solver_name arithOption bindings initWriter
+  conn <- newWriterConn h in_h ack solver_name isStrict arithOption bindings initWriter
  return $! conn { supportFunctionDefs = permitDefineFun
                 , supportQuantifiers = quantSupport
                 }
@ -813,17 +820,6 @@ data Session t a = Session
  , sessionResponse :: !(Streams.InputStream Text)
  }

-parseSMTLib2String :: AT.Parser Text
-parseSMTLib2String = AT.char '\"' >> go
- where
- go :: AT.Parser Text
- go = do xs <- AT.takeWhile (not . (=='\"'))
-         _ <- AT.char '\"'
-         (do _ <- AT.char '\"'
-             ys <- go
-             return (xs <> "\"" <> ys)
-          ) <|> return xs
-
 -- | Get a value from a solver (must be called after checkSat)
 runGetValue :: SMTLib2Tweaks a
            => Session t a
@ -831,11 +827,10 @@ runGetValue :: SMTLib2Tweaks a
            -> IO SExp
 runGetValue s e = do
  writeGetValue (sessionWriter s) [ e ]
-  msexp <- try $ Streams.parseFromStream (parseSExp parseSMTLib2String) (sessionResponse s)
-  case msexp of
-    Left Streams.ParseException{} -> fail $ "Could not parse solver value."
-    Right (SApp [SApp [_, b]]) -> return b
-    Right sexp -> fail $ "Could not parse solver value:\n  " ++ show sexp
+  let valRsp = \case
+        AckSuccessSExp (SApp [SApp [_, b]]) -> Just b
+        _ -> Nothing
+  getLimitedSolverResponse "get value" valRsp (sessionWriter s) (SMT2.getValue [e])

 -- | This function runs a check sat command
 runCheckSat :: forall b t a.
@ -849,7 +844,7 @@ runCheckSat s doEval =
  do let w = sessionWriter s
         r = sessionResponse s
     addCommands w (checkCommands w)
-     res <- smtSatResult w r
+     res <- smtSatResult w w
     case res of
       Unsat x -> doEval (Unsat x)
       Unknown -> doEval Unknown
@ -857,93 +852,39 @@ runCheckSat s doEval =
         do evalFn <- smtExprGroundEvalFn w (smtEvalFuns w r)
            doEval (Sat (evalFn, Nothing))

-- | Called when methods in the following instance encounter an exception
-throwSMTLib2ParseError :: (Exception e) => Text -> SMT2.Command -> e -> m a
-throwSMTLib2ParseError what cmd e =
-  throw $ SMTLib2ParseError [cmd] $ Text.unlines
-    [ Text.unwords ["Could not parse result from", what, "."]
-    , "*** Exception: " <> Text.pack (displayException e)
-    ]
-
 instance SMTLib2Tweaks a => SMTReadWriter (Writer a) where
  smtEvalFuns w s = smtLibEvalFuns Session { sessionWriter = w
                                           , sessionResponse = s }

  smtSatResult p s =
-    do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s)
-       case mb of
-         Left (SomeException e) ->
-            fail $ unlines [ "Could not parse check_sat result."
-                           , "*** Exception: " ++ displayException e
-                           ]
-         Right (SAtom "unsat") -> return (Unsat ())
-         Right (SAtom "sat") -> return (Sat ())
-         Right (SAtom "unknown") -> return Unknown
-         Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error (head $ reverse (checkCommands p)) msg)
-         Right res -> throw $ SMTLib2ParseError (checkCommands p) (Text.pack (show res))
+    let satRsp = \case
+          AckSat     -> Just $ Sat ()
+          AckUnsat   -> Just $ Unsat ()
+          AckUnknown -> Just Unknown
+          _ -> Nothing
+    in getLimitedSolverResponse "sat result" satRsp s
+       (head $ reverse $ checkCommands p)

  smtUnsatAssumptionsResult p s =
-    do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s)
-       let cmd = getUnsatAssumptionsCommand p
-       case mb of
-         Right (asNegAtomList -> Just as) -> return as
-         Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg)
-         Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res)))
-         Left (SomeException e) ->
-           throwSMTLib2ParseError "unsat assumptions" cmd e
+    let unsatAssumpRsp = \case
+         AckSuccessSExp (asNegAtomList -> Just as) -> Just as
+         _ -> Nothing
+        cmd = getUnsatAssumptionsCommand p
+    in getLimitedSolverResponse "unsat assumptions" unsatAssumpRsp s cmd

  smtUnsatCoreResult p s =
-    do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s)
-       let cmd = getUnsatCoreCommand p
-       case mb of
-         Right (asAtomList -> Just nms) -> return nms
-         Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg)
-         Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res)))
-         Left (SomeException e) ->
-           throwSMTLib2ParseError "unsat core" cmd e
+    let unsatCoreRsp = \case
+          AckSuccessSExp (asAtomList -> Just nms) -> Just nms
+          _ -> Nothing
+        cmd = getUnsatCoreCommand p
+    in getLimitedSolverResponse "unsat core" unsatCoreRsp s cmd


-data SMTLib2Exception
-  = SMTLib2Unsupported SMT2.Command
-  | SMTLib2Error SMT2.Command Text
-  | SMTLib2ParseError [SMT2.Command] Text
-
-instance Show SMTLib2Exception where
-  show (SMTLib2Unsupported (SMT2.Cmd cmd)) =
-     unlines
-       [ "unsupported command:"
-       , "  " ++ Lazy.unpack (Builder.toLazyText cmd)
-       ]
-  show (SMTLib2Error (SMT2.Cmd cmd) msg) =
-     unlines
-       [ "Solver reported an error:"
-       , "  " ++ Text.unpack msg
-       , "in response to command:"
-       , "  " ++ Lazy.unpack (Builder.toLazyText cmd)
-       ]
-  show (SMTLib2ParseError cmds msg) =
-     unlines $
-       [ "Could not parse solver response:"
-       , "  " ++ Text.unpack msg
-       , "in response to commands:"
-       ] ++ map cmdToString cmds
-       where cmdToString (SMT2.Cmd cmd) =
-               "  " ++ Lazy.unpack (Builder.toLazyText cmd)
-
-instance Exception SMTLib2Exception
-
 smtAckResult :: AcknowledgementAction t (Writer a)
-smtAckResult = AckAction $ \conn cmd ->
-  do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) (connInputHandle conn))
-     case mb of
-       Right (SAtom "success") -> return ()
-       Right (SAtom "unsupported") -> throw (SMTLib2Unsupported cmd)
-       Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg)
-       Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res)))
-       Left (SomeException e) -> throw $ SMTLib2ParseError [cmd] $ Text.pack $
-               unlines [ "Could not parse acknowledgement result."
-                       , "*** Exception: " ++ displayException e
-                       ]
+smtAckResult = AckAction $ getLimitedSolverResponse "get ack" $ \case
+                 AckSuccess -> Just ()
+                 _ -> Nothing
+

 smtLibEvalFuns ::
  forall t a. SMTLib2Tweaks a => Session t a -> SMTEvalFunctions (Writer a)
@ -977,8 +918,8 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where

  defaultFeatures :: a -> ProblemFeatures

-  getErrorBehavior :: a -> WriterConn t (Writer a) -> Streams.InputStream Text -> IO ErrorBehavior
-  getErrorBehavior _ _ _ = return ImmediateExit
+  getErrorBehavior :: a -> WriterConn t (Writer a) -> IO ErrorBehavior
+  getErrorBehavior _ _ = return ImmediateExit

  supportsResetAssertions :: a -> Bool
  supportsResetAssertions _ = False
@ -989,12 +930,16 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
    :: a ->
       AcknowledgementAction t (Writer a) ->
       ProblemFeatures ->
+       -- | strictness override configuration
+       Maybe (CFG.ConfigOption I.BaseBoolType) ->
       B.ExprBuilder t st fs ->
       Streams.OutputStream Text ->
       Streams.InputStream Text ->
       IO (WriterConn t (Writer a))
-  newDefaultWriter solver ack feats sym h in_h =
-    newWriter solver h in_h ack (show solver) True feats True
+  newDefaultWriter solver ack feats strictOpt sym h in_h = do
+    let cfg = I.getConfiguration sym
+    strictness <- parserStrictness strictOpt strictSMTParsing cfg
+    newWriter solver h in_h ack strictness (show solver) True feats True
      =<< B.getSymbolVarBimap sym

  -- | Run the solver in a session.
@ -1002,6 +947,8 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
    :: a
    -> AcknowledgementAction t (Writer a)
    -> ProblemFeatures
+    -> Maybe (CFG.ConfigOption I.BaseBoolType)
+       -- ^ strictness override configuration
    -> B.ExprBuilder t st fs
    -> FilePath
      -- ^ Path to solver executable
@ -1009,7 +956,7 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
    -> (Session t a -> IO b)
      -- ^ Action to run
    -> IO b
-  withSolver solver ack feats sym path logData action = do
+  withSolver solver ack feats strictOpt sym path logData action = do
    args <- defaultSolverArgs solver sym
    withProcessHandles path args Nothing $
      \hdls@(in_h, out_h, err_h, _ph) -> do
@ -1018,7 +965,7 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
          demuxProcessHandles in_h out_h err_h
            (fmap (\x -> ("; ", x)) $ logHandle logData)

-        writer <- newDefaultWriter solver ack feats sym in_stream out_stream
+        writer <- newDefaultWriter solver ack feats strictOpt sym in_stream out_stream
        let s = Session
              { sessionWriter   = writer
              , sessionResponse = out_stream
@ -1044,19 +991,21 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
    :: a
    -> AcknowledgementAction t (Writer a)
    -> ProblemFeatures
+    -> Maybe (CFG.ConfigOption I.BaseBoolType)
+    -- ^ strictness override configuration
    -> B.ExprBuilder t st fs
    -> LogData
    -> [B.BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b)
    -> IO b
-  runSolverInOverride solver ack feats sym logData predicates cont = do
+  runSolverInOverride solver ack feats strictOpt sym logData predicates cont = do
    I.logSolverEvent sym
      (I.SolverStartSATQuery $ I.SolverStartSATQueryRec
        { I.satQuerySolverName = show solver
        , I.satQueryReason     = logReason logData
        })
    path <- defaultSolverPath solver sym
-    withSolver solver ack feats sym path (logData{logVerbosity=2}) $ \session -> do
+    withSolver solver ack feats strictOpt sym path (logData{logVerbosity=2}) $ \session -> do
      -- Assume the predicates hold.
      forM_ predicates (SMTWriter.assume (sessionWriter session))
      -- Run check SAT and get the model back.
@ -1076,15 +1025,19 @@ writeDefaultSMT2 :: SMTLib2Tweaks a
                    -- ^ Name of solver for reporting.
                 -> ProblemFeatures
                    -- ^ Features supported by solver
+                 -> Maybe (CFG.ConfigOption I.BaseBoolType)
+                    -- ^ strictness override configuration
                 -> B.ExprBuilder t st fs
                 -> IO.Handle
                 -> [B.BoolExpr t]
                 -> IO ()
-writeDefaultSMT2 a nm feat sym h ps = do
+writeDefaultSMT2 a nm feat strictOpt sym h ps = do
  bindings <- B.getSymbolVarBimap sym
  str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
  null_in <- Streams.nullInput
-  c <- newWriter a str null_in nullAcknowledgementAction nm True feat True bindings
+  let cfg = I.getConfiguration sym
+  strictness <- parserStrictness strictOpt strictSMTParsing cfg
+  c <- newWriter a str null_in nullAcknowledgementAction strictness nm True feat True bindings
  setProduceModels c True
  forM_ ps (SMTWriter.assume c)
  writeCheckSat c
@ -1097,10 +1050,12 @@ startSolver
        -- ^ Action for acknowledging command responses
  -> (WriterConn t (Writer a) -> IO ()) -- ^ Action for setting start-up-time options and logic
  -> ProblemFeatures
+  -> Maybe (CFG.ConfigOption I.BaseBoolType)
+  -- ^ strictness override configuration
  -> Maybe IO.Handle
  -> B.ExprBuilder t st fs
  -> IO (SolverProcess t (Writer a))
-startSolver solver ack setup feats auxOutput sym = do
+startSolver solver ack setup feats strictOpt auxOutput sym = do
  path <- defaultSolverPath solver sym
  args <- defaultSolverArgs solver sym
  hdls@(in_h, out_h, err_h, ph) <- startProcess path args Nothing
@ -1110,13 +1065,13 @@ startSolver solver ack setup feats auxOutput sym = do
       (fmap (\x -> ("; ", x)) auxOutput)

  -- Create writer
-  writer <- newDefaultWriter solver ack feats sym in_stream out_stream
+  writer <- newDefaultWriter solver ack feats strictOpt sym in_stream out_stream

  -- Set solver logic and solver-specific options
  setup writer

  -- Query the solver for it's error behavior
-  errBeh <- getErrorBehavior solver writer out_stream
+  errBeh <- getErrorBehavior solver writer

  earlyUnsatRef <- newIORef Nothing

@ -1126,11 +1081,9 @@ startSolver solver ack setup feats auxOutput sym = do
  return $! SolverProcess
            { solverConn     = writer
            , solverCleanupCallback = cleanupProcess hdls
-            , solverStdin    = in_stream
            , solverStderr   = err_reader
            , solverHandle   = ph
            , solverErrorBehavior = errBeh
-            , solverResponse = out_stream
            , solverEvalFuns = smtEvalFuns writer out_stream
            , solverLogFn    = I.logSolverEvent sym
            , solverName     = show solver
@ -1192,45 +1145,42 @@ ppSolverVersionError err =
        na Nothing  = "n/a"

 -- | Get the result of a version query
-nameResult :: Streams.InputStream Text -> IO Text
-nameResult s =
-  let cmd = SMT2.getName
-  in
-    tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) >>=
-      \case
-        Right (SApp [SAtom ":name", SString nm]) -> pure nm
-        Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg)
-        Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res)))
-        Left (SomeException e) ->
-          throwSMTLib2ParseError "name query" cmd e
+nameResult :: WriterConn t a -> IO Text
+nameResult conn =
+  getLimitedSolverResponse "solver name"
+  (\case
+      RspName nm -> Just nm
+      _ -> Nothing
+  )
+  conn SMT2.getName


 -- | Query the solver's error behavior setting
 queryErrorBehavior :: SMTLib2Tweaks a =>
-  WriterConn t (Writer a) -> Streams.InputStream Text -> IO ErrorBehavior
-queryErrorBehavior conn resp =
+  WriterConn t (Writer a) -> IO ErrorBehavior
+queryErrorBehavior conn =
  do let cmd = SMT2.getErrorBehavior
     writeCommand conn cmd
-     tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) resp) >>=
-       \case
-         Right (SApp [SAtom ":error-behavior", SAtom "continued-execution"]) -> return ContinueOnError
-         Right (SApp [SAtom ":error-behavior", SAtom "immediate-exit"]) -> return ImmediateExit
-         Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res)))
-         Left (SomeException e) -> throwSMTLib2ParseError "error behavior query" cmd e
+     getLimitedSolverResponse "error behavior"
+       (\case
+           RspErrBehavior bh -> case bh of
+             "continued-execution" -> return ContinueOnError
+             "immediate-exit" -> return ImmediateExit
+             _ -> throw $ SMTLib2ResponseUnrecognized cmd bh
+           _ -> Nothing
+       ) conn cmd


 -- | Get the result of a version query
-versionResult :: Streams.InputStream Text -> IO Text
-versionResult s =
-  let cmd = SMT2.getVersion
-  in
-    tryJust filterAsync (Streams.parseFromStream (parseSExp parseSMTLib2String) s) >>=
-      \case
-        Right (SApp [SAtom ":version", SString v]) -> pure v
-        Right (SApp [SAtom "error", SString msg]) -> throw (SMTLib2Error cmd msg)
-        Right res -> throw (SMTLib2ParseError [cmd] (Text.pack (show res)))
-        Left (SomeException e) ->
-          throwSMTLib2ParseError "version query" cmd e
+versionResult :: WriterConn t a -> IO Text
+versionResult conn =
+  getLimitedSolverResponse "solver version"
+  (\case
+      RspVersion v -> Just v
+      _ -> Nothing
+  )
+  conn SMT2.getVersion
+

 -- | Ensure the solver's version falls within a known-good range.
 checkSolverVersion' :: SMTLib2Tweaks solver =>
@ -1246,7 +1196,7 @@ checkSolverVersion' boundsMap proc =
    Nothing -> done
    Just bnds ->
      do getVersion conn
-         res <- versionResult (solverResponse proc)
+         res <- versionResult $ solverConn proc
         case Versions.version res of
           Left e -> pure (Left (UnparseableVersion e))
           Right actualVer ->
--- a/what4/src/What4/Protocol/SMTLib2/Response.hs
+++ b/what4/src/What4/Protocol/SMTLib2/Response.hs
@ -0,0 +1,241 @@
+{-|
+This module defines types and operations for parsing SMTLib2 solver responses.
+
+These are high-level responses, as describe in
+@https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf@,
+page 47, Figure 3.9.
+
+This parser is designed to be the top level handling for solver
+responses, and to be used in conjuction with
+What4.Protocol.SMTLib2.Parse and What4.Protocol.SExp with the latter
+handling detailed parsing of specific constructs returned in the body
+of the general response.
+-}
+
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module What4.Protocol.SMTLib2.Response
+  (
+    SMTResponse(..)
+  , SMTLib2Exception(..)
+  , getSolverResponse
+  , getLimitedSolverResponse
+  , smtParseOptions
+  , strictSMTParsing
+  , strictSMTParseOpt
+  )
+where
+
+import           Control.Applicative
+import           Control.Exception
+import qualified Data.Attoparsec.Text as AT
+import           Data.Text ( Text )
+import qualified Data.Text as Text
+import qualified Data.Text.Lazy as Lazy
+import qualified Data.Text.Lazy.Builder as Builder
+import qualified Prettyprinter.Util as PPU
+import qualified System.IO.Streams as Streams
+import qualified System.IO.Streams.Attoparsec.Text as AStreams
+
+import qualified What4.BaseTypes as BT
+import qualified What4.Config as CFG
+import           What4.Protocol.SExp
+import qualified What4.Protocol.SMTLib2.Syntax as SMT2
+import qualified What4.Protocol.SMTWriter as SMTWriter
+import           What4.Utils.Process ( filterAsync )
+
+
+strictSMTParsing :: CFG.ConfigOption BT.BaseBoolType
+strictSMTParsing = CFG.configOption BT.BaseBoolRepr "solver.strict_parsing"
+
+strictSMTParseOpt :: CFG.ConfigDesc
+strictSMTParseOpt =
+  CFG.mkOpt strictSMTParsing CFG.boolOptSty
+  (Just $ PPU.reflow $
+   Text.concat ["Strictly parse SMT responses and fail on"
+               , "unrecognized data (the default)."
+               , "This might need to be disabled when running"
+               , "the SMT solver in verbose mode."
+               ])
+  Nothing
+
+smtParseOptions :: [CFG.ConfigDesc]
+smtParseOptions = [ strictSMTParseOpt ]
+
+
+data SMTResponse = AckSuccess
+                 | AckUnsupported
+                 | AckError Text
+                 | AckSat
+                 | AckUnsat
+                 | AckUnknown
+                 | RspName Text
+                 | RspVersion Text
+                 | RspErrBehavior Text
+                 | RspOutOfMemory
+                 | RspRsnIncomplete
+                 | RspUnkReason SExp
+                 | AckSuccessSExp SExp
+                 | AckSkipped Text SMTResponse
+                 deriving (Eq, Show)
+
+-- | Called to get a response from the SMT connection.
+
+getSolverResponse :: SMTWriter.WriterConn t h
+                  -> IO (Either SomeException SMTResponse)
+getSolverResponse conn = do
+  mb <- tryJust filterAsync
+        (AStreams.parseFromStream
+          (rspParser (SMTWriter.strictParsing conn))
+          (SMTWriter.connInputHandle conn))
+  return mb
+
+
+-- | Gets a limited set of responses, throwing an exception when a
+-- response is not matched by the filter.  Also throws exceptions for
+-- standard error results.  The passed command and intent arguments
+-- are only used for marking error messages.
+--
+-- Callers which do not want exceptions thrown for standard error
+-- conditions should feel free to use 'getSolverResponse' and handle
+-- all response cases themselves.
+
+getLimitedSolverResponse :: String
+                         -> (SMTResponse -> Maybe a)
+                         -> SMTWriter.WriterConn t h
+                         -> SMT2.Command
+                         -> IO a
+getLimitedSolverResponse intent handleResponse conn cmd =
+  let validateResp rsp =
+        case rsp of
+          AckUnsupported -> throw (SMTLib2Unsupported cmd)
+          (AckError msg) -> throw (SMTLib2Error cmd msg)
+          (AckSkipped line rest) -> validateResp rest
+          _ -> case handleResponse rsp of
+                 Just x -> return x
+                 Nothing -> throw $ SMTLib2InvalidResponse cmd intent rsp
+  in getSolverResponse conn >>= \case
+    Right rsp -> validateResp rsp
+    Left (SomeException e) -> do
+      curInp <- Streams.read (SMTWriter.connInputHandle conn)
+      throw $ SMTLib2ParseError intent [cmd] $ Text.pack $
+        unlines [ "Solver response parsing failure."
+                , "*** Exception: " ++ displayException e
+                , "Attempting to parse input for " <> intent <> ":"
+                , show curInp
+                ]
+
+
+rspParser :: SMTWriter.ResponseStrictness -> AT.Parser SMTResponse
+rspParser strictness =
+  let lexeme p = skipSpaceOrNewline *> p
+      parens p = AT.char '(' *> p <* AT.char ')'
+      errParser = parens $ lexeme (AT.string "error")
+                  *> (AckError <$> lexeme parseSMTLib2String)
+      specific_success_response = check_sat_response <|> get_info_response
+      check_sat_response = (AckSat <$ AT.string "sat")
+                           <|> (AckUnsat <$ AT.string "unsat")
+                           <|> (AckUnknown <$ AT.string "unknown")
+      get_info_response = parens info_response
+      info_response = errBhvParser
+                      <|> nameParser
+                      <|> unkReasonParser
+                      <|> versionParser
+      nameParser = lexeme (AT.string ":name")
+                   *> lexeme (RspName <$> parseSMTLib2String)
+      versionParser = lexeme (AT.string ":version")
+                      *> lexeme (RspVersion <$> parseSMTLib2String)
+      errBhvParser = lexeme (AT.string ":error-behavior")
+                     *> lexeme (RspErrBehavior <$>
+                                (AT.string "continued-execution"
+                                 <|> AT.string "immediate-exit")
+                                 -- Explicit error instead of generic
+                                 -- fallback since :error-behavior was
+                                 -- matched but behavior type was not.
+                                 <|> throw (SMTLib2ResponseUnrecognized
+                                            SMT2.getErrorBehavior
+                                            "bad :error-behavior value")
+                               )
+      unkReasonParser =
+        lexeme (AT.string ":reason-unknown")
+        *> lexeme (RspOutOfMemory <$ AT.string "memout"
+                    <|> RspRsnIncomplete <$ AT.string "incomplete"
+                    <|> (AT.char '(' *> (RspUnkReason <$> parseSExpBody parseSMTLib2String))
+                    -- already matched :reason-unknown, so any other
+                    -- arguments to that are errors.
+                    <|> throw (SMTLib2ResponseUnrecognized
+                               (SMT2.Cmd "reason?")
+                               "bad :reason-unknown value")
+                  )
+  in skipSpaceOrNewline *>
+     ((AckSuccess <$ AT.string "success")
+      <|> (AckUnsupported <$ AT.string "unsupported")
+      <|> specific_success_response
+      <|> errParser
+      <|> (AT.char '(' *> (AckSuccessSExp <$> parseSExpBody parseSMTLib2String))
+      -- sometimes verbose output mode will generate interim text
+      -- before the actual ack; the following skips lines of input
+      -- that aren't recognized.
+       <|> (case strictness of
+              SMTWriter.Strict -> empty
+              SMTWriter.Lenient -> AckSkipped
+                                   <$> AT.takeWhile1 (not . AT.isEndOfLine)
+                                   <*> (rspParser strictness))
+     )
+
+parseSMTLib2String :: AT.Parser Text
+parseSMTLib2String = AT.char '\"' >> go
+ where
+ go :: AT.Parser Text
+ go = do xs <- AT.takeWhile (not . (=='\"'))
+         _ <- AT.char '\"'
+         (do _ <- AT.char '\"'
+             ys <- go
+             return (xs <> "\"" <> ys)
+          ) <|> return xs
+
+----------------------------------------------------------------------
+
+data SMTLib2Exception
+  = SMTLib2Unsupported SMT2.Command
+  | SMTLib2Error SMT2.Command Text
+  | SMTLib2ParseError SMTLib2Intent [SMT2.Command] Text
+  | SMTLib2ResponseUnrecognized SMT2.Command Text
+  | SMTLib2InvalidResponse SMT2.Command SMTLib2Intent SMTResponse
+
+type SMTLib2Intent = String
+
+instance Show SMTLib2Exception where
+  show =
+    let showCmd (SMT2.Cmd c) = Lazy.unpack $ Builder.toLazyText c
+    in unlines . \case
+      (SMTLib2Unsupported cmd) ->
+        [ "unsupported command:"
+        , "  " <> showCmd cmd
+        ]
+      (SMTLib2Error cmd msg) ->
+        [ "Solver reported an error:"
+        , "  " ++ Text.unpack msg
+        , "in response to command:"
+        , "  " <> showCmd cmd
+        ]
+      (SMTLib2ParseError intent cmds msg) ->
+        [ "Could not parse solver response:"
+        , "  " ++ Text.unpack msg
+        , "in response to commands for " <> intent <> ":"
+        ] ++ map showCmd cmds
+      (SMTLib2ResponseUnrecognized cmd rsp) ->
+        [ "Unrecognized response from solver:"
+        , "  " <> Text.unpack rsp
+        , "in response to command:"
+        , "  " <> showCmd cmd
+        ]
+      (SMTLib2InvalidResponse cmd intent rsp) ->
+        [ "Received parsed and understood but unexpected response from solver:"
+        , "  " <> show rsp
+        , "in response to command for " <> intent <> ":"
+        , "  " <> showCmd cmd
+        ]
+
+instance Exception SMTLib2Exception
--- a/what4/src/What4/Protocol/SMTWriter.hs
+++ b/what4/src/What4/Protocol/SMTWriter.hs
@ -57,6 +57,7 @@ module What4.Protocol.SMTWriter
              , supportFunctionArguments
              , supportQuantifiers
              , supportedFeatures
+              , strictParsing
              , connHandle
              , connInputHandle
              , smtWriterName
@ -82,6 +83,8 @@ module What4.Protocol.SMTWriter
  , assumeFormulaWithFreshName
  , DefineStyle(..)
  , AcknowledgementAction(..)
+  , ResponseStrictness(..)
+  , parserStrictness
  , nullAcknowledgementAction
    -- * SMTWriter operations
  , assume
@ -102,7 +105,7 @@ import Control.Monad.Fail( MonadFail )
 #endif

 import           Control.Exception
-import           Control.Lens hiding ((.>))
+import           Control.Lens hiding ((.>), Strict)
 import           Control.Monad.Extra
 import           Control.Monad.IO.Class
 import           Control.Monad.Reader
@ -138,15 +141,16 @@ import           System.IO.Streams (OutputStream, InputStream)
 import qualified System.IO.Streams as Streams

 import           What4.BaseTypes
-import           What4.Interface (RoundingMode(..), stringInfo)
-import           What4.ProblemFeatures
+import qualified What4.Config as CFG
 import qualified What4.Expr.ArrayUpdateMap as AUM
 import qualified What4.Expr.BoolMap as BM
 import           What4.Expr.Builder
 import           What4.Expr.GroundEval
 import qualified What4.Expr.StringSeq as SSeq
-import qualified What4.Expr.WeightedSum as WSum
 import qualified What4.Expr.UnaryBV as UnaryBV
+import qualified What4.Expr.WeightedSum as WSum
+import           What4.Interface (RoundingMode(..), stringInfo)
+import           What4.ProblemFeatures
 import           What4.ProgramLoc
 import           What4.SatResult
 import qualified What4.SemiRing as SR
@ -589,6 +593,7 @@ data StackEntry t (h :: Type) = StackEntry
 data WriterConn t (h :: Type) =
  WriterConn { smtWriterName :: !String
               -- ^ Name of writer for error reporting purposes.
+
             , connHandle :: !(OutputStream Text)
               -- ^ Handle to write to

@ -612,6 +617,9 @@ data WriterConn t (h :: Type) =
               -- indices.
             , supportQuantifiers :: !Bool
               -- ^ Allow the SMT writer to generate problems with quantifiers.
+             , strictParsing :: !ResponseStrictness
+               -- ^ Be strict in parsing SMTLib2 responses; no
+               -- verbosity or variants allowed
             , supportedFeatures :: !ProblemFeatures
               -- ^ Indicates features supported by the solver.
             , entryStack :: !(IORef [StackEntry t h])
@ -701,6 +709,8 @@ newWriterConn :: OutputStream Text
              -- ^ An action to consume solver acknowledgement responses
              -> String
              -- ^ Name of solver for reporting purposes.
+              -> ResponseStrictness
+              -- ^ Be strict in parsing responses?
              -> ProblemFeatures
              -- ^ Indicates what features are supported by the solver.
              -> SymbolVarBimap t
@ -708,7 +718,7 @@ newWriterConn :: OutputStream Text
              -- canonical name (if any).
              -> cs -- ^ State information specific to the type of connection
              -> IO (WriterConn t cs)
-newWriterConn h in_h ack solver_name features bindings cs = do
+newWriterConn h in_h ack solver_name beStrict features bindings cs = do
  entry <- newStackEntry
  stk_ref <- newIORef [entry]
  r <- newIORef emptyState
@ -718,6 +728,7 @@ newWriterConn h in_h ack solver_name features bindings cs = do
                       , supportFunctionDefs      = False
                       , supportFunctionArguments = False
                       , supportQuantifiers       = False
+                       , strictParsing            = beStrict
                       , supportedFeatures        = features
                       , entryStack   = stk_ref
                       , stateRef     = r
@ -726,6 +737,29 @@ newWriterConn h in_h ack solver_name features bindings cs = do
                       , consumeAcknowledgement = ack
                       }

+-- | Strictness level for parsing solver responses.
+data ResponseStrictness
+  = Lenient  -- ^ allows other output preceeding recognized solver responses
+  | Strict   -- ^ parse _only_ recognized solver responses; fail on anything else
+  deriving (Eq, Show)
+
+-- | Given an optional override configuration option, return the SMT
+-- response parsing strictness that should be applied based on the
+-- override or thedefault strictSMTParsing configuration.
+parserStrictness :: Maybe (CFG.ConfigOption BaseBoolType)
+                 -> CFG.ConfigOption BaseBoolType
+                 -> CFG.Config
+                 -> IO ResponseStrictness
+parserStrictness overrideOpt strictOpt cfg = do
+  ovr <- case overrideOpt of
+           Nothing -> return Nothing
+           Just o -> CFG.getMaybeOpt =<< CFG.getOptionSetting o cfg
+  optval <- case ovr of
+              Just v -> return $ Just v
+              Nothing -> CFG.getMaybeOpt =<< CFG.getOptionSetting strictOpt cfg
+  return $ maybe Strict (\c -> if c then Strict else Lenient) optval
+
+
 -- | Status to indicate when term value will be uncached.
 data TermLifetime
   = DeleteNever
@ -2865,16 +2899,16 @@ class SMTWriter h => SMTReadWriter h where
    WriterConn t h -> Streams.InputStream Text -> SMTEvalFunctions h

  -- | Parse a set result from the solver's response.
-  smtSatResult :: f h -> Streams.InputStream Text -> IO (SatResult () ())
+  smtSatResult :: f h -> WriterConn t h -> IO (SatResult () ())

  -- | Parse a list of names of assumptions that form an unsatisfiable core.
  --   These correspond to previously-named assertions.
-  smtUnsatCoreResult :: f h -> Streams.InputStream Text -> IO [Text]
+  smtUnsatCoreResult :: f h -> WriterConn t h -> IO [Text]

  -- | Parse a list of names of assumptions that form an unsatisfiable core.
  --   The boolean indicates the polarity of the atom: true for an ordinary
  --   atom, false for a negated atom.
-  smtUnsatAssumptionsResult :: f h -> Streams.InputStream Text -> IO [(Bool,Text)]
+  smtUnsatAssumptionsResult :: f h -> WriterConn t h -> IO [(Bool,Text)]


 -- | Return the terms associated with the given ground index variables.
--- a/what4/src/What4/Solver.hs
+++ b/what4/src/What4/Solver.hs
@ -45,6 +45,7 @@ module What4.Solver
  , CVC4(..)
  , cvc4Adapter
  , cvc4Path
+  , cvc4Timeout
  , runCVC4InOverride
  , writeCVC4SMT2File
  , withCVC4
@ -71,6 +72,9 @@ module What4.Solver
    -- * Yices
  , yicesAdapter
  , yicesPath
+  , yicesEnableMCSat
+  , yicesEnableInteractive
+  , yicesGoalTimeout
  , runYicesInOverride
  , writeYicesFile
  , yicesOptions
@ -79,6 +83,7 @@ module What4.Solver
    -- * Z3
  , Z3(..)
  , z3Path
+  , z3Timeout
  , z3Adapter
  , runZ3InOverride
  , withZ3
--- a/what4/src/What4/Solver/Adapter.hs
+++ b/what4/src/What4/Solver/Adapter.hs
@ -112,8 +112,16 @@ defaultWriteSMTLIB2Features
  .|. useSymbolicArrays

 defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
-defaultSolverAdapter = configOption (BaseStringRepr UnicodeRepr) "default_solver"
+defaultSolverAdapter = configOption (BaseStringRepr UnicodeRepr) "solver.default"

+deprecatedDefaultSolverAdapterConfig :: ConfigOption (BaseStringType Unicode)
+deprecatedDefaultSolverAdapterConfig = configOption (BaseStringRepr UnicodeRepr) "default_solver"
+
+
+-- Given a list of solver adapters, returns a tuple of the full set of
+-- solver config options for all adapters (plus a configuration to
+-- specify the default adapter) and an IO operation that will return
+-- current default adapter when executed.

 solverAdapterOptions ::
  [SolverAdapter st] ->
@ -121,7 +129,7 @@ solverAdapterOptions ::
 solverAdapterOptions [] = fail "No solver adapters specified!"
 solverAdapterOptions xs@(def:_) =
  do ref <- newIORef def
-     let opts = sty ref : concatMap solver_adapter_config_options xs
+     let opts = sty ref : sty' ref : concatMap solver_adapter_config_options xs
     return (opts, readIORef ref)

 where
@ -131,6 +139,11 @@ solverAdapterOptions xs@(def:_) =
                 (listOptSty (vals ref))
                 (Just (PP.pretty "Indicates which solver to use for check-sat queries"))
                 (Just (ConcreteString (UnicodeLiteral (T.pack (solver_adapter_name def)))))
+ sty' ref = deprecatedOpt [sty ref] $
+            mkOpt deprecatedDefaultSolverAdapterConfig
+                  (listOptSty (vals ref))
+                  (Just (PP.pretty "Indicates which solver to use for check-sat queries."))
+                  (Just (ConcreteString (UnicodeLiteral (T.pack (solver_adapter_name def)))))

 -- | Test the ability to interact with a solver by peforming a check-sat query
 --   on a trivially unsatisfiable problem.
--- a/what4/src/What4/Solver/Boolector.hs
+++ b/what4/src/What4/Solver/Boolector.hs
@ -30,35 +30,46 @@ import           Control.Monad
 import           Data.Bits ( (.|.) )

 import           What4.BaseTypes
-import           What4.Config
 import           What4.Concrete
-import           What4.Interface
-import           What4.ProblemFeatures
-import           What4.SatResult
+import           What4.Config
 import           What4.Expr.Builder
 import           What4.Expr.GroundEval
-import           What4.Solver.Adapter
+import           What4.Interface
+import           What4.ProblemFeatures
 import           What4.Protocol.Online
 import qualified What4.Protocol.SMTLib2 as SMT2
+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
+import           What4.SatResult
+import           What4.Solver.Adapter
 import           What4.Utils.Process


-
-
 data Boolector = Boolector deriving Show

 -- | Path to boolector
 boolectorPath :: ConfigOption (BaseStringType Unicode)
-boolectorPath = configOption knownRepr "boolector_path"
+boolectorPath = configOption knownRepr "solver.boolector.path"
+
+boolectorPathOLD :: ConfigOption (BaseStringType Unicode)
+boolectorPathOLD = configOption knownRepr "boolector_path"
+
+-- | Control strict parsing for Boolector solver responses (defaults
+-- to solver.strict-parsing option setting).
+boolectorStrictParsing :: ConfigOption BaseBoolType
+boolectorStrictParsing = configOption knownRepr "solver.boolector.strict_parsing"

 boolectorOptions :: [ConfigDesc]
 boolectorOptions =
-  [ mkOpt
-      boolectorPath
-      executablePathOptSty
-      (Just "Path to boolector executable")
-      (Just (ConcreteString "boolector"))
-  ]
+  let bpOpt co = mkOpt
+                 co
+                 executablePathOptSty
+                 (Just "Path to boolector executable")
+                 (Just (ConcreteString "boolector"))
+      bp = bpOpt boolectorPath
+      bp2 = deprecatedOpt [bp] $ bpOpt boolectorPathOLD
+  in [ bp, bp2
+     , copyOpt (const $ configOptionText boolectorStrictParsing) strictSMTParseOpt
+     ] <> SMT2.smtlib2Options

 boolectorAdapter :: SolverAdapter st
 boolectorAdapter =
@ -68,6 +79,7 @@ boolectorAdapter =
  , solver_adapter_check_sat = runBoolectorInOverride
  , solver_adapter_write_smt2 =
      SMT2.writeDefaultSMT2 () "Boolector" defaultWriteSMTLIB2Features
+      (Just boolectorStrictParsing)
  }

 instance SMT2.SMTLib2Tweaks Boolector where
@ -80,7 +92,8 @@ runBoolectorInOverride ::
  (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) ->
  IO a
 runBoolectorInOverride =
-  SMT2.runSolverInOverride Boolector SMT2.nullAcknowledgementAction boolectorFeatures
+  SMT2.runSolverInOverride Boolector SMT2.nullAcknowledgementAction
+  boolectorFeatures (Just boolectorStrictParsing)

 -- | Run Boolector in a session. Boolector will be configured to produce models, but
 -- otherwise left with the default configuration.
@ -92,7 +105,8 @@ withBoolector
  -> (SMT2.Session t Boolector -> IO a)
    -- ^ Action to run
  -> IO a
-withBoolector = SMT2.withSolver Boolector SMT2.nullAcknowledgementAction boolectorFeatures
+withBoolector = SMT2.withSolver Boolector SMT2.nullAcknowledgementAction
+                boolectorFeatures (Just boolectorStrictParsing)


 boolectorFeatures :: ProblemFeatures
@ -120,5 +134,7 @@ setInteractiveLogicAndOptions writer = do
    SMT2.setLogic writer SMT2.allSupported

 instance OnlineSolver (SMT2.Writer Boolector) where
-  startSolverProcess = SMT2.startSolver Boolector SMT2.smtAckResult setInteractiveLogicAndOptions
+  startSolverProcess feat = SMT2.startSolver Boolector SMT2.smtAckResult
+                            setInteractiveLogicAndOptions feat
+                            (Just boolectorStrictParsing)
  shutdownSolverProcess = SMT2.shutdownSolver Boolector
--- a/what4/src/What4/Solver/CVC4.hs
+++ b/what4/src/What4/Solver/CVC4.hs
@ -35,18 +35,20 @@ import           System.IO
 import qualified System.IO.Streams as Streams

 import           What4.BaseTypes
-import           What4.Config
-import           What4.Solver.Adapter
 import           What4.Concrete
-import           What4.Interface
-import           What4.ProblemFeatures
-import           What4.SatResult
+import           What4.Config
 import           What4.Expr.Builder
 import           What4.Expr.GroundEval
+import           What4.Interface
+import           What4.ProblemFeatures
 import           What4.Protocol.Online
 import qualified What4.Protocol.SMTLib2 as SMT2
+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
+import qualified What4.Protocol.SMTLib2.Response as RSP
 import qualified What4.Protocol.SMTLib2.Syntax as Syntax
 import           What4.Protocol.SMTWriter
+import           What4.SatResult
+import           What4.Solver.Adapter
 import           What4.Utils.Process


@ -58,27 +60,49 @@ data CVC4 = CVC4 deriving Show

 -- | Path to cvc4
 cvc4Path :: ConfigOption (BaseStringType Unicode)
-cvc4Path = configOption knownRepr "cvc4_path"
+cvc4Path = configOption knownRepr "solver.cvc4.path"
+
+cvc4PathOLD :: ConfigOption (BaseStringType Unicode)
+cvc4PathOLD = configOption knownRepr "cvc4_path"

 cvc4RandomSeed :: ConfigOption BaseIntegerType
-cvc4RandomSeed = configOption knownRepr "cvc4.random-seed"
+cvc4RandomSeed = configOption knownRepr "solver.cvc4.random-seed"
+
+cvc4RandomSeedOLD :: ConfigOption BaseIntegerType
+cvc4RandomSeedOLD = configOption knownRepr "cvc4.random-seed"

 -- | Per-check timeout, in milliseconds (zero is none)
 cvc4Timeout :: ConfigOption BaseIntegerType
-cvc4Timeout = configOption knownRepr "cvc4_timeout"
+cvc4Timeout = configOption knownRepr "solver.cvc4.timeout"
+
+cvc4TimeoutOLD :: ConfigOption BaseIntegerType
+cvc4TimeoutOLD = configOption knownRepr "cvc4_timeout"
+
+-- | Control strict parsing for Boolector solver responses (defaults
+-- to solver.strict-parsing option setting).
+cvc4StrictParsing :: ConfigOption BaseBoolType
+cvc4StrictParsing = configOption knownRepr "solver.cvc4.strict_parsing"

 cvc4Options :: [ConfigDesc]
 cvc4Options =
-  [ mkOpt cvc4Path
-          executablePathOptSty
-          (Just "Path to CVC4 executable")
-          (Just (ConcreteString "cvc4"))
-  , intWithRangeOpt cvc4RandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1)
-  , mkOpt cvc4Timeout
-          integerOptSty
-          (Just "Per-check timeout in milliseconds (zero is none)")
-          (Just (ConcreteInteger 0))
-  ]
+  let pathOpt co = mkOpt co
+                   executablePathOptSty
+                   (Just "Path to CVC4 executable")
+                   (Just (ConcreteString "cvc4"))
+      p1 = pathOpt cvc4Path
+      r1 = intWithRangeOpt cvc4RandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1)
+      tmOpt co = mkOpt co
+                 integerOptSty
+                 (Just "Per-check timeout in milliseconds (zero is none)")
+                 (Just (ConcreteInteger 0))
+      t1 = tmOpt cvc4Timeout
+  in [ p1, r1, t1
+     , copyOpt (const $ configOptionText cvc4StrictParsing) strictSMTParseOpt
+     , deprecatedOpt [p1] $ pathOpt cvc4PathOLD
+     , deprecatedOpt [r1] $ intWithRangeOpt cvc4RandomSeedOLD
+       (negate (2^(30::Int)-1)) (2^(30::Int)-1)
+     , deprecatedOpt [t1] $ tmOpt cvc4TimeoutOLD
+     ] <> SMT2.smtlib2Options

 cvc4Adapter :: SolverAdapter st
 cvc4Adapter =
@ -130,7 +154,11 @@ writeMultiAsmpCVC4SMT2File sym h ps = do
  bindings <- getSymbolVarBimap sym
  out_str  <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
  in_str <- Streams.nullInput
-  c <- SMT2.newWriter CVC4 out_str in_str nullAcknowledgementAction "CVC4"
+  let cfg = getConfiguration sym
+  strictness <- maybe Strict
+                (\c -> if fromConcreteBool c then Strict else Lenient) <$>
+                (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
+  c <- SMT2.newWriter CVC4 out_str in_str nullAcknowledgementAction strictness "CVC4"
         True cvc4Features True bindings
  SMT2.setLogic c SMT2.allSupported
  SMT2.setProduceModels c True
@ -174,7 +202,8 @@ runCVC4InOverride
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
-runCVC4InOverride = SMT2.runSolverInOverride CVC4 nullAcknowledgementAction (SMT2.defaultFeatures CVC4)
+runCVC4InOverride = SMT2.runSolverInOverride CVC4 nullAcknowledgementAction
+                    (SMT2.defaultFeatures CVC4) (Just cvc4StrictParsing)

 -- | Run CVC4 in a session. CVC4 will be configured to produce models, but
 -- otherwise left with the default configuration.
@ -186,7 +215,8 @@ withCVC4
  -> (SMT2.Session t CVC4 -> IO a)
    -- ^ Action to run
  -> IO a
-withCVC4 = SMT2.withSolver CVC4 nullAcknowledgementAction (SMT2.defaultFeatures CVC4)
+withCVC4 = SMT2.withSolver CVC4 nullAcknowledgementAction
+           (SMT2.defaultFeatures CVC4) (Just cvc4StrictParsing)

 setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
@ -207,7 +237,8 @@ setInteractiveLogicAndOptions writer = do

 instance OnlineSolver (SMT2.Writer CVC4) where
  startSolverProcess feat mbIOh sym = do
-    sp <- SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions feat mbIOh sym
+    sp <- SMT2.startSolver CVC4 SMT2.smtAckResult setInteractiveLogicAndOptions
+          feat (Just cvc4StrictParsing) mbIOh sym
    timeout <- SolverGoalTimeout <$>
               (getOpt =<< getOptionSetting cvc4Timeout (getConfiguration sym))
    return $ sp { solverGoalTimeout = timeout }
--- a/what4/src/What4/Solver/DReal.hs
+++ b/what4/src/What4/Solver/DReal.hs
@ -56,6 +56,7 @@ import           What4.SatResult
 import           What4.Expr.Builder
 import           What4.Expr.GroundEval
 import qualified What4.Protocol.SMTLib2 as SMT2
+import qualified What4.Protocol.SMTLib2.Response as RSP
 import qualified What4.Protocol.SMTWriter as SMTWriter
 import           What4.Utils.Process
 import           What4.Utils.Streams (logErrorStream)
@ -65,16 +66,21 @@ data DReal = DReal deriving Show

 -- | Path to dReal
 drealPath :: ConfigOption (BaseStringType Unicode)
-drealPath = configOption knownRepr "dreal_path"
+drealPath = configOption knownRepr "solver.dreal.path"
+
+drealPathOLD :: ConfigOption (BaseStringType Unicode)
+drealPathOLD = configOption knownRepr "dreal_path"

 drealOptions :: [ConfigDesc]
 drealOptions =
-  [ mkOpt
-      drealPath
-      executablePathOptSty
-      (Just "Path to dReal executable")
-      (Just (ConcreteString "dreal"))
-  ]
+  let dpOpt co = mkOpt co
+                 executablePathOptSty
+                 (Just "Path to dReal executable")
+                 (Just (ConcreteString "dreal"))
+      dp = dpOpt drealPath
+  in [ dp
+     , deprecatedOpt [dp] $ dpOpt drealPathOLD
+     ] <> SMT2.smtlib2Options

 drealAdapter :: SolverAdapter st
 drealAdapter =
@ -106,7 +112,13 @@ writeDRealSMT2File sym h ps = do
  bindings <- getSymbolVarBimap sym
  out_str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
  in_str <- Streams.nullInput
-  c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction "dReal"
+  let cfg = getConfiguration sym
+  strictness <- maybe SMTWriter.Strict
+                (\c -> if fromConcreteBool c
+                       then SMTWriter.Strict
+                       else SMTWriter.Lenient) <$>
+                (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
+  c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal"
          False useComputableReals False bindings
  SMT2.setProduceModels c True
  SMT2.setLogic c (SMT2.Logic "QF_NRA")
@ -299,7 +311,14 @@ runDRealInOverride sym logData ps modelFn = do

      in_str <- Streams.nullInput

-      c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction "dReal"
+      let cfg = getConfiguration sym
+      strictness <- maybe SMTWriter.Strict
+                    (\c -> if fromConcreteBool c
+                           then SMTWriter.Strict
+                           else SMTWriter.Lenient) <$>
+                    (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
+
+      c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal"
             False useComputableReals False bindings

      -- Set the dReal default logic
--- a/what4/src/What4/Solver/ExternalABC.hs
+++ b/what4/src/What4/Solver/ExternalABC.hs
@ -35,6 +35,7 @@ import           What4.Expr.GroundEval
 import           What4.Interface
 import           What4.ProblemFeatures
 import qualified What4.Protocol.SMTLib2 as SMT2
+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
 import           What4.Protocol.SMTWriter
 import           What4.SatResult
 import           What4.Solver.Adapter
@ -44,16 +45,27 @@ data ExternalABC = ExternalABC deriving Show

 -- | Path to ABC
 abcPath :: ConfigOption (BaseStringType Unicode)
-abcPath = configOption knownRepr "abc_path"
+abcPath = configOption knownRepr "solver.abc.path"
+
+abcPathOLD :: ConfigOption (BaseStringType Unicode)
+abcPathOLD = configOption knownRepr "abc_path"
+
+-- | Control strict parsing for ABC solver responses (defaults
+-- to solver.strict-parsing option setting).
+abcStrictParsing :: ConfigOption BaseBoolType
+abcStrictParsing = configOption knownRepr "solver.abc.strict_parsing"

 abcOptions :: [ConfigDesc]
 abcOptions =
-  [ mkOpt
-      abcPath
-      executablePathOptSty
-      (Just "ABC executable path")
-      (Just (ConcreteString "abc"))
-  ]
+  let optPath co = mkOpt co
+                   executablePathOptSty
+                   (Just "ABC executable path")
+                   (Just (ConcreteString "abc"))
+      p = optPath abcPath
+  in [ p
+     , copyOpt (const $ configOptionText abcStrictParsing) strictSMTParseOpt
+     , deprecatedOpt [p] $ optPath abcPathOLD
+     ] <> SMT2.smtlib2Options

 externalABCAdapter :: SolverAdapter st
 externalABCAdapter =
@ -95,6 +107,7 @@ writeABCSMT2File
   -> [BoolExpr t]
   -> IO ()
 writeABCSMT2File = SMT2.writeDefaultSMT2 ExternalABC "ABC" abcFeatures
+                   (Just abcStrictParsing)

 instance SMT2.SMTLib2GenericSolver ExternalABC where
  defaultSolverPath _ = findSolverPath abcPath . getConfiguration
@ -114,3 +127,4 @@ runExternalABCInOverride
  -> IO a
 runExternalABCInOverride =
  SMT2.runSolverInOverride ExternalABC nullAcknowledgementAction abcFeatures
+  (Just abcStrictParsing)
--- a/what4/src/What4/Solver/STP.hs
+++ b/what4/src/What4/Solver/STP.hs
@ -25,26 +25,38 @@ module What4.Solver.STP
 import           Data.Bits

 import           What4.BaseTypes
-import           What4.Config
 import           What4.Concrete
-import           What4.Interface
-import           What4.ProblemFeatures
-import           What4.SatResult
+import           What4.Config
 import           What4.Expr.Builder
 import           What4.Expr.GroundEval
-import           What4.Solver.Adapter
+import           What4.Interface
+import           What4.ProblemFeatures
 import           What4.Protocol.Online
 import qualified What4.Protocol.SMTLib2 as SMT2
+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
+import           What4.SatResult
+import           What4.Solver.Adapter
 import           What4.Utils.Process

 data STP = STP deriving Show

 -- | Path to stp
 stpPath :: ConfigOption (BaseStringType Unicode)
-stpPath = configOption knownRepr "stp_path"
+stpPath = configOption knownRepr "solver.stp.path"
+
+stpPathOLD :: ConfigOption (BaseStringType Unicode)
+stpPathOLD = configOption knownRepr "stp_path"

 stpRandomSeed :: ConfigOption BaseIntegerType
-stpRandomSeed = configOption knownRepr "stp.random-seed"
+stpRandomSeed = configOption knownRepr "solver.stp.random-seed"
+
+stpRandomSeedOLD :: ConfigOption BaseIntegerType
+stpRandomSeedOLD = configOption knownRepr "stp.random-seed"
+
+-- | Control strict parsing for Boolector solver responses (defaults
+-- to solver.strict-parsing option setting).
+stpStrictParsing :: ConfigOption BaseBoolType
+stpStrictParsing = configOption knownRepr "solver.stp.strict_parsing"

 intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc
 intWithRangeOpt nm lo hi = mkOpt nm sty Nothing Nothing
@ -52,12 +64,19 @@ intWithRangeOpt nm lo hi = mkOpt nm sty Nothing Nothing

 stpOptions :: [ConfigDesc]
 stpOptions =
-  [ mkOpt stpPath
-          executablePathOptSty
-          (Just "Path to STP executable.")
-          (Just (ConcreteString "stp"))
-  , intWithRangeOpt stpRandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1)
-  ]
+  let mkPath co = mkOpt co
+                  executablePathOptSty
+                  (Just "Path to STP executable.")
+                  (Just (ConcreteString "stp"))
+      p1 = mkPath stpPath
+      randbitval = 2^(30 :: Int)-1
+      r1 = intWithRangeOpt stpRandomSeed (negate randbitval) randbitval
+  in [ p1, r1
+     , copyOpt (const $ configOptionText stpStrictParsing) strictSMTParseOpt
+     , deprecatedOpt [p1] $ mkPath stpPathOLD
+     , deprecatedOpt [r1] $ intWithRangeOpt stpRandomSeedOLD
+       (negate randbitval) randbitval
+     ] <> SMT2.smtlib2Options

 stpAdapter :: SolverAdapter st
 stpAdapter =
@ -67,6 +86,7 @@ stpAdapter =
  , solver_adapter_check_sat  = runSTPInOverride
  , solver_adapter_write_smt2 =
       SMT2.writeDefaultSMT2 STP "STP" defaultWriteSMTLIB2Features
+       (Just stpStrictParsing)
  }

 instance SMT2.SMTLib2Tweaks STP where
@ -83,9 +103,6 @@ instance SMT2.SMTLib2GenericSolver STP where
    SMT2.setProduceModels writer True
    SMT2.setLogic writer SMT2.qf_bv

-  newDefaultWriter solver ack feats sym h in_h =
-    SMT2.newWriter solver h in_h ack (show solver) True feats False
-      =<< getSymbolVarBimap sym

 stpFeatures :: ProblemFeatures
 stpFeatures = useIntegerArithmetic .|. useBitvectors
@ -96,7 +113,8 @@ runSTPInOverride
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
-runSTPInOverride = SMT2.runSolverInOverride STP SMT2.nullAcknowledgementAction (SMT2.defaultFeatures STP)
+runSTPInOverride = SMT2.runSolverInOverride STP SMT2.nullAcknowledgementAction
+                   (SMT2.defaultFeatures STP) (Just stpStrictParsing)

 -- | Run STP in a session. STP will be configured to produce models, buth
 -- otherwise left with the default configuration.
@ -108,7 +126,8 @@ withSTP
  -> (SMT2.Session t STP -> IO a)
    -- ^ Action to run
  -> IO a
-withSTP = SMT2.withSolver STP SMT2.nullAcknowledgementAction (SMT2.defaultFeatures STP)
+withSTP = SMT2.withSolver STP SMT2.nullAcknowledgementAction
+          (SMT2.defaultFeatures STP) (Just stpStrictParsing)

 setInteractiveLogicAndOptions ::
  SMT2.SMTLib2Tweaks a =>
@ -125,5 +144,7 @@ setInteractiveLogicAndOptions writer = do
 --    SMT2.setOption writer "global-declarations" "true"

 instance OnlineSolver (SMT2.Writer STP) where
-  startSolverProcess = SMT2.startSolver STP SMT2.smtAckResult setInteractiveLogicAndOptions
+  startSolverProcess feat = SMT2.startSolver STP SMT2.smtAckResult
+                            setInteractiveLogicAndOptions feat
+                            (Just stpStrictParsing)
  shutdownSolverProcess = SMT2.shutdownSolver STP
--- a/what4/src/What4/Solver/Yices.hs
+++ b/what4/src/What4/Solver/Yices.hs
@ -64,7 +64,7 @@ module What4.Solver.Yices
  ) where

 #if !MIN_VERSION_base(4,13,0)
-import Control.Monad.Fail( MonadFail )
+import           Control.Monad.Fail ( MonadFail )
 #endif

 import           Control.Applicative
@ -102,25 +102,26 @@ import qualified System.IO.Streams.Attoparsec.Text as Streams
 import qualified Prettyprinter as PP

 import           What4.BaseTypes
-import           What4.Config
-import           What4.Solver.Adapter
 import           What4.Concrete
-import           What4.Interface
-import           What4.ProblemFeatures
-import           What4.SatResult
+import           What4.Config
 import qualified What4.Expr.Builder as B
 import           What4.Expr.GroundEval
 import           What4.Expr.VarIdentification
-import           What4.Protocol.SExp
-import           What4.Protocol.SMTLib2 (writeDefaultSMT2)
-import           What4.Protocol.SMTWriter as SMTWriter
+import           What4.Interface
+import           What4.ProblemFeatures
 import           What4.Protocol.Online
 import qualified What4.Protocol.PolyRoot as Root
+import           What4.Protocol.SExp
+import           What4.Protocol.SMTLib2 (writeDefaultSMT2)
+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
+import           What4.Protocol.SMTWriter as SMTWriter
+import           What4.SatResult
+import           What4.Solver.Adapter
 import           What4.Utils.HandleReader
 import           What4.Utils.Process

-import Prelude
-import GHC.Stack
+import           Prelude
+import           GHC.Stack

 -- | This is a tag used to indicate that a 'WriterConn' is a connection
 -- to a specific Yices process.
@ -451,7 +452,7 @@ newConnection stream in_stream ack reqFeatures timeout bindings = do
                     , yicesTimeout = timeout
                     , yicesUnitDeclared = unitRef
                     }
-  conn <- newWriterConn stream in_stream (ack earlyUnsatRef) nm features' bindings c
+  conn <- newWriterConn stream in_stream (ack earlyUnsatRef) nm Strict features' bindings c
  return $! conn { supportFunctionDefs = True
                 , supportFunctionArguments = True
                 , supportQuantifiers = efSolver
@ -561,7 +562,7 @@ instance SMTReadWriter Connection where
  smtSatResult _ = getSatResponse

  smtUnsatAssumptionsResult _ s =
-    do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) s)
+    do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) (connInputHandle s))
       let cmd = safeCmd "(show-unsat-assumptions)"
       case mb of
         Right (asNegAtomList -> Just as) -> return as
@ -573,7 +574,7 @@ instance SMTReadWriter Connection where
                         ]

  smtUnsatCoreResult _ s =
-    do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) s)
+    do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) (connInputHandle s))
       let cmd = safeCmd "(show-unsat-core)"
       case mb of
         Right (asAtomList -> Just nms) -> return nms
@ -693,10 +694,8 @@ yicesStartSolver features auxOutput sym = do -- FIXME

  return $! SolverProcess { solverConn   = conn
                          , solverCleanupCallback = cleanupProcess hdls
-                          , solverStdin  = in_stream'
                          , solverStderr = err_reader
                          , solverHandle = ph
-                          , solverResponse = out_stream
                          , solverErrorBehavior = ContinueOnError
                          , solverEvalFuns = smtEvalFuns conn out_stream
                          , solverLogFn = logSolverEvent sym
@ -764,9 +763,9 @@ getAckResponse resps =

 -- | Get the sat result from a previous SAT command.
 -- Throws an exception if something goes wrong.
-getSatResponse :: Streams.InputStream Text -> IO (SatResult () ())
-getSatResponse resps =
-  do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) resps)
+getSatResponse :: WriterConn t Connection -> IO (SatResult () ())
+getSatResponse conn =
+  do mb <- tryJust filterAsync (Streams.parseFromStream (parseSExp parseYicesString) (connInputHandle conn))
     case mb of
       Right (SAtom "unsat")   -> return (Unsat ())
       Right (SAtom "sat")     -> return (Sat ())
@ -905,49 +904,72 @@ yicesAdapter =
       runYicesInOverride sym logData ps
          (cont . runIdentity . traverseSatResult (\x -> pure (x,Nothing)) pure)
   , solver_adapter_write_smt2 =
-       writeDefaultSMT2 () "YICES" yicesSMT2Features
+       writeDefaultSMT2 () "YICES" yicesSMT2Features (Just yicesStrictParsing)
   }

 -- | Path to yices
 yicesPath :: ConfigOption (BaseStringType Unicode)
-yicesPath = configOption knownRepr "yices_path"
+yicesPath = configOption knownRepr "solver.yices.path"
+
+yicesPathOLD :: ConfigOption (BaseStringType Unicode)
+yicesPathOLD = configOption knownRepr "yices_path"

 -- | Enable the MC-SAT solver
 yicesEnableMCSat :: ConfigOption BaseBoolType
-yicesEnableMCSat = configOption knownRepr "yices_enable-mcsat"
+yicesEnableMCSat = configOption knownRepr "solver.yices.enable-mcsat"
+
+yicesEnableMCSatOLD :: ConfigOption BaseBoolType
+yicesEnableMCSatOLD = configOption knownRepr "yices_enable-mcsat"

 -- | Enable interactive mode (necessary for per-goal timeouts)
 yicesEnableInteractive :: ConfigOption BaseBoolType
-yicesEnableInteractive = configOption knownRepr "yices_enable-interactive"
+yicesEnableInteractive = configOption knownRepr "solver.yices.enable-interactive"
+
+yicesEnableInteractiveOLD :: ConfigOption BaseBoolType
+yicesEnableInteractiveOLD = configOption knownRepr "yices_enable-interactive"

 -- | Set a per-goal timeout in seconds.
 yicesGoalTimeout :: ConfigOption BaseIntegerType
-yicesGoalTimeout = configOption knownRepr "yices_goal-timeout"
+yicesGoalTimeout = configOption knownRepr "solver.yices.goal-timeout"
+
+yicesGoalTimeoutOLD :: ConfigOption BaseIntegerType
+yicesGoalTimeoutOLD = configOption knownRepr "yices_goal-timeout"
+
+-- | Control strict parsing for Yices solver responses (defaults
+-- to solver.strict-parsing option setting).
+yicesStrictParsing :: ConfigOption BaseBoolType
+yicesStrictParsing = configOption knownRepr "solver.yices.strict_parsing"

 yicesOptions :: [ConfigDesc]
 yicesOptions =
-  [ mkOpt
-      yicesPath
-      executablePathOptSty
-      (Just "Yices executable path")
-      (Just (ConcreteString "yices"))
-  , mkOpt
-      yicesEnableMCSat
-      boolOptSty
-      (Just "Enable the Yices MCSAT solving engine")
-      (Just (ConcreteBool False))
-  , mkOpt
-      yicesEnableInteractive
-      boolOptSty
-      (Just "Enable Yices interactive mode (needed to support timeouts)")
-      (Just (ConcreteBool False))
-  , mkOpt
-      yicesGoalTimeout
-      integerOptSty
-      (Just "Set a per-goal timeout")
-      (Just (ConcreteInteger 0))
-  ]
-  ++ yicesInternalOptions
+  let mkPath co = mkOpt co
+                  executablePathOptSty
+                  (Just "Yices executable path")
+                  (Just (ConcreteString "yices"))
+      mkMCSat co = mkOpt co
+                   boolOptSty
+                   (Just "Enable the Yices MCSAT solving engine")
+                   (Just (ConcreteBool False))
+      mkIntr co = mkOpt co
+                  boolOptSty
+                  (Just "Enable Yices interactive mode (needed to support timeouts)")
+                  (Just (ConcreteBool False))
+      mkTmout co = mkOpt co
+                   integerOptSty
+                   (Just "Set a per-goal timeout")
+                   (Just (ConcreteInteger 0))
+      p = mkPath yicesPath
+      m = mkMCSat yicesEnableMCSat
+      i = mkIntr yicesEnableInteractive
+      t = mkTmout yicesGoalTimeout
+  in [ p, m, i, t
+     , copyOpt (const $ configOptionText yicesStrictParsing) strictSMTParseOpt
+     , deprecatedOpt [p] $ mkPath yicesPathOLD
+     , deprecatedOpt [m] $ mkMCSat yicesEnableMCSatOLD
+     , deprecatedOpt [i] $ mkIntr yicesEnableInteractiveOLD
+     , deprecatedOpt [t] $ mkTmout yicesGoalTimeoutOLD
+     ]
+     ++ yicesInternalOptions

 yicesBranchingChoices :: Set Text
 yicesBranchingChoices = Set.fromList
@ -967,8 +989,12 @@ yicesEFGenModes = Set.fromList
  , "projection"
  ]

-booleanOpt :: String -> ConfigDesc
-booleanOpt nm = booleanOpt' (configOption BaseBoolRepr ("yices."++nm))
+booleanOpt :: String -> [ConfigDesc]
+booleanOpt nm =
+  let b = booleanOpt' (configOption BaseBoolRepr ("solver.yices."++nm))
+  in [ b
+     , deprecatedOpt [b] $ booleanOpt' (configOption BaseBoolRepr ("yices."++nm))
+     ]

 booleanOpt' :: ConfigOption BaseBoolType -> ConfigDesc
 booleanOpt' o =
@ -977,36 +1003,52 @@ booleanOpt' o =
        Nothing
        Nothing

-floatWithRangeOpt :: String -> Rational -> Rational -> ConfigDesc
+floatWithRangeOpt :: String -> Rational -> Rational -> [ConfigDesc]
 floatWithRangeOpt nm lo hi =
-  mkOpt (configOption BaseRealRepr $ "yices."++nm)
-        (realWithRangeOptSty (Inclusive lo) (Inclusive hi))
-        Nothing
-        Nothing
+  let mkO n = mkOpt (configOption BaseRealRepr $ n++nm)
+              (realWithRangeOptSty (Inclusive lo) (Inclusive hi))
+              Nothing
+              Nothing
+      f = mkO "solver.yices."
+  in [ f
+     , deprecatedOpt [f] $ mkO "yices."
+     ]

-floatWithMinOpt :: String -> Bound Rational -> ConfigDesc
+floatWithMinOpt :: String -> Bound Rational -> [ConfigDesc]
 floatWithMinOpt nm lo =
-  mkOpt (configOption BaseRealRepr $ "yices."++nm)
-        (realWithMinOptSty lo)
-        Nothing
-        Nothing
+  let mkO n = mkOpt (configOption BaseRealRepr $ n++nm)
+              (realWithMinOptSty lo)
+              Nothing
+              Nothing
+      f = mkO "solver.yices."
+  in [ f
+     , deprecatedOpt [f] $ mkO "yices."
+     ]

-intWithRangeOpt :: String -> Integer -> Integer -> ConfigDesc
+intWithRangeOpt :: String -> Integer -> Integer -> [ConfigDesc]
 intWithRangeOpt nm lo hi =
-  mkOpt (configOption BaseIntegerRepr $ "yices."++nm)
-        (integerWithRangeOptSty (Inclusive lo) (Inclusive hi))
-        Nothing
-        Nothing
+  let mkO n = mkOpt (configOption BaseIntegerRepr $ n++nm)
+              (integerWithRangeOptSty (Inclusive lo) (Inclusive hi))
+              Nothing
+              Nothing
+      i = mkO "solver.yices."
+  in [ i
+     , deprecatedOpt [i] $ mkO "yices."
+     ]

-enumOpt :: String -> Set Text -> ConfigDesc
+enumOpt :: String -> Set Text -> [ConfigDesc]
 enumOpt nm xs =
-  mkOpt (configOption (BaseStringRepr UnicodeRepr) $ "yices."++nm)
-        (enumOptSty xs)
-        Nothing
-        Nothing
+  let mkO n = mkOpt (configOption (BaseStringRepr UnicodeRepr) $ n++nm)
+              (enumOptSty xs)
+              Nothing
+              Nothing
+      e = mkO "solver.yices."
+  in [ e
+     , deprecatedOpt [e] $ mkO "yices."
+     ]

 yicesInternalOptions :: [ConfigDesc]
-yicesInternalOptions =
+yicesInternalOptions = concat
  [ booleanOpt "var-elim"
  , booleanOpt "arith-elim"
  , booleanOpt "flatten"
@ -1155,8 +1197,6 @@ runYicesInOverride sym logData conditions resultFn = do
      let yp = SolverProcess { solverConn = c
                             , solverCleanupCallback = cleanupProcess hdls
                             , solverHandle = ph
-                             , solverStdin  = in_stream
-                             , solverResponse = out_stream
                             , solverErrorBehavior = ImmediateExit
                             , solverStderr = err_reader
                             , solverEvalFuns = smtEvalFuns c out_stream
--- a/what4/src/What4/Solver/Z3.hs
+++ b/what4/src/What4/Solver/Z3.hs
@ -41,6 +41,7 @@ import           What4.Interface
 import           What4.ProblemFeatures
 import           What4.Protocol.Online
 import qualified What4.Protocol.SMTLib2 as SMT2
+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )
 import qualified What4.Protocol.SMTLib2.Syntax as SMT2Syntax
 import           What4.Protocol.SMTWriter
 import           What4.SatResult
@ -51,25 +52,41 @@ data Z3 = Z3 deriving Show

 -- | Path to Z3
 z3Path :: ConfigOption (BaseStringType Unicode)
-z3Path = configOption knownRepr "z3_path"
+z3Path = configOption knownRepr "solver.z3.path"
+
+z3PathOLD :: ConfigOption (BaseStringType Unicode)
+z3PathOLD = configOption knownRepr "z3_path"

 -- | Per-check timeout, in milliseconds (zero is none)
 z3Timeout :: ConfigOption BaseIntegerType
-z3Timeout = configOption knownRepr "z3_timeout"
+z3Timeout = configOption knownRepr "solver.z3.timeout"
+
+z3TimeoutOLD :: ConfigOption BaseIntegerType
+z3TimeoutOLD = configOption knownRepr "z3_timeout"
+
+-- | Strict parsing specifically for Z3 interaction?  If set,
+-- overrides solver.strict_parsing, otherwise defaults to
+-- solver.strict_parsing.
+z3StrictParsing  :: ConfigOption BaseBoolType
+z3StrictParsing = configOption knownRepr "solver.z3.strict_parsing"

 z3Options :: [ConfigDesc]
 z3Options =
-  [ mkOpt
-      z3Path
-      executablePathOptSty
-      (Just "Z3 executable path")
-      (Just (ConcreteString "z3"))
-  , mkOpt
-      z3Timeout
-      integerOptSty
-      (Just "Per-check timeout in milliseconds (zero is none)")
-      (Just (ConcreteInteger 0))
-  ]
+  let mkPath co = mkOpt co
+                  executablePathOptSty
+                  (Just "Z3 executable path")
+                  (Just (ConcreteString "z3"))
+      mkTmo co = mkOpt co
+                 integerOptSty
+                 (Just "Per-check timeout in milliseconds (zero is none)")
+                 (Just (ConcreteInteger 0))
+      p = mkPath z3Path
+      t = mkTmo z3Timeout
+  in [ p, t
+     , copyOpt (const $ configOptionText z3StrictParsing) strictSMTParseOpt
+     , deprecatedOpt [p] $ mkPath z3PathOLD
+     , deprecatedOpt [t] $ mkTmo z3TimeoutOLD
+     ] <> SMT2.smtlib2Options

 z3Adapter :: SolverAdapter st
 z3Adapter =
@ -128,7 +145,7 @@ writeZ3SMT2File
   -> Handle
   -> [BoolExpr t]
   -> IO ()
-writeZ3SMT2File = SMT2.writeDefaultSMT2 Z3 "Z3" z3Features
+writeZ3SMT2File = SMT2.writeDefaultSMT2 Z3 "Z3" z3Features (Just z3StrictParsing)

 instance SMT2.SMTLib2GenericSolver Z3 where
  defaultSolverPath _ = findSolverPath z3Path . getConfiguration
@ -162,7 +179,8 @@ runZ3InOverride
  -> [BoolExpr t]
  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)
  -> IO a
-runZ3InOverride = SMT2.runSolverInOverride Z3 nullAcknowledgementAction z3Features
+runZ3InOverride = SMT2.runSolverInOverride Z3 nullAcknowledgementAction
+                  z3Features (Just z3StrictParsing)

 -- | Run Z3 in a session. Z3 will be configured to produce models, but
 -- otherwise left with the default configuration.
@ -174,7 +192,8 @@ withZ3
  -> (SMT2.Session t Z3 -> IO a)
    -- ^ Action to run
  -> IO a
-withZ3 = SMT2.withSolver Z3 nullAcknowledgementAction z3Features
+withZ3 = SMT2.withSolver Z3 nullAcknowledgementAction
+         z3Features (Just z3StrictParsing)


 setInteractiveLogicAndOptions ::
@ -196,7 +215,8 @@ setInteractiveLogicAndOptions writer = do

 instance OnlineSolver (SMT2.Writer Z3) where
  startSolverProcess feat mbIOh sym = do
-    sp <- SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions feat mbIOh sym
+    sp <- SMT2.startSolver Z3 SMT2.smtAckResult setInteractiveLogicAndOptions feat
+          (Just z3StrictParsing) mbIOh sym
    timeout <- SolverGoalTimeout <$>
               (getOpt =<< getOptionSetting z3Timeout (getConfiguration sym))
    return $ sp { solverGoalTimeout = timeout }
--- a/what4/test/AdapterTest.hs
+++ b/what4/test/AdapterTest.hs
@ -12,26 +12,31 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}

-import Control.Exception ( displayException, try, SomeException )
-import Control.Lens (folded)
-import Control.Monad ( forM, unless, void )
-import Control.Monad.Except ( runExceptT )
-import Data.BitVector.Sized ( mkBV )
-import Data.Char ( toLower )
-import System.Exit ( ExitCode(..) )
-import System.Process ( readProcessWithExitCode )
+import           Control.Exception ( displayException, try, SomeException(..), fromException )
+import           Control.Lens (folded)
+import           Control.Monad ( forM, unless, void )
+import           Control.Monad.Except ( runExceptT )
+import           Data.BitVector.Sized ( mkBV )
+import           Data.Char ( toLower )
+import qualified Data.List as L
+import           Data.Text ( pack )
+import           System.Exit ( ExitCode(..) )
+import           System.Process ( readProcessWithExitCode )

-import Test.Tasty
-import Test.Tasty.HUnit
+import           Test.Tasty
+import           Test.Tasty.HUnit

-import Data.Parameterized.Nonce
-import Data.Parameterized.Some
+import           Data.Parameterized.Nonce
+import           Data.Parameterized.Some

-import What4.Config
-import What4.Interface
-import What4.Expr
-import What4.Solver
-import What4.Protocol.VerilogWriter
+import qualified What4.BaseTypes as BT
+import           What4.Config
+import           What4.Expr
+import           What4.Interface
+import           What4.Protocol.SMTLib2.Response ( strictSMTParsing )
+import           What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) )
+import           What4.Protocol.VerilogWriter
+import           What4.Solver

 data State t = State

@ -69,6 +74,459 @@ mkSmokeTest adpt = testCase (solver_adapter_name adpt) $
        Nothing -> return ()
        Just ex -> fail $ displayException ex

+
+----------------------------------------------------------------------
+
+mkConfigTests :: [SolverAdapter State] -> [TestTree]
+mkConfigTests adapters =
+  [
+    testGroup "deprecated configs" (deprecatedConfigTests adapters)
+  , testGroup "strict parsing config" (strictParseConfigTests adapters)
+  ]
+  where
+    wantOptSetFailure withText res = case res of
+      Right r ->
+        assertFailure ("Expected '" <> withText <>
+                       "' but completed successfully with: " <> show r)
+      Left err ->
+        case fromException err of
+          Just (e :: OptSetFailure) ->
+            withText `L.isInfixOf` (show e) @?
+            ("Expected '" <> withText <> "' exception error but got: " <>
+             show e)
+          _ -> assertFailure $
+               "Expected OptSetFailure exception but got: " <> show err
+    wantOptGetFailure withText res = case res of
+      Right r ->
+        assertFailure ("Expected '" <> withText <>
+                       "' but completed successfully with: " <> show r)
+      Left err ->
+        case fromException err of
+          Just (e :: OptGetFailure) ->
+            withText `L.isInfixOf` (show e) @?
+            ("Expected '" <> withText <> "' exception error but got: " <>
+             show e)
+          _ -> assertFailure $
+               "Expected OptGetFailure exception but got: " <> show err
+    withAdapters :: [SolverAdapter State]
+                 -> (forall t . ExprBuilder t State (Flags FloatUninterpreted) -> IO a)
+                 -> IO a
+    withAdapters adptrs op = do
+        (cfgs, _getDefAdapter) <- solverAdapterOptions adptrs
+        withIONonceGenerator $ \gen ->
+          do sym <- newExprBuilder FloatUninterpretedRepr State gen
+             extendConfig cfgs (getConfiguration sym)
+             op sym
+
+    cmpUnderSomes :: Some OptionSetting -> Some OptionSetting -> IO ()
+    cmpUnderSomes (Some setterX) (Some setterY) =
+      case testEquality
+           (configOptionType (optionSettingName setterX))
+           (BaseStringRepr UnicodeRepr) of
+        Just Refl ->
+          case testEquality
+               (configOptionType (optionSettingName setterY))
+               (BaseStringRepr UnicodeRepr) of
+            Just Refl -> do vX <- getMaybeOpt setterX
+                            vY <- getMaybeOpt setterY
+                            vX @=? vY
+            Nothing -> assertFailure "second some is not a unicode string"
+        Nothing -> assertFailure "first some is not a unicode string"
+
+    cmpUnderSomesI :: Some OptionSetting -> Some OptionSetting -> IO ()
+    cmpUnderSomesI (Some setterX) (Some setterY) =
+      case testEquality BaseIntegerRepr
+           (configOptionType (optionSettingName setterX)) of
+        Just Refl ->
+          case testEquality BaseIntegerRepr
+               (configOptionType (optionSettingName setterY)) of
+            Just Refl -> do vX <- getMaybeOpt setterX
+                            vY <- getMaybeOpt setterY
+                            vX @=? vY
+            Nothing -> assertFailure "second some is not an integer"
+        Nothing -> assertFailure "first some is not an integer"
+
+    cmpUnderSome :: Some OptionSetting
+                 -> OptionSetting (BaseStringType Unicode) -> IO ()
+    cmpUnderSome (Some setterX) setterY =
+      case testEquality
+           (configOptionType (optionSettingName setterX))
+           (BaseStringRepr UnicodeRepr) of
+        Just Refl -> do vX <- getMaybeOpt setterX
+                        vY <- getMaybeOpt setterY
+                        vX @=? vY
+        Nothing -> assertFailure "first some is not a unicode string"
+
+    cmpUnderSomeI :: Some OptionSetting
+                 -> OptionSetting BaseIntegerType -> IO ()
+    cmpUnderSomeI (Some setterX) setterY =
+      case testEquality BaseIntegerRepr
+           (configOptionType (optionSettingName setterX)) of
+        Just Refl -> do vX <- getMaybeOpt setterX
+                        vY <- getMaybeOpt setterY
+                        vX @=? vY
+        Nothing -> assertFailure "first some is not an integer"
+
+    cmpUnderSomeB :: Some OptionSetting
+                 -> OptionSetting BaseBoolType -> IO ()
+    cmpUnderSomeB (Some setterX) setterY =
+      case testEquality BaseBoolRepr
+           (configOptionType (optionSettingName setterX)) of
+        Just Refl -> do vX <- getMaybeOpt setterX
+                        vY <- getMaybeOpt setterY
+                        vX @=? vY
+        Nothing -> assertFailure "first some is not a boolean"
+
+    strictParseConfigTests adaptrs =
+      let mkPCTest adaptr =
+            testGroup (solver_adapter_name adaptr) $
+            let setCommonStrictness cfg v = do
+                  setter <- getOptionSetting strictSMTParsing cfg
+                  show <$> setOpt setter v >>= (@?= "[]")
+                setSpecificStrictness cfg v = do
+                  setter <- getOptionSettingFromText (pack cfgName) cfg
+                  show <$> setBoolOpt setter v >>= (@?= "[]")
+                cfgName = "solver." <> (toLower <$> (solver_adapter_name adaptr)) <> ".strict_parsing"
+            in [
+                 testCase "default val" $
+                 withAdapters adaptrs $ \sym -> do
+                   let cfg = getConfiguration sym
+                       strictOpt = Just $ configOption knownRepr cfgName
+                   parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Strict)
+
+               , testCase "common val" $
+                 withAdapters adaptrs $ \sym -> do
+                   let cfg = getConfiguration sym
+                       strictOpt = Just $ configOption knownRepr cfgName
+                   setCommonStrictness cfg False
+                   parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Lenient)
+
+               , testCase "strict val" $
+                 withAdapters adaptrs $ \sym -> do
+                   let cfg = getConfiguration sym
+                       strictOpt = Just $ configOption knownRepr cfgName
+                   setSpecificStrictness cfg False
+                   parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Lenient)
+
+               , testCase "strict overrides common val" $
+                 withAdapters adaptrs $ \sym -> do
+                   let cfg = getConfiguration sym
+                       strictOpt = Just $ configOption knownRepr cfgName
+                   setCommonStrictness cfg False
+                   setSpecificStrictness cfg True
+                   parserStrictness strictOpt strictSMTParsing cfg >>= (@?= Strict)
+
+              ]
+      in fmap mkPCTest adaptrs
+
+    deprecatedConfigTests adaptrs =
+      [
+
+        testCaseSteps "deprecated default_solver is equivalent to solver.default" $
+        -- n.b. requires at least 2 entries in the adaptrs list
+        \step -> withAdapters adaptrs $ \sym -> do
+          step "Get OptionSetters, regular and deprecated, Text and ConfigOption"
+          settera <- getOptionSettingFromText "solver.default"
+                     (getConfiguration sym)
+          setterb <- getOptionSettingFromText "default_solver"
+                     (getConfiguration sym)
+          settera' <- getOptionSetting defaultSolverAdapter
+                     (getConfiguration sym)
+          step "Get (same) initial value from regular and deprecated"
+          cmpUnderSomes settera setterb
+          step "Get (same) initial value from Text and ConfigOption identification"
+          cmpUnderSome settera settera'
+          v0 <- getMaybeOpt settera'
+
+          step "Update the value via deprecated"
+          res1 <- try $ setUnicodeOpt setterb $
+                  pack $ solver_adapter_name $ last adaptrs
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "DEPRECATED CONFIG OPTION USED: default_solver (renamed to: solver.default)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          -- Get (same) updated value from regular and deprecated
+          cmpUnderSomes settera setterb
+          v1 <- getMaybeOpt settera'
+          (v0 /= v1) @? ("Update from " <> show v0 <> " failed for " <>
+                         show (fmap solver_adapter_name adaptrs))
+
+          step "Update the value via regular (text identification)"
+          res2 <- try $ setUnicodeOpt settera $
+                  pack $ solver_adapter_name $ head adaptrs
+          case res2 of
+            Right warns -> fmap show warns @?= []
+            Left (SomeException e) -> assertFailure $ show e
+          v2 <- getMaybeOpt settera'
+          v0 @=? v2
+
+          step "Update the value via regular (ConfigOption identification)"
+          res3 <- try $ setOpt settera' $
+                  pack $ solver_adapter_name $ last $ take 2 adaptrs
+          case res3 of
+            Right warns -> fmap show warns @?= []
+            Left (SomeException e) -> assertFailure $ show e
+          v3 <- getMaybeOpt settera'
+          (v0 /= v3) @? ("Update from " <> show v0 <> " failed for " <>
+                         show (fmap solver_adapter_name adaptrs))
+
+          step "Attempt invalid update via deprecated"
+          wantOptSetFailure "invalid setting" =<<
+            try (setUnicodeOpt setterb "foo")
+          v4 <- getMaybeOpt settera'
+          v3 @=? v4
+
+          step "Reset to original value"
+          res4 <- try $ setOpt settera' $
+                  pack $ solver_adapter_name $ head adaptrs
+          case res4 of
+            Right warns -> fmap show warns @?= []
+            Left (SomeException e) -> assertFailure $ show e
+          v5 <- getMaybeOpt settera'
+          v0 @=? v5
+          cmpUnderSome settera settera'
+
+      , testCase "deprecated boolector_path is equivalent to solver.boolector.path" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "boolector_path"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting boolectorPath
+                     (getConfiguration sym)
+          cmpUnderSome settera setterb
+          res1 <- try $ setUnicodeOpt settera "/foo/bar"
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "Could not find: /foo/bar"
+              , "DEPRECATED CONFIG OPTION USED: boolector_path (renamed to: solver.boolector.path)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSome settera setterb
+
+      , testCase "deprecated cvc4_path is equivalent to solver.cvc4.path" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "cvc4_path"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting cvc4Path
+                     (getConfiguration sym)
+          cmpUnderSome settera setterb
+          res1 <- try $ setUnicodeOpt settera "/foo/bar"
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "Could not find: /foo/bar"
+              , "DEPRECATED CONFIG OPTION USED: cvc4_path (renamed to: solver.cvc4.path)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSome settera setterb
+
+      , testCase "deprecated cvc4_timeout is equivalent to solver.cvc4.timeout" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "cvc4_timeout"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting cvc4Timeout
+                     (getConfiguration sym)
+          cmpUnderSomeI settera setterb
+          res1 <- try $ setIntegerOpt settera 42
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "DEPRECATED CONFIG OPTION USED: cvc4_timeout (renamed to: solver.cvc4.timeout)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSomeI settera setterb
+
+      , testCase "deprecated stp.random-seed is equivalent to solver.stp.random-seed" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "cvc4.random-seed"
+                     (getConfiguration sym)
+          setterb <- getOptionSettingFromText "solver.cvc4.random-seed"
+                     (getConfiguration sym)
+          cmpUnderSomesI settera setterb
+          res1 <- try $ setIntegerOpt settera 99
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "DEPRECATED CONFIG OPTION USED: cvc4.random-seed (renamed to: solver.cvc4.random-seed)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSomesI settera setterb
+
+      , testCase "deprecated dreal_path is equivalent to solver.dreal.path" $
+        withAdapters adaptrs $ \sym -> do
+#ifdef TEST_DREAL
+          settera <- getOptionSettingFromText "dreal_path"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting drealPath
+                     (getConfiguration sym)
+          cmpUnderSome settera setterb
+          res1 <- try $ setUnicodeOpt settera "/foo/bar"
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "Could not find: /foo/bar"
+              , "DEPRECATED CONFIG OPTION USED: dreal_path (renamed to: solver.dreal.path)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSome settera setterb
+#else
+          settera <- try $ getOptionSettingFromText "dreal_path"
+                     (getConfiguration sym)
+          wantOptGetFailure "not found" settera
+#endif
+
+      , testCase "deprecated abc_path is equivalent to solver.abc.path" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "abc_path"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting abcPath
+                     (getConfiguration sym)
+          cmpUnderSome settera setterb
+          res1 <- try $ setUnicodeOpt settera "/foo/bar"
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "Could not find: /foo/bar"
+              , "DEPRECATED CONFIG OPTION USED: abc_path (renamed to: solver.abc.path)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSome settera setterb
+
+      , testCase "deprecated stp_path is equivalent to solver.stp.path" $
+        withAdapters adaptrs $ \sym -> do
+#ifdef TEST_STP
+          settera <- getOptionSettingFromText "stp_path"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting stpPath
+                     (getConfiguration sym)
+          cmpUnderSome settera setterb
+          res1 <- try $ setUnicodeOpt settera "/foo/bar"
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "Could not find: /foo/bar"
+              , "DEPRECATED CONFIG OPTION USED: stp_path (renamed to: solver.stp.path)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSome settera setterb
+#else
+          settera <- try $ getOptionSettingFromText "stp_path"
+                     (getConfiguration sym)
+          wantOptGetFailure "not found" settera
+#endif
+
+      , testCase "deprecated stp.random-seed is equivalent to solver.stp.random-seed" $
+        withAdapters adaptrs $ \sym -> do
+#ifdef TEST_STP
+          settera <- getOptionSettingFromText "stp.random-seed"
+                     (getConfiguration sym)
+          setterb <- getOptionSettingFromText "solver.stp.random-seed"
+                     (getConfiguration sym)
+          cmpUnderSomesI settera setterb
+          res1 <- try $ setIntegerOpt settera 99
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "DEPRECATED CONFIG OPTION USED: stp.random-seed (renamed to: solver.stp.random-seed)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSomesI settera setterb
+#else
+          settera <- try $ getOptionSettingFromText "stp.random-seed"
+                     (getConfiguration sym)
+          wantOptGetFailure "not found" settera
+#endif
+
+      , testCase "deprecated yices_path is equivalent to solver.yices.path" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "yices_path"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting yicesPath
+                     (getConfiguration sym)
+          cmpUnderSome settera setterb
+          res1 <- try $ setUnicodeOpt settera "/foo/bar"
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "Could not find: /foo/bar"
+              , "DEPRECATED CONFIG OPTION USED: yices_path (renamed to: solver.yices.path)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSome settera setterb
+
+      , testCase "deprecated yices_enable-interactive is equivalent to solver.yices.en.." $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "yices_enable-interactive"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting yicesEnableInteractive
+                     (getConfiguration sym)
+          cmpUnderSomeB settera setterb
+          res1 <- try $ setBoolOpt settera True
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "DEPRECATED CONFIG OPTION USED: yices_enable-interactive (renamed to: solver.yices.enable-interactive)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSomeB settera setterb
+
+      , testCase "deprecated yices_enable-mcsat is equivalent to solver.yices.enable-mcsat" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "yices_enable-mcsat"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting yicesEnableMCSat
+                     (getConfiguration sym)
+          cmpUnderSomeB settera setterb
+          res1 <- try $ setBoolOpt settera True
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "DEPRECATED CONFIG OPTION USED: yices_enable-mcsat (renamed to: solver.yices.enable-mcsat)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSomeB settera setterb
+
+      , testCase "deprecated yices_goal-timeout is equivalent to solver.yices.goal-timeout" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "yices_goal-timeout"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting yicesGoalTimeout
+                     (getConfiguration sym)
+          cmpUnderSomeI settera setterb
+          res1 <- try $ setIntegerOpt settera 123
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "DEPRECATED CONFIG OPTION USED: yices_goal-timeout (renamed to: solver.yices.goal-timeout)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSomeI settera setterb
+
+      , testCase "deprecated z3_path is equivalent to solver.z3.path" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "z3_path"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting z3Path
+                     (getConfiguration sym)
+          cmpUnderSome settera setterb
+          res1 <- try $ setUnicodeOpt settera "/bar/foo"
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "Could not find: /bar/foo"
+              , "DEPRECATED CONFIG OPTION USED: z3_path (renamed to: solver.z3.path)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSome settera setterb
+
+      , testCase "deprecated z3_timeout is equivalent to solver.z3.timeout" $
+        withAdapters adaptrs $ \sym -> do
+          settera <- getOptionSettingFromText "z3_timeout"
+                     (getConfiguration sym)
+          setterb <- getOptionSetting z3Timeout
+                     (getConfiguration sym)
+          cmpUnderSomeI settera setterb
+          res1 <- try $ setIntegerOpt settera 123
+          case res1 of
+            Right warns -> fmap show warns @?=
+              [ "DEPRECATED CONFIG OPTION USED: z3_timeout (renamed to: solver.z3.timeout)"
+              ]
+            Left (SomeException e) -> assertFailure $ show e
+          cmpUnderSomeI settera setterb
+
+      ]
+
+
+----------------------------------------------------------------------
+
 nonlinearRealTest :: SolverAdapter State -> TestTree
 nonlinearRealTest adpt = testCase (solver_adapter_name adpt) $
  withSym adpt $ \sym ->
@ -192,7 +650,12 @@ verilogTest = testCase "verilogTest" $ withIONonceGenerator $ \gen ->

 getSolverVersion :: String -> IO String
 getSolverVersion solver = do
-  try (readProcessWithExitCode (toLower <$> solver) ["--version"] "") >>= \case
+  let args = case toLower <$> solver of
+               -- n.b. abc will return a non-zero exit code if asked
+               -- for command usage.
+               "abc" -> ["s", "-q", "version;quit"]
+               _ -> ["--version"]
+  try (readProcessWithExitCode (toLower <$> solver) args "") >>= \case
    Right (r,o,e) ->
      if r == ExitSuccess
      then let ol = lines o in
@ -215,6 +678,7 @@ main = do
    localOption (mkTimeout (10 * 1000 * 1000)) $
    testGroup "AdapterTests"
    [ testGroup "SmokeTest" $ map mkSmokeTest allAdapters
+    , testGroup "Config Tests" $ mkConfigTests allAdapters
    , testGroup "QuickStart" $ map mkQuickstartTest allAdapters
    , testGroup "nonlinear reals" $ map nonlinearRealTest
      -- NB: nonlinear arith expected to fail for STP and Boolector
--- a/what4/test/ConfigTest.hs
+++ b/what4/test/ConfigTest.hs
@ -0,0 +1,599 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+import           Control.Exception ( displayException, try, SomeException(..), fromException )
+import qualified Data.List as L
+import           Data.Parameterized.Context ( pattern Empty, pattern (:>) )
+import           Data.Parameterized.Some
+import           Data.Ratio ( (%) )
+import qualified Data.Set as Set
+import qualified Data.Text as T
+import           Data.Void
+import qualified Prettyprinter as PP
+
+import           Test.Tasty
+import           Test.Tasty.Checklist
+import           Test.Tasty.HUnit
+
+import           What4.BaseTypes
+import           What4.Concrete
+import           What4.Config
+
+
+testSetAndGet :: [TestTree]
+testSetAndGet =
+  [
+    testCase "create multiple options" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr"
+          o2 = configOption BaseIntegerRepr "optint"
+          o3 = configOption BaseBoolRepr "optbool"
+          o1' = mkOpt o1 stringOptSty Nothing Nothing
+          o2' = mkOpt o2 integerOptSty Nothing Nothing
+          o3' = mkOpt o3 boolOptSty Nothing Nothing
+      extendConfig [o3', o2', o1'] cfg
+
+  , testCase "create conflicting options" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "mainopt"
+          o2 = configOption BaseIntegerRepr "mainopt"
+          o1' = mkOpt o1 stringOptSty Nothing Nothing
+          o2' = mkOpt o2 integerOptSty Nothing Nothing
+      res <- try $ extendConfig [o2', o1'] cfg
+      wantOptCreateFailure "already exists with type" res
+
+  , testCase "create conflicting options at different levels" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "mainopt"
+          o2 = configOption BaseIntegerRepr "main.mainopt"
+          o1' = mkOpt o1 stringOptSty Nothing Nothing
+          o2' = mkOpt o2 integerOptSty Nothing Nothing
+      res <- try @SomeException $ extendConfig [o2', o1'] cfg
+      case res of
+        Right () -> return ()
+        Left e -> assertFailure $ "Unexpected exception: " <> displayException e
+
+  , testCase "create duplicate unicode options" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "mainopt"
+          o2 = configOption (BaseStringRepr UnicodeRepr) "mainopt"
+          o1' = mkOpt o1 stringOptSty Nothing Nothing
+          o2' = mkOpt o2 stringOptSty Nothing Nothing
+      res <- try @SomeException $ extendConfig [o2', o1'] cfg
+      case res of
+        Right () -> return ()
+        Left e -> assertFailure $ "Unexpected exception: " <> displayException e
+
+  , testCaseSteps "get unset value, no default" $ \step -> do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr"
+          o2 = configOption BaseIntegerRepr "optint"
+          o3 = configOption BaseBoolRepr "optbool"
+          o1' = mkOpt o1 stringOptSty Nothing Nothing
+          o2' = mkOpt o2 integerOptSty Nothing Nothing
+          o3' = mkOpt o3 boolOptSty Nothing Nothing
+      extendConfig [o3', o2', o1'] cfg
+      access1 <- getOptionSetting o1 cfg
+      access2 <- getOptionSetting o2 cfg
+      access3 <- getOptionSetting o3 cfg
+
+      step "get unset string opt"
+      v1 <- getMaybeOpt access1
+      Nothing @=? v1
+      res1 <- try $ getOpt access1
+      wantOptGetFailure "not set" res1
+
+      step "get unset integer opt"
+      v2 <- getMaybeOpt access2
+      Nothing @=? v2
+      res2 <- try $ getOpt access2
+      wantOptGetFailure "not set" res2
+
+      step "get unset bool opt"
+      v3 <- getMaybeOpt access3
+      Nothing @=? v3
+      res3 <- try $ getOpt access3
+      wantOptGetFailure "not set" res3
+
+  , testCaseSteps "get unset value, with default" $ \step -> do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr"
+          o2 = configOption BaseIntegerRepr "optint"
+          o3 = configOption BaseBoolRepr "optbool"
+          o1' = mkOpt o1 stringOptSty Nothing (Just $ ConcreteString "strval")
+          o2' = mkOpt o2 integerOptSty Nothing (Just $ ConcreteInteger 11)
+          o3' = mkOpt o3 boolOptSty Nothing (Just $ ConcreteBool True)
+      extendConfig [o3', o2', o1'] cfg
+      access1 <- getOptionSetting o1 cfg
+      access2 <- getOptionSetting o2 cfg
+      access3 <- getOptionSetting o3 cfg
+      step "get unset default string opt"
+      v1 <- getMaybeOpt access1
+      Just "strval" @=? v1
+      step "get unset default integer opt"
+      v2 <- getMaybeOpt access2
+      Just 11 @=? v2
+      step "get unset default bool opt"
+      v3 <- getMaybeOpt access3
+      Just True @=? v3
+
+  , testCaseSteps "get set value, with default" $ \step -> do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr"
+          o2 = configOption BaseIntegerRepr "optint"
+          o3 = configOption BaseBoolRepr "optbool"
+          o1' = mkOpt o1 stringOptSty Nothing (Just $ ConcreteString "strval")
+          o2' = mkOpt o2 integerOptSty Nothing (Just $ ConcreteInteger 11)
+          o3' = mkOpt o3 boolOptSty Nothing (Just $ ConcreteBool True)
+      extendConfig [o3', o2', o1'] cfg
+      access1 <- getOptionSetting o1 cfg
+      access2 <- getOptionSetting o2 cfg
+      access3 <- getOptionSetting o3 cfg
+
+      step "set string opt"
+      res1 <- setOpt access1 "flibberty"
+      show <$> res1 @?= []
+
+      step "set bool opt"
+      res2 <- setOpt access3 False
+      show <$> res2 @?= []
+
+      step "set integer opt"
+      res3 <- setOpt access2 9945
+      show <$> res3 @?= []
+
+      step "get string opt"
+      v1 <- getMaybeOpt access1
+      Just "flibberty" @=? v1
+      step "get integer opt"
+      v2 <- getMaybeOpt access2
+      Just 9945 @=? v2
+      step "get bool opt"
+      v3 <- getMaybeOpt access3
+      Just False @=? v3
+
+  , testCaseSteps "set invalid values" $ \step -> do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr"
+          o2 = configOption BaseIntegerRepr "optint"
+          o3 = configOption BaseRealRepr "optbool"
+          -- n.b. the default values are not checked by the style!
+          o1' = mkOpt o1 (enumOptSty
+                          (Set.fromList ["eeny", "meeny", "miny", "mo" ]))
+                Nothing (Just $ ConcreteString "strval")
+          o2' = mkOpt o2 (integerWithRangeOptSty Unbounded (Inclusive 10))
+                Nothing (Just $ ConcreteInteger 11)
+          o3' = mkOpt o3 (realWithMinOptSty (Exclusive 1.23))
+                Nothing (Just $ ConcreteReal 0.0)
+      extendConfig [o3', o2', o1'] cfg
+      access1 <- getOptionSetting o1 cfg
+      access2 <- getOptionSetting o2 cfg
+      access3 <- getOptionSetting o3 cfg
+
+      step "initial defaults"
+      getMaybeOpt access1 >>= (@?= Just "strval")
+      getMaybeOpt access2 >>= (@?= Just 11)
+      getMaybeOpt access3 >>= (@?= Just (0 % 1 :: Rational))
+
+      step "set string opt invalidly"
+      -- Note: the strong typing prevents both of the following
+      -- setOpt access1 32
+      -- setOpt access1 False
+      res1 <- try $ setOpt access1 "frobozz"
+      wantOptSetFailure "invalid setting \"frobozz\"" res1
+      wantOptSetFailure "eeny, meeny, miny, mo" res1
+      (try @SomeException $ setOpt access1 "meeny") >>= \case
+        Right [] -> return ()
+        Right w -> assertFailure $ "Unexpected warnings: " <> show w
+        Left e -> assertFailure $ "Unexpected exception: " <> displayException e
+
+      step "set integer opt invalidly"
+      wantOptSetFailure "out of range" =<< (try $ setOpt access2 11)
+      wantOptSetFailure "expected integer value in (-∞, 10]" =<< (try $ setOpt access2 11)
+      (try @SomeException $ setOpt access2 10) >>= \case
+        Right [] -> return ()
+        Right w -> assertFailure $ "Unexpected warnings: " <> show w
+        Left e -> assertFailure $ "Unexpected exception: " <> displayException e
+      (try @SomeException $ setOpt access2 (-3)) >>= \case
+        Right [] -> return ()
+        Right w -> assertFailure $ "Unexpected warnings: " <> show w
+        Left e -> assertFailure $ "Unexpected exception: " <> displayException e
+
+      step "set real opt invalidly"
+      wantOptSetFailure "out of range" =<< (try $ setOpt access3 (0 % 3))
+      wantOptSetFailure "expected real value in (123 % 100, +∞)"
+        =<< (try $ setOpt access3 (0 % 3))
+      wantOptSetFailure "out of range" =<< (try $ setOpt access3 (1229 % 1000))
+      wantOptSetFailure "out of range" =<< (try $ setOpt access3 (123 % 100))
+      (try @SomeException $ setOpt access3 (123001 % 100000)) >>= \case
+        Right [] -> return ()
+        Right w -> assertFailure $ "Unexpected warnings: " <> show w
+        Left e -> assertFailure $ "Unexpected exception: " <> displayException e
+
+  , testCaseSteps "get and set option values by name" $ \step ->
+      withChecklist "multiple values" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "main.optstr"
+          o2 = configOption BaseIntegerRepr "main.set.cfg.optint"
+          o3 = configOption BaseBoolRepr "main.set.cfg.optbool"
+          o4 = configOption BaseIntegerRepr "alt.optint"
+          o1' = mkOpt o1 stringOptSty Nothing (Just $ ConcreteString "strval")
+          o2' = mkOpt o2 integerOptSty Nothing (Just $ ConcreteInteger 11)
+          o3' = mkOpt o3 boolOptSty Nothing (Just $ ConcreteBool True)
+          o4' = mkOpt o4 integerOptSty Nothing (Just $ ConcreteInteger 88)
+      extendConfig [o4', o3', o2', o1'] cfg
+      accessSome1 <- getOptionSettingFromText "main.optstr" cfg
+      accessSome2 <- getOptionSettingFromText "main.set.cfg.optint" cfg
+      accessSome3 <- getOptionSettingFromText "main.set.cfg.optbool" cfg
+      accessSome4 <- getOptionSettingFromText "alt.optint" cfg
+
+      access1 <- getOptionSetting o1 cfg
+      access2 <- getOptionSetting o2 cfg
+      access3 <- getOptionSetting o3 cfg
+      access4 <- getOptionSetting o4 cfg
+
+      step "getting with a Some OptionSetter requires type verification"
+      let cmpUnderSome :: Some OptionSetting -> T.Text -> IO ()
+          cmpUnderSome (Some getter) v =
+            case testEquality
+                 (configOptionType (optionSettingName getter))
+                 (BaseStringRepr UnicodeRepr) of
+              Just Refl -> do vt <- getMaybeOpt getter
+                              Just v @=? vt
+              Nothing -> assertFailure "invalid option type"
+      cmpUnderSome accessSome1 "strval"
+
+      step "setting using special setting functions"
+      let goodNoWarn f s v =
+            (try @SomeException $ f s v) >>= \case
+            Right [] -> return ()
+            Right w -> assertFailure $ "Unexpected warnings: " <> show w
+            Left e -> assertFailure $ "Unexpected exception: " <> displayException e
+      goodNoWarn setUnicodeOpt accessSome1 "wild carrots"
+      goodNoWarn setIntegerOpt accessSome2 31
+      goodNoWarn setIntegerOpt accessSome4 42
+      goodNoWarn setBoolOpt accessSome3 False
+
+      step "verify set values"
+      (Just "wild carrots" @=?) =<< getMaybeOpt access1
+      (Just 31 @=?) =<< getMaybeOpt access2
+      (Just False @=?) =<< getMaybeOpt access3
+      (Just 42 @=?) =<< getMaybeOpt access4
+
+      step "cannot set values with wrong types"
+      -- Note that using an OptionSetting allows compile-time
+      -- elimination, but using a (Some OptionSetting) requires
+      -- run-time type witnessing and validation
+      wantOptSetFailure "type is a BaseStringRepr"
+        =<< (try $ setIntegerOpt accessSome1 54)
+      wantOptSetFailure "but given an integer"
+        =<< (try $ setIntegerOpt accessSome1 54)
+
+      wantOptSetFailure "type is a BaseStringRepr"
+        =<< (try $ setBoolOpt accessSome1 True)
+      wantOptSetFailure "but given a boolean"
+        =<< (try $ setBoolOpt accessSome1 True)
+
+      wantOptSetFailure "type is a BaseIntegerRepr"
+        =<< (try $ setUnicodeOpt accessSome2 "fresh tomatoes")
+      wantOptSetFailure "but given a text string"
+        =<< (try $ setUnicodeOpt accessSome2 "fresh tomatoes")
+
+
+  , testCaseSteps "get multiple values at once" $ \step ->
+      withChecklist "multiple values" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "main.optstr"
+          o2 = configOption BaseIntegerRepr "main.set.cfg.optint"
+          o3 = configOption BaseBoolRepr "main.set.cfg.optbool"
+          o4 = configOption BaseIntegerRepr "alt.optint"
+          o1' = mkOpt o1 stringOptSty Nothing (Just $ ConcreteString "strval")
+          o2' = mkOpt o2 integerOptSty Nothing (Just $ ConcreteInteger 11)
+          o3' = mkOpt o3 boolOptSty Nothing (Just $ ConcreteBool True)
+          o4' = mkOpt o4 integerOptSty Nothing (Just $ ConcreteInteger 88)
+      extendConfig [o4', o3', o2', o1'] cfg
+      access1 <- getOptionSetting o1 cfg
+      access3 <- getOptionSetting o3 cfg
+      access4 <- getOptionSetting o4 cfg
+
+      step "set string opt"
+      res1 <- setOpt access1 "flibberty"
+      show <$> res1 @?= []
+
+      step "set bool opt"
+      res2 <- setOpt access3 False
+      show <$> res2 @?= []
+
+      step "set alt int opt"
+      res4 <- setOpt access4 789
+      show <$> res4 @?= []
+
+      step "get main config values"
+      res <- getConfigValues "main.set" cfg
+      let msg = show . PP.pretty <$> res
+      msg `checkValues`
+        (Empty
+        :> Val "num values" length 2
+        :> Val "bool" (any (L.isInfixOf "main.set.cfg.optbool = False")) True
+        :> Val "int" (any (L.isInfixOf "main.set.cfg.optint = 11")) True
+        )
+
+      step "get all config values"
+      resAll <- getConfigValues "" cfg
+      let msgAll = show . PP.pretty <$> resAll
+      msgAll `checkValues`
+        (Empty
+        :> Val "num values" length 5
+        :> Val "bool" (any (L.isInfixOf "main.set.cfg.optbool = False")) True
+        :> Val "int" (any (L.isInfixOf "main.set.cfg.optint = 11")) True
+        :> Val "alt int" (any (L.isInfixOf "alt.optint = 789")) True
+        :> Val "str" (any (L.isInfixOf "main.optstr = \"flibberty\"")) True
+        :> Val "verbosity" (any (L.isInfixOf "verbosity = 0")) True
+        )
+
+      step "get specific config value"
+      resOne <- getConfigValues "alt.optint" cfg
+      let msgOne = show . PP.pretty <$> resOne
+      msgOne `checkValues`
+        (Empty
+        :> Val "num values" length 1
+        :> Val "alt int" (any (L.isInfixOf "alt.optint = 789")) True
+        )
+
+      step "get unknown config value"
+      resNope <- getConfigValues "fargle.bargle" cfg
+      let msgNope = show . PP.pretty <$> resNope
+      msgNope `checkValues` (Empty :> Val "num values" length 0)
+
+
+  ]
+
+testDeprecated :: [TestTree]
+testDeprecated =
+  [
+    testCase "deprecation removal (case #1)" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "hello"
+          o1' = mkOpt o1 stringOptSty (Just "greeting") Nothing
+      extendConfig [deprecatedOpt [] o1'] cfg
+      setter <- getOptionSetting o1 cfg
+      res <- try $ setOpt setter "eh?"
+      case res of
+        Right warns ->
+          fmap show warns @?=
+          [ "DEPRECATED CONFIG OPTION WILL BE IGNORED: hello (no longer valid)"
+          ]
+        Left (SomeException e) -> assertFailure $ show e
+
+  , testCase "deprecation rename (case #2)" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "hi"
+          o2 = configOption (BaseStringRepr UnicodeRepr) "hello"
+          o1' = deprecatedOpt [o2'] $
+                mkOpt o1 stringOptSty (Just "greeting") Nothing
+          o2' = mkOpt o2 stringOptSty (Just "greeting") Nothing
+      extendConfig [o2', o1'] cfg
+      setter <- getOptionSetting o1 cfg
+      res <- try $ setOpt setter "eh?"
+      case res of
+        Right warns ->
+          fmap show warns @?=
+          [ "DEPRECATED CONFIG OPTION USED: hi (renamed to: hello)"
+          ]
+        Left (SomeException e) -> assertFailure $ show e
+
+  , testCase "deprecation rename (case #2), wrong order" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "yo"
+          o2 = configOption (BaseStringRepr UnicodeRepr) "hello"
+          o1' = deprecatedOpt [o2'] $
+                mkOpt o1 stringOptSty (Just "greeting") Nothing
+          o2' = mkOpt o2 stringOptSty (Just "greeting") Nothing
+      res <- try $ extendConfig [o1', o2'] cfg
+      wantOptCreateFailure
+        "replacement options must be inserted into Config \
+        \before this deprecated option"
+        res
+
+  , testCase "deprecation rename and re-typed (case #3)" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr"
+          o2 = configOption BaseIntegerRepr "optnum"
+          o1' = deprecatedOpt [o2'] $
+                mkOpt o1 stringOptSty (Just "some opt") Nothing
+          o2' = mkOpt o2 integerOptSty (Just "some other opt") Nothing
+      extendConfig [o2', o1'] cfg
+      setter <- getOptionSetting o1 cfg
+      res <- try $ setOpt setter "eh?"
+      case res of
+        Right warns ->
+          fmap show warns @?=
+          [ "DEPRECATED CONFIG OPTION USED: optstr::BaseStringRepr UnicodeRepr (changed to: \"optnum\"::BaseIntegerRepr); this value may be ignored"
+          ]
+        Left (SomeException e) -> assertFailure $ show e
+
+  , testCase "deprecation, multiple replacements (case #4)" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "url"
+          o2 = configOption (BaseStringRepr UnicodeRepr) "hostname"
+          o3 = configOption BaseIntegerRepr "port"
+          o1' = deprecatedOpt [o2', o3'] $
+                mkOpt o1 stringOptSty (Just "some opt") Nothing
+          o2' = mkOpt o2 stringOptSty (Just "some other opt") Nothing
+          o3' = mkOpt o3 integerOptSty (Just "some other opt") Nothing
+      extendConfig [o3', o2', o1'] cfg
+      setter <- getOptionSetting o1 cfg
+      res <- try $ setOpt setter "here?"
+      case res of
+        Right warns ->
+          fmap show warns @?=
+          [ "DEPRECATED CONFIG OPTION USED: url::BaseStringRepr UnicodeRepr (replaced by: \"hostname\"::BaseStringRepr UnicodeRepr, \"port\"::BaseIntegerRepr); this value may be ignored"
+          ]
+        Left (SomeException e) -> assertFailure $ show e
+
+  , testCase "deprecation, multiple + removed/split (case #4,(#1,#3))" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "url"
+          o2 = configOption (BaseStringRepr UnicodeRepr) "hostname"
+          o3 = configOption BaseIntegerRepr "port"
+          o4 = configOption (BaseStringRepr UnicodeRepr) "host"
+          o5 = configOption (BaseStringRepr UnicodeRepr) "domain"
+          o1' = deprecatedOpt [o2', o3'] $
+                mkOpt o1 stringOptSty (Just "some opt") Nothing
+          o2' = deprecatedOpt [o4', o5'] $
+                mkOpt o2 stringOptSty (Just "some other opt") Nothing
+          o3' = deprecatedOpt [] $
+                mkOpt o3 integerOptSty (Just "some other opt") Nothing
+          o4' = mkOpt o4 stringOptSty (Nothing) Nothing
+          o5' = mkOpt o5 stringOptSty (Just "some opt") (Just $ ConcreteString "cow.barn")
+      extendConfig [ o4', o5', o2', o3', o1' ] cfg
+      setter <- getOptionSetting o1 cfg
+      res <- try $ setOpt setter "here?"
+      case res of
+        Right warns ->
+          fmap show warns @?=
+          [ "DEPRECATED CONFIG OPTION USED: url::BaseStringRepr UnicodeRepr (replaced by: \"host\"::BaseStringRepr UnicodeRepr, \"domain\"::BaseStringRepr UnicodeRepr); this value may be ignored"
+          ]
+        Left (SomeException e) -> assertFailure $ show e
+
+  ]
+
+testHelp :: [TestTree]
+testHelp =
+  [
+    testCase "builtin-only config help" $
+    withChecklist "builtins" $ do
+      cfg <- initialConfig 0 []
+      help <- configHelp "" cfg
+      help `checkValues`
+        (Empty
+        :> Val "num" length 1
+        :> Val "verbosity" (L.isInfixOf "verbosity =" . show . head) True
+        )
+
+
+  , testCaseSteps "three item (1 deprecated) config help" $ \step ->
+      withChecklist "three items" $ do
+      cfg <- initialConfig 0 []
+      let o1 = configOption (BaseStringRepr UnicodeRepr) "optstr"
+          o2 = configOption BaseIntegerRepr "optnum"
+          o3 = configOption BaseIntegerRepr "foo.bar.baz.num"
+          o1' = mkOpt o1 stringOptSty (Just "some opt") Nothing
+          o2' = mkOpt o2 integerOptSty (Just "some other opt") Nothing
+          o3' = mkOpt o3 integerOptSty (Just "foo stuff") Nothing
+          helpIncludes txts = any (\h -> all (\t -> L.isInfixOf t (show h)) txts)
+      extendConfig [o2', deprecatedOpt [o2'] o1', o3'] cfg
+      setter2 <- getOptionSetting o2 cfg
+      setRes <- setOpt setter2 13
+      setRes `checkValues` (Empty :> Val "no warnings" null True)
+
+      step "all help"
+      help <- configHelp "" cfg
+      help `checkValues`
+        (Empty
+        :> Val "num" length 4
+        :> Val "verbosity" (helpIncludes ["verbosity ="]) True
+        :> Val "option 1" (helpIncludes ["optstr"
+                                        , "some opt"
+                                        , "DEPRECATED!"
+                                        , "Suggest"
+                                        , "to \"optnum\""
+                                        ]) True
+        :> Val "option 2" (helpIncludes ["optnum", "= 13", "some other opt"]) True
+        :> Val "option 3" (helpIncludes ["foo.bar.baz.num", "foo stuff"]) True
+        )
+
+      step "sub help"
+      subHelp <- configHelp "foo.bar" cfg
+      subHelp `checkValues`
+        (Empty
+        :> Val "num" length 1
+        :> Val "option 3" (helpIncludes ["foo.bar.baz.num", "foo stuff"]) True
+        )
+
+      step "specific help"
+      spec <- configHelp "optstr" cfg
+      spec `checkValues`
+        (Empty
+        :> Val "num" length 1
+        :> Val "spec name" (helpIncludes ["optstr"]) True
+        :> Val "spec opt help" (helpIncludes ["some opt"]) True
+        :> Val "spec opt help deprecated" (helpIncludes [ "DEPRECATED!"
+                                                        , "Suggest"
+                                                        , "to \"optnum\""
+                                                        ]) True
+        )
+
+      step "specific sub help"
+      subspec <- configHelp "foo.bar.baz.num" cfg
+      subspec `checkValues`
+        (Empty
+        :> Val "num" length 1
+        :> Val "option 3" (helpIncludes ["foo.bar.baz.num", "foo stuff"]) True
+        )
+
+  ]
+
+instance TestShow (PP.Doc Void) where testShow = show
+instance TestShow [PP.Doc Void] where testShow = testShowList
+instance TestShow [String] where testShow = testShowList
+
+wantOptCreateFailure :: Show a => String -> Either SomeException a -> IO ()
+wantOptCreateFailure withText res = case res of
+  Right r ->
+    assertFailure ("Expected '" <> withText <>
+                   "' but completed successfully with: " <> show r)
+  Left err ->
+    case fromException err of
+      Just (e :: OptCreateFailure) ->
+        withText `L.isInfixOf` (show e) @?
+        ("Expected '" <> withText <> "' exception error but got: " <>
+         displayException e)
+      _ -> assertFailure $
+           "Expected OptCreateFailure exception but got: " <>
+           displayException err
+
+wantOptSetFailure :: Show a => String -> Either SomeException a -> IO ()
+wantOptSetFailure withText res = case res of
+  Right r ->
+    assertFailure ("Expected '" <> withText <>
+                   "' but completed successfully with: " <> show r)
+  Left err ->
+    case fromException err of
+      Just (e :: OptSetFailure) ->
+        withText `L.isInfixOf` (show e) @?
+        ("Expected '" <> withText <> "' exception error but got: " <>
+         displayException e)
+      _ -> assertFailure $
+           "Expected OptSetFailure exception but got: " <>
+           displayException err
+
+wantOptGetFailure :: Show a => String -> Either SomeException a -> IO ()
+wantOptGetFailure withText res = case res of
+  Right r ->
+    assertFailure ("Expected '" <> withText <>
+                   "' but completed successfully with: " <> show r)
+  Left err ->
+    case fromException err of
+      Just (e :: OptGetFailure) ->
+        withText `L.isInfixOf` (show e) @?
+        ("Expected '" <> withText <> "' exception error but got: " <>
+         displayException e)
+      _ -> assertFailure $
+           "Expected OptGetFailure exception but got: " <>
+           displayException err
+
+
+main :: IO ()
+main = defaultMain $
+       testGroup "ConfigTests"
+       [ testGroup "Set and get" $ testSetAndGet
+       , testGroup "Deprecated Configs" $ testDeprecated
+       , testGroup "Config help" $ testHelp
+       ]
--- a/what4/test/ExprBuilderSMTLib2.hs
+++ b/what4/test/ExprBuilderSMTLib2.hs
@ -885,12 +885,12 @@ testSolverInfo = testGroup "solver info queries" $
  [ testCase "test get solver version" $ withOnlineZ3 $ \_ proc -> do
      let conn = solverConn proc
      getVersion conn
-      _ <- versionResult (solverResponse proc)
+      _ <- versionResult conn
      pure ()
  , testCase "test get solver name" $ withOnlineZ3 $ \_ proc -> do
      let conn = solverConn proc
      getName conn
-      nm <- nameResult (solverResponse proc)
+      nm <- nameResult conn
      nm @?= "Z3"
  ]

--- a/what4/test/OnlineSolverTest.hs
+++ b/what4/test/OnlineSolverTest.hs
@ -214,7 +214,12 @@ quickstartTestAlt (nm, AnOnlineSolver (Proxy :: Proxy s), features, opts) = test

 getSolverVersion :: String -> IO String
 getSolverVersion solver =
-  try (readProcessWithExitCode (toLower <$> solver) ["--version"] "") >>= \case
+  let args = case toLower <$> solver of
+               -- n.b. abc will return a non-zero exit code if asked
+               -- for command usage.
+               "abc" -> ["s", "-q", "version;quit"]
+               _ -> ["--version"]
+  in try (readProcessWithExitCode (toLower <$> solver) args "") >>= \case
    Right (r,o,e) ->
      if r == ExitSuccess
      then let ol = lines o in
--- a/what4/test/SolverParserTest.hs
+++ b/what4/test/SolverParserTest.hs
@ -0,0 +1,69 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+
+import           Control.Monad.Catch ( SomeException, try )
+import qualified Data.Text.IO as TIO
+import           Numeric.Natural
+import qualified System.IO.Streams as Streams
+
+import           Test.Tasty
+import           Test.Tasty.HUnit
+import           Test.Tasty.Ingredients
+import           Test.Tasty.Sugar
+
+import           What4.Expr.Builder ( emptySymbolVarBimap )
+import           What4.ProblemFeatures ( noFeatures )
+import           What4.Protocol.SMTLib2.Response ( SMTResponse, getLimitedSolverResponse )
+import qualified What4.Protocol.SMTLib2.Syntax as SMT2
+import           What4.Protocol.SMTWriter
+
+
+sugarCube :: CUBE
+sugarCube = mkCUBE { inputDir = "test/responses"
+                   , rootName = "*.rsp"
+                   , expectedSuffix = ".exp"
+                   , validParams = [ ("parsing", Just ["strict", "lenient"])
+                                   ]
+                   }
+
+ingredients :: [Ingredient]
+ingredients = includingOptions sugarOptions :
+              sugarIngredients [sugarCube] <>
+              defaultIngredients
+
+
+main :: IO ()
+main = do testSweets <- findSugar sugarCube
+          defaultMainWithIngredients ingredients .
+            testGroup "solver response tests" =<<
+            withSugarGroups testSweets testGroup mkTest
+
+mkTest :: Sweets -> Natural -> Expectation -> IO [TestTree]
+mkTest s n e = do
+  expect <- readFile $ expectedFile e
+  let strictness =
+        let strictVal pmtch =
+              if paramMatchVal "strict" pmtch
+              then Strict
+              else if paramMatchVal "lenient" pmtch
+                   then Lenient
+                   else error "Invalid strictness specification"
+        in maybe Strict strictVal $ lookup "parsing" $ expParamsMatch e
+  return
+    [
+      testCase (rootMatchName s <> " #" <> show n) $ do
+        inpStrm <- Streams.makeInputStream $ Just <$> TIO.readFile (rootFile s)
+        outStrm <- Streams.makeOutputStream $ \_ -> error "output not supported for test"
+        w <- newWriterConn
+             outStrm
+             inpStrm
+             (AckAction $ undefined)
+             "test-solver"
+             strictness
+             noFeatures
+             emptySymbolVarBimap
+             ()
+        actual <- try $ getLimitedSolverResponse "test resp" Just w (SMT2.Cmd "test cmd")
+        expect @=? show (actual :: Either SomeException SMTResponse)
+    ]
--- a/what4/test/responses/err-behav-continue.exp
+++ b/what4/test/responses/err-behav-continue.exp
@ -0,0 +1 @@
+Right (RspErrBehavior "continued-execution")
--- a/what4/test/responses/err-behav-continue.rsp
+++ b/what4/test/responses/err-behav-continue.rsp
@ -0,0 +1 @@
+(:error-behavior continued-execution)
--- a/what4/test/responses/err-behav-unrec.exp
+++ b/what4/test/responses/err-behav-unrec.exp
@ -0,0 +1,12 @@
+Left Could not parse solver response:
+  Solver response parsing failure.
+*** Exception: Unrecognized response from solver:
+  bad :error-behavior value
+in response to command:
+  (get-info :error-behavior)
+
+Attempting to parse input for test resp:
+Just "(:error-behavior freak-out)\n"
+
+in response to commands for test resp:
+test cmd
--- a/what4/test/responses/err-behav-unrec.rsp
+++ b/what4/test/responses/err-behav-unrec.rsp
@ -0,0 +1 @@
+(:error-behavior freak-out)
--- a/what4/test/responses/error_bad.exp
+++ b/what4/test/responses/error_bad.exp
@ -0,0 +1,4 @@
+Left Solver reported an error:
+  this is bad
+in response to command:
+  test cmd
--- a/what4/test/responses/error_bad.rsp
+++ b/what4/test/responses/error_bad.rsp
@ -0,0 +1 @@
+(error "this is bad")
--- a/what4/test/responses/minisat_verbose_success.exp
+++ b/what4/test/responses/minisat_verbose_success.exp
@ -0,0 +1 @@
+Right AckSuccess
--- a/what4/test/responses/minisat_verbose_success.rsp
+++ b/what4/test/responses/minisat_verbose_success.rsp
@ -0,0 +1,2 @@
+minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy.
+success
--- a/what4/test/responses/minisat_verbose_success.strict.exp
+++ b/what4/test/responses/minisat_verbose_success.strict.exp
@ -0,0 +1,8 @@
+Left Could not parse solver response:
+  Solver response parsing failure.
+*** Exception: Parse exception: Failed reading: empty
+Attempting to parse input for test resp:
+Just "minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy.\nsuccess\n"
+
+in response to commands for test resp:
+test cmd
--- a/what4/test/responses/name.exp
+++ b/what4/test/responses/name.exp
@ -0,0 +1 @@
+Right (RspName "fancy solver #12")
--- a/what4/test/responses/name.rsp
+++ b/what4/test/responses/name.rsp
@ -0,0 +1 @@
+(:name "fancy solver #12")
--- a/what4/test/responses/rsnunk-bad.exp
+++ b/what4/test/responses/rsnunk-bad.exp
@ -0,0 +1,12 @@
+Left Could not parse solver response:
+  Solver response parsing failure.
+*** Exception: Unrecognized response from solver:
+  bad :reason-unknown value
+in response to command:
+  reason?
+
+Attempting to parse input for test resp:
+Just "(:reason-unknown foo bar baz)\n"
+
+in response to commands for test resp:
+test cmd
--- a/what4/test/responses/rsnunk-bad.rsp
+++ b/what4/test/responses/rsnunk-bad.rsp
@ -0,0 +1 @@
+(:reason-unknown foo bar baz)
--- a/what4/test/responses/rsnunk-incomplete.exp
+++ b/what4/test/responses/rsnunk-incomplete.exp
@ -0,0 +1 @@
+Right RspRsnIncomplete
--- a/what4/test/responses/rsnunk-incomplete.rsp
+++ b/what4/test/responses/rsnunk-incomplete.rsp
@ -0,0 +1 @@
+(:reason-unknown incomplete)
--- a/what4/test/responses/rsnunk-memout.exp
+++ b/what4/test/responses/rsnunk-memout.exp
@ -0,0 +1 @@
+Right RspOutOfMemory
--- a/what4/test/responses/rsnunk-memout.rsp
+++ b/what4/test/responses/rsnunk-memout.rsp
@ -0,0 +1 @@
+(:reason-unknown memout)
--- a/what4/test/responses/rsnunk-sexp.exp
+++ b/what4/test/responses/rsnunk-sexp.exp
@ -0,0 +1 @@
+Right (RspUnkReason (SApp [SAtom "foo",SAtom "bar",SAtom "baz"]))
--- a/what4/test/responses/rsnunk-sexp.rsp
+++ b/what4/test/responses/rsnunk-sexp.rsp
@ -0,0 +1 @@
+(:reason-unknown (foo bar baz))
--- a/what4/test/responses/sat.exp
+++ b/what4/test/responses/sat.exp
@ -0,0 +1 @@
+Right AckSat
--- a/what4/test/responses/sat.rsp
+++ b/what4/test/responses/sat.rsp
@ -0,0 +1 @@
+sat
--- a/what4/test/responses/success.exp
+++ b/what4/test/responses/success.exp
@ -0,0 +1 @@
+Right AckSuccess
--- a/what4/test/responses/success.rsp
+++ b/what4/test/responses/success.rsp
@ -0,0 +1 @@
+success
--- a/what4/test/responses/unknown.exp
+++ b/what4/test/responses/unknown.exp
@ -0,0 +1 @@
+Right AckUnknown
--- a/what4/test/responses/unknown.rsp
+++ b/what4/test/responses/unknown.rsp
@ -0,0 +1 @@
+unknown
--- a/what4/test/responses/unsat.exp
+++ b/what4/test/responses/unsat.exp
@ -0,0 +1 @@
+Right AckUnsat
--- a/what4/test/responses/unsat.rsp
+++ b/what4/test/responses/unsat.rsp
@ -0,0 +1 @@
+unsat
--- a/what4/test/responses/unsupported.exp
+++ b/what4/test/responses/unsupported.exp
@ -0,0 +1,2 @@
+Left unsupported command:
+  test cmd
--- a/what4/test/responses/unsupported.rsp
+++ b/what4/test/responses/unsupported.rsp
@ -0,0 +1 @@
+unsupported
--- a/what4/test/responses/version.exp
+++ b/what4/test/responses/version.exp
@ -0,0 +1 @@
+Right (RspVersion "1.8")
--- a/what4/test/responses/version.rsp
+++ b/what4/test/responses/version.rsp
@ -0,0 +1 @@
+(:version "1.8")
--- a/what4/what4.cabal
+++ b/what4/what4.cabal
@ -177,6 +177,7 @@ library
    What4.Protocol.Online
    What4.Protocol.SMTLib2
    What4.Protocol.SMTLib2.Parse
+    What4.Protocol.SMTLib2.Response
    What4.Protocol.SMTLib2.Syntax
    What4.Protocol.SMTWriter
    What4.Protocol.ReadDecimal
@ -249,6 +250,16 @@ test-suite adapter-test
    text,
    versions

+test-suite config-test
+  import: bldflags, testdefs-hunit
+  type: exitcode-stdio-1.0
+  main-is: ConfigTest.hs
+  build-depends: containers
+               , parameterized-utils
+               , prettyprinter
+               , tasty-checklist >= 1.0 && < 1.1
+               , text
+
 test-suite online-solver-test
  import: bldflags, testdefs-hunit
  type: exitcode-stdio-1.0
@ -344,3 +355,15 @@ test-suite template_tests
  build-depends: bv-sized
               , libBF
               , transformers
+
+
+test-suite solver_parsing_tests
+  import: bldflags, testdefs-hunit
+  type: exitcode-stdio-1.0
+  main-is : SolverParserTest.hs
+  build-depends: contravariant
+               , exceptions
+               , io-streams
+               , lumberjack
+               , tasty-sugar >= 1.1 && < 1.2
+               , text
				`@ -0,0 +1 @@`
				`Right (RspErrBehavior "continued-execution")`
				`@ -0,0 +1 @@`
				`Right (RspUnkReason (SApp [SAtom "foo",SAtom "bar",SAtom "baz"]))`