From 3f29753e9d97f04845a2085c7327cfd934793fa8 Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Mon, 12 Aug 2024 08:38:28 +0200
Subject: [PATCH] Correct typos and test description

---
 booster/library/Booster/Pattern/ApplyEquations.hs   | 8 +++-----
 booster/test/rpc-integration/test-vacuous/README.md | 4 +---
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
index 366670c4a39..e225ebb63f0 100644
--- a/booster/library/Booster/Pattern/ApplyEquations.hs
+++ b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -457,7 +457,6 @@ evaluatePattern ::
 evaluatePattern def mLlvmLibrary smtSolver cache pat =
     runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
 
--- version for internal nested evaluation
 -- version for internal nested evaluation
 evaluatePattern' ::
     LoggerMIO io =>
@@ -470,9 +469,8 @@ evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternCon
         withContext CtxConstraint $ do
             withContext CtxDetail . withTermContext (coerce $ collapseAndBools constraints) $ pure ()
             consistent <- SMT.isSat solver (Set.toList constraints)
-            withContext CtxConstraint $
-                logMessage $
-                    "Constraints consistency check returns: " <> show consistent
+            logMessage $
+                "Constraints consistency check returns: " <> show consistent
             pure consistent
     case consistent of
         SMT.IsUnsat -> do
@@ -480,7 +478,7 @@ evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternCon
             throw . SideConditionFalse . collapseAndBools $ constraints
         SMT.IsUnknown{} -> do
             -- unlikely case of an Unknown response to a consistency check.
-            -- continue to preserver the old behaviour.
+            -- continue to preserve the old behaviour.
             withContext CtxConstraint . logWarn . Text.pack $
                 "Constraints consistency UNKNOWN: " <> show consistent
             pure ()
diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md
index 9464e3a6de8..bd26765c7c7 100644
--- a/booster/test/rpc-integration/test-vacuous/README.md
+++ b/booster/test/rpc-integration/test-vacuous/README.md
@@ -45,9 +45,7 @@ Rules `init` and `AC` introduce constraints on this variable:
      ==Int 1  \and N =/=Int  1` (A contradiction in the initial constraints).
 
    _Expected:_
-   - Rewrite with `BD` (despite the contradiction)
-   - The rewrite is stuck with `<k>d</k><int>N</int> \and...(contradiction)`
-   - The result is simplified and discovered to be `vacuous` (with state `d`).
+   - The state is simplified and discovered to be `vacuous` (with state `b`).
 
 With `kore-rpc-dev`, some contradictions will be discovered before or while
 attempting to rewrite (at the time of writing, it returns `stuck`, though).