Correct typos and test description

runtimeverification · Aug 12, 2024 · 3f29753 · 3f29753
1 parent 67bf458
commit 3f29753
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 8 deletions.
diff --git 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,17 +469,16 @@ 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
             -- the constraints are unsatisfiable, which means that the patten is Bottom
             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
@@ -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).