fix: fix failing test when multiple feasible branches are present

Change condition of redundant/impossible condition to to be triggered
only if the z3 check fails for all branches for all paths
Add test cases for multiple feasible branches

python_ta/checkers/condition_logic_checker.py

@@ -76,17 +76,19 @@ def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None:
         env = Z3Environment(node.frame().cfg.z3_vars, [])
         z3_condition = env.parse_constraint(condition_node)
 
-        for edge in (pred for pred in node_block.predecessors if pred.is_feasible):
-            if all(
-                self._check_unsat(z3.And(*constraints), z3.Not(z3_condition))
-                for constraints in edge.z3_constraints.values()
-            ):
-                self.add_message("redundant-condition", node=node)
-            if all(
-                self._check_unsat(z3.And(*constraints), z3_condition)
-                for constraints in edge.z3_constraints.values()
-            ):
-                self.add_message("impossible-condition", node=node)
+        if all(
+            self._check_unsat(z3.And(*constraints), z3.Not(z3_condition))
+            for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
+            for constraints in edge.z3_constraints.values()
+        ):
+            self.add_message("redundant-condition", node=node)
+
+        if all(
+            self._check_unsat(z3.And(*constraints), z3_condition)
+            for edge in (pred for pred in node_block.predecessors if pred.is_feasible)
+            for constraints in edge.z3_constraints.values()
+        ):
+            self.add_message("impossible-condition", node=node)
 
     def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool:
         """Check if the condition is redundant."""

tests/test_custom_checkers/test_impossible_condition_checker.py

@@ -262,3 +262,23 @@ def func(x: float):
 
         with self.assertNoMessages():
             self.checker.visit_if(condition_node)
+
+    def test_not_impossible_by_reassignment_one_path(self):
+        src = """
+        def func(x: str, y: int):
+            '''
+            Preconditions:
+                - x in {"a", "b"}
+            '''
+            if y > 0:
+                x = "c"
+            if x == "c":
+                print(x)
+        """
+        z3v = Z3Visitor()
+        mod = z3v.visitor.visit(astroid.parse(src))
+        mod.accept(CFGVisitor())
+        *_, condition_node = mod.nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)

tests/test_custom_checkers/test_redundant_condition_checker.py

@@ -233,3 +233,23 @@ def func(x: float):
 
         with self.assertNoMessages():
             self.checker.visit_if(condition_node)
+
+    def test_not_redundant_by_reassignment_one_path(self):
+        src = """
+        def func(x: str, y: int):
+            '''
+            Preconditions:
+                - x in {"a", "b"}
+            '''
+            if y > 0:
+                x = "c"
+            if x == "a" or x == "b":
+                print(x)
+        """
+        z3v = Z3Visitor()
+        mod = z3v.visitor.visit(astroid.parse(src))
+        mod.accept(CFGVisitor())
+        *_, condition_node = mod.nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)