Remove auto option

src/Options.hs

@@ -40,7 +40,6 @@ data Options = Options { inputFormat :: InputFormat
                        , optProperties :: PropertyOption
                        , optRefinementType :: RefinementOption
                        , optMinimizeRefinement :: Int
-                       , optSMTAuto :: Bool
                        , optInvariant :: Bool
                        , optOutput :: Maybe String
                        , outputFormat :: OutputFormat
@@ -56,7 +55,6 @@ startOptions = Options { inputFormat = InPP
                        , optProperties = PropDefault
                        , optRefinementType = RefDefault
                        , optMinimizeRefinement = 0
-                       , optSMTAuto = True
                        , optInvariant = False
                        , optOutput = Nothing
                        , outputFormat = OutDOT
@@ -143,10 +141,6 @@ options =
                 "METHOD")
         "Minimize size of refinement structure by method METHOD (1-4)"
 
-        , Option "" ["smt-disable-auto-config"]
-        (NoArg (\opt -> Right opt { optSMTAuto = False }))
-        "Disable automatic configuration of the SMT solver"
-
         , Option "v" ["verbose"]
         (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
         "Increase verbosity (may be specified more than once)"

src/Solver.hs

@@ -32,20 +32,17 @@ symConstraints vars exVars allVars constraint = do
         allSyms <- mapM forall allVars
         return $ constraint $ val $ M.fromList $ (vars `zip` syms) ++ (exVars `zip` exSyms) ++ (allVars `zip` allSyms)
 
-getSolverConfig :: Bool -> Bool -> SMTConfig
-getSolverConfig verbose auto =
-        let tweaks = if auto then [] else ["(set-option :auto_config false)"]
-        in  z3{ verbose=verbose, solverTweaks=tweaks }
+getSolverConfig :: Bool -> SMTConfig
+getSolverConfig verbose = z3{ verbose=verbose }
 
 checkSat :: (SatModel a, SymWord a, Show a, Show b) =>
         ConstraintProblem a b -> OptIO (Maybe b)
 checkSat (problemName, resultName, vars, exVars, allVars, constraint, interpretation) = do
         verbosePut 2 $ "Checking SAT of " ++ problemName
         verbosity <- opt optVerbosity
-        autoConf <- opt optSMTAuto
-        result <- liftIO (satWith (getSolverConfig (verbosity >= 4) autoConf)
+        result <- liftIO (satWith (getSolverConfig (verbosity >= 4))
                     (symConstraints vars exVars allVars constraint))
-        case rebuildModel vars (getModel result) of
+        case rebuildModel vars (getModelAssignment result) of
             Nothing -> do
                 verbosePut 2 "- unsat"
                 return Nothing