Add syntactic filtering of side conditions after simplification

Author: geo2a

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -886,9 +886,17 @@ applyEquation term rule = fmap (either Failure Success) $ runExceptT $ do
                     renderOneLineText $
                         "Known true side conditions (won't check):" <+> hsep (intersperse "," $ map pretty knownTrue)
 
+            -- unclear conditions may have been simplified and
+            -- could now be syntactically present in the path constraints, check again
+            -- FIXME: factor this filtering out into a function ans use above
             unclearConditions' <- catMaybes <$> mapM (checkConstraint ConditionFalse) toCheck
+            let (newKnownTrue, stillUnclear) = partition (`Set.member` knownPredicates) unclearConditions'
+            unless (null newKnownTrue) $
+                logMessage $
+                    renderOneLineText $
+                        "Known true side conditions (won't check):" <+> hsep (intersperse "," $ map pretty knownTrue)
 
-            case unclearConditions' of
+            case stillUnclear of
                 [] -> do
                     -- check ensured conditions, filter any
                     -- true ones, prune if any is false