Skip to content

Commit

Permalink
Correct comments
Browse files Browse the repository at this point in the history
  • Loading branch information
geo2a committed Aug 5, 2024
1 parent 10f6b18 commit 985fcbc
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion booster/library/Booster/JsonRpc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ respond stateVar request =

case evaluatedInitialPattern of
(Left ApplyEquations.SideConditionFalse{}, _) -> do
-- input pattern's constrains are Bottom, return Bottom
-- input pattern's constraints are Bottom, return Vacuous
stop <- liftIO $ getTime Monotonic
pure $
execResponse
Expand Down
4 changes: 2 additions & 2 deletions booster/library/Booster/Pattern/ApplyEquations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -479,15 +479,15 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
throw . SideConditionFalse . collapseAndBools $ pat.constraints
Left SMT.SMTSolverUnknown{} -> do
-- unlikely case of an Unknown response to a consistency check.
-- What to do here? continue for now to preserver the old behaviour.
-- continue to preserver the old behaviour.
withContext CtxConstraint . logWarn . Text.pack $
"Constraints consistency UNKNOWN: " <> show consistent
continue
Left other ->
-- fail hard on SMT error other than @SMT.SMTSolverUnknown@
liftIO $ Exception.throw other
Right True -> do
-- constrains are consistent, continue
-- constraints are consistent, continue
continue
where
continue = do
Expand Down

0 comments on commit 985fcbc

Please sign in to comment.