Fixed the handling of OR in logical expressions, and added a testcase

checks/Check.hs

@@ -149,11 +149,19 @@ addBK mp mp2 g nid n = fmap ((,) $ followBK (map keepDefined joined')) n
       where
         g :: A.Expression -> And (Or BackgroundKnowledge)
         g (A.Dyadic _ op lhs rhs)
-          -- (A or B) and (C or D) = ((A or B) and C) or ((A or B) and D)
+          -- If one of the components of an AND is unrecognised, we still keep
-          -- = (A and C) or (B and C) or (A and D) or (B and D)
+          -- the other part:
           | op == A.And = g lhs `mappend` g rhs
--- TODO:
+          -- (A and B) or (C and D) = ((A and B) or C) and ((A and B) or D)
---          | op == A.Or = And $ map Or $ productN $ map (map deOr . deAnd) [g lhs, g rhs]
+          -- = (A or C) and (B or C) and (A or D) and (B or D)
+          --
+          -- If one component of an OR is unrecognised, we end up dropping both
+          -- halves because we can no longer count on that BK (given A OR B, where
+          -- we recognise A, since we can't tell if B is true, we actually have
+          -- no information about A even if the branch is taken).  We do know that
+          -- if the branch is not taken, A cannot be true, but that's dealt with
+          -- because a negated OR ends up as an AND, see above.
+          | op == A.Or = let f = deAnd . g in And $ map (\(x,y) -> x `mappend` y) $ product2 (f lhs, f rhs)
           | op == A.Eq = noAnd $ noOr $ Equal lhs rhs
           | op == A.LessEq = noAnd $ noOr $ LessThanOrEqual lhs rhs
           | op == A.MoreEq = noAnd $ noOr $ LessThanOrEqual rhs lhs

testcases/automatic/usage-check-8.occ.test

@@ -81,6 +81,21 @@ PROC m()
           read(c[j])
         TRUE
           write(c[j])
+%PASS Safe replicated parallel use with overlap #5
+  PAR
+    PAR i = 0 FOR 10
+      IF
+        (i = 5) OR (i >= 6)
+          write(c[i])
+        TRUE
+          read(c[i])
+    PAR j = 0 FOR 10
+      IF
+        (j >= 5) AND ((j = 5) OR (j = 6) OR (j > 6))
+          read(c[j])
+        TRUE
+          write(c[j])
+
 %FAIL Unsafe replicated parallel use with overlap #3
   PAR
     PAR i = 0 FOR 5