Fix bug report: --smt-reset-interval (#2263)

runtimeverification · Nov 16, 2020 · b692823 · b692823
1 parent 626f230
commit b692823
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 9 deletions.
diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs
@@ -396,8 +396,8 @@ parserInfoModifiers =
 unparseKoreSearchOptions :: KoreSearchOptions -> [String]
 unparseKoreSearchOptions (KoreSearchOptions _ bound searchType) =
     [ "--search searchFile.kore"
-    , maybeLimit "" (\limit -> "--bound " <> show limit) bound
-    , "--searchType " <> show searchType
+    , maybeLimit "" (\limit -> unwords ["--bound", show limit]) bound
+    , unwords ["--searchType", show searchType]
     ]
 
 unparseKoreMergeOptions :: KoreMergeOptions -> [String]
@@ -416,9 +416,11 @@ unparseKoreProveOptions
     )
   =
     [ "--prove spec.kore"
-    , "--spec-module " <> unpack moduleName
-    , "--graph-search "
-        <> if graphSearch == DepthFirst then "depth-first" else "breadth-first"
+    , unwords ["--spec-module", unpack moduleName]
+    , unwords
+        [ "--graph-search"
+        , if graphSearch == DepthFirst then "depth-first" else "breadth-first"
+        ]
     , if bmc then "--bmc" else ""
     , maybe "" ("--save-proofs " <>) saveProofs
     ]
@@ -455,12 +457,12 @@ koreExecSh
             [ pure $ defaultDefinitionFilePath koreExecOptions
             , patternFileName $> "--pattern pgm.kore"
             , outputFileName $> "--output result.kore"
-            , pure $ "--module " <> unpack (getModuleName mainModuleName)
+            , pure $ unwords ["--module", unpack (getModuleName mainModuleName)]
             , (\limit -> unwords ["--breadth", show limit])
                 <$> maybeLimit Nothing Just breadthLimit
             , (\limit -> unwords ["--depth", show limit])
                 <$> maybeLimit Nothing Just depthLimit
-            , pure $ "--strategy " <> fst strategy
+            , pure $ unwords ["--strategy", fst strategy]
             , rtsStatistics $>
                 unwords ["--rts-statistics", defaultRtsStatisticsFilePath]
             ]

diff --git a/kore/src/Options/SMT.hs b/kore/src/Options/SMT.hs
@@ -121,10 +121,14 @@ unparseKoreSolverOptions
     catMaybes
         [ (\limit -> unwords ["--smt-timeout", show limit])
             <$> maybeLimit Nothing Just unwrappedTimeOut
-        , pure $ unwords ["--smt-reset-interval", show resetInterval]
+        , pure
+            $ unwords
+                [ "--smt-reset-interval"
+                , show . getResetInterval $ resetInterval
+                ]
         , unwrappedPrelude
             $> unwords ["--smt-prelude", defaultSmtPreludeFilePath]
-        , pure $ "--smt " <> fmap Char.toLower (show solver)
+        , pure $ unwords ["--smt", unparseSolver solver]
         ]
 
 -- | Available SMT solvers.
@@ -144,6 +148,10 @@ parseSolver =
     knownOptions = intercalate ", " (map fst options)
     options = [ (map Char.toLower $ show s, s) | s <- [minBound .. maxBound] ]
 
+unparseSolver :: Solver -> String
+unparseSolver Z3 = "z3"
+unparseSolver None = "none"
+
 readSum :: String -> [(String, value)] -> Options.ReadM (String, value)
 readSum longName options = do
     opt <- str