Only emit proxy branch-eliminating rewrite trace when asked (#3976)

Follow-up to #3974
runtimeverification · Jul 12, 2024 · d137af6 · d137af6
1 parent 95d7d59
commit d137af6
Showing 1 changed file with 13 additions and 10 deletions.
diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs
@@ -642,22 +642,25 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
                                 -- extract the rule-id information from the result we proceed with
                                 let onlyNext = head filteredNexts
                                     rewriteRuleId = fromMaybe "UNKNOWN" onlyNext.ruleId
-                                    proxyRewriteStepLog =
-                                        RPCLog.Rewrite
-                                            { result =
-                                                RPCLog.Success
-                                                    { rewrittenTerm = Nothing
-                                                    , substitution = Nothing
-                                                    , ruleId = rewriteRuleId
+                                    proxyRewriteStepLogs
+                                        | Just True <- logSettings.logSuccessfulRewrites =
+                                            Just . (: []) $
+                                                RPCLog.Rewrite
+                                                    { result =
+                                                        RPCLog.Success
+                                                            { rewrittenTerm = Nothing
+                                                            , substitution = Nothing
+                                                            , ruleId = rewriteRuleId
+                                                            }
+                                                    , origin = RPCLog.Proxy
                                                     }
-                                            , origin = RPCLog.Proxy
-                                            }
+                                        | otherwise = Nothing
                                 Booster.Log.withContext CtxProxy $
                                     Booster.Log.logMessage' ("Continuing after rewriting with rule " <> rewriteRuleId)
                                 pure $
                                     Left
                                         ( execStateToKoreJson onlyNext
-                                        , logsOnly <> filteredNextLogs <> [Just [proxyRewriteStepLog]]
+                                        , logsOnly <> filteredNextLogs <> [proxyRewriteStepLogs]
                                         )
                         -- otherwise falling through to _otherReason
                         CutPointRule