From ca76acba35fefd694f7644a523a82907492c89fb Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Mon, 11 Sep 2023 12:43:49 +0200 Subject: [PATCH] Use (||) directly when enabling tracing (#3652) This PR fixes the case of an `ExecuteRequest` with logging parameters `{logSuccessfulRewrites = Just True, logSuccessfulSimplifications = Nothing}` not retuning any logs (except of terminal/cut-point case). --- kore/src/Kore/JsonRpc.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index efc1e0aeb7..a0ceb438fb 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -124,6 +124,8 @@ respond serverState moduleName runSMT = case verifyIn serializedModule state of Left err -> pure $ Left $ backendError CouldNotVerifyPattern err Right verifiedPattern -> do + let tracingEnabled = + fromMaybe False logSuccessfulRewrites || fromMaybe False logSuccessfulSimplifications traversalResult <- liftIO ( runSMT (Exec.metadataTools serializedModule) lemmas $ @@ -134,7 +136,7 @@ respond serverState moduleName runSMT = then EnableMovingAverage else DisableMovingAverage ) - (fromMaybe False $ liftA2 (||) logSuccessfulRewrites logSuccessfulSimplifications) + tracingEnabled serializedModule (toStopLabels cutPointRules terminalRules) verifiedPattern