We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent ca79544 commit 5ede3d6Copy full SHA for 5ede3d6
booster/library/Booster/SMT/Interface.hs
@@ -357,7 +357,7 @@ checkPredicates ctxt givenPs givenSubst psToCheck
357
Just (Unknown, _) -> retry smtGiven sexprsToCheck transState
358
Just (_, Unknown) -> retry smtGiven sexprsToCheck transState
359
Just other -> throwSMT' $ "Unexpected result while checking a condition: " <> show other
360
- Nothing -> pure Nothing
+ Nothing -> pure Nothing -- inconsistent ground truth
361
retry :: [DeclareCommand] -> [SExpr] -> TranslationState -> SMT io (Maybe Bool)
362
retry smtGiven sexprsToCheck transState = do
363
opts <- SMT $ gets (.options)
0 commit comments