Merge remote-tracking branch 'origin/master' into 3813-map-update-hook-and-hook-refactoring

Author: jberthold

booster/tools/booster/Server.hs

@@ -145,13 +145,15 @@ main = do
             monadLogger <- askLoggerIO
 
             koreLogEntriesAsJsonSelector <-
-                case Map.lookup (Logger.LevelOther "SimplifyJson") logLevelToKoreLogEntryMap of
-                    Nothing -> do
-                        Logger.logWarnNS
-                            "proxy"
-                            "Could not find out which Kore log entries correspond to the SimplifyJson level"
-                        pure (const False)
-                    Just es -> pure (`elem` es)
+                if Logger.LevelOther "SimplifyJson" `elem` customLevels
+                    then case Map.lookup (Logger.LevelOther "SimplifyJson") logLevelToKoreLogEntryMap of
+                        Nothing -> do
+                            Logger.logWarnNS
+                                "proxy"
+                                "Could not find out which Kore log entries correspond to the SimplifyJson level"
+                            pure (const False)
+                        Just koreSimplificationLogEntries -> pure (`elem` koreSimplificationLogEntries)
+                    else pure (const False)
 
             liftIO $ void $ withBugReport (ExeName "kore-rpc-booster") BugReportOnError $ \_reportDirectory -> withMDLib llvmLibraryFile $ \mdl -> do
                 let coLogLevel = fromMaybe Log.Info $ toSeverity logLevel

dev-tools/kore-rpc-dev/Server.hs

@@ -157,13 +157,15 @@ main = do
         monadLogger <- askLoggerIO
 
         koreLogEntriesAsJsonSelector <-
-            case Map.lookup (Logger.LevelOther "SimplifyJson") logLevelToKoreLogEntryMap of
-                Nothing -> do
-                    Logger.logWarnNS
-                        "proxy"
-                        "Could not find out which Kore log entries correspond to the SimplifyJson level"
-                    pure (const False)
-                Just es -> pure (`elem` es)
+            if Logger.LevelOther "SimplifyJson" `elem` customLevels
+                then case Map.lookup (Logger.LevelOther "SimplifyJson") logLevelToKoreLogEntryMap of
+                    Nothing -> do
+                        Logger.logWarnNS
+                            "proxy"
+                            "Could not find out which Kore log entries correspond to the SimplifyJson level"
+                        pure (const False)
+                    Just koreSimplificationLogEntries -> pure (`elem` koreSimplificationLogEntries)
+                else pure (const False)
 
         let coLogLevel = fromMaybe Log.Info $ toSeverity logLevel
             koreLogOptions =

kore/src/Kore/Rewrite/SMT/Evaluator.hs

@@ -224,7 +224,7 @@ retryWithScaledTimeout q = do
     retryOnceWithScaledTimeout :: MonadSMT m => m a -> Integer -> m a
     retryOnceWithScaledTimeout action scale =
         -- reinit with scaled timeout to override the original timeout
-        SMT.localTimeOut (scaleTimeOut scale) $ SMT.reinit >> action
+        SMT.reinit >> SMT.localTimeOut (scaleTimeOut scale) action
 
     scaleTimeOut :: Integer -> SMT.TimeOut -> SMT.TimeOut
     scaleTimeOut _ (SMT.TimeOut Unlimited) = SMT.TimeOut Unlimited