diff --git a/CHANGELOG.md b/CHANGELOG.md
index 776adec2d..bffec8c9b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,9 @@ and adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
 ### 💫 New checkers
 
+- `redundant-condition`: Provide error message when a conditional statement within a function is guaranteed true. This checker requires `z3` option to be turned on.
+- `impossible-condition`: Provide error message when a conditional statement within a function is guaranteed false. This checker requires `z3` option to be turned on.
+
 ### 🐛 Bug fixes
 
 ### 🔧 Internal changes
diff --git a/docs/checkers/index.md b/docs/checkers/index.md
index 0b4019085..ebccbd2a5 100644
--- a/docs/checkers/index.md
+++ b/docs/checkers/index.md
@@ -2699,6 +2699,48 @@ python_ta.check_all(config={
 })
 ```
 
+(R9900)=
+
+### Redundant Condition (R9900)
+
+This error occurs when an `if` or `while` condition is guaranteed to be true.
+
+Example:
+
+```{literalinclude} /../examples/custom_checkers/r9900_redundant_condition.py
+
+```
+
+This error will only be checked if the `z3-solver` library is installed and `z3` option of PythonTA
+is enabled:
+
+```python
+import python_ta
+python_ta.check_all(config={
+    "z3": True
+})
+```
+
+### Impossible Condition (R9901)
+
+This error occurs when an `if` or `while` condition is guaranteed to be false.
+
+Example:
+
+```{literalinclude} /../examples/custom_checkers/r9901_impossible_condition.py
+
+```
+
+This error will only be checked if the `z3-solver` library is installed and `z3` option of PythonTA
+is enabled:
+
+```python
+import python_ta
+python_ta.check_all(config={
+    "z3": True
+})
+```
+
 ## Miscellaneous
 
 (E1305)=
diff --git a/examples/custom_checkers/r9900_redundant_condition.py b/examples/custom_checkers/r9900_redundant_condition.py
new file mode 100644
index 000000000..0d745c925
--- /dev/null
+++ b/examples/custom_checkers/r9900_redundant_condition.py
@@ -0,0 +1,23 @@
+def return_large_number(x: int) -> int:
+    """Return number x only if it's greater than 1000
+
+    Preconditions:
+        - x > 1000
+    """
+    # the if condition is already checked by function precondition
+    if x > 1000:   # Error on this line
+        return x
+
+
+def nested_condition(x: int) -> int:
+    if x > 10:
+        # the condition `x > 5` is already guaranteed by `x > 10`
+        if x > 5:   # Error on this line
+            return x
+    return 0
+
+
+def redundant_condition(x: bool) -> None:
+    # the if condition is always true
+    if x or not x:     # Error on this line
+        print("redundant")
diff --git a/examples/custom_checkers/r9901_impossible_condition.py b/examples/custom_checkers/r9901_impossible_condition.py
new file mode 100644
index 000000000..505846e23
--- /dev/null
+++ b/examples/custom_checkers/r9901_impossible_condition.py
@@ -0,0 +1,28 @@
+def print_none_negative_number(x: int) -> None:
+    """Print number x only if it's greater or equal to 0
+
+    Preconditions:
+        - x >= 0
+    """
+    # the if condition is impossible given the function precondition
+    if x < 0:   # Error on this line
+        raise Exception("x is smaller than zero")
+    print(x)
+
+
+def impossible_condition(x: bool) -> None:
+    # the if condition is always false
+    if x and not x:     # Error on this line
+        print("impossible")
+
+
+def display_number(x: int) -> str:
+    """Display numbers 0 to 2 in word"""
+    if x == 0:
+        "zero"
+    elif x == 1:
+        return "one"
+    elif x == 2:
+        return "two"
+    elif x == 2:    # Error on this line
+        return "two again"
diff --git a/python_ta/cfg/graph.py b/python_ta/cfg/graph.py
index 4f547e94d..7be66a5de 100644
--- a/python_ta/cfg/graph.py
+++ b/python_ta/cfg/graph.py
@@ -56,7 +56,7 @@ class ControlFlowGraph:
     # z3 constraints of preconditions
     precondition_constraints: List[ExprRef]
     # map from variable names to z3 variables
-    _z3_vars: Dict[str, ExprRef]
+    z3_vars: Dict[str, ExprRef]
 
     def __init__(self, cfg_id: int = 0) -> None:
         self.block_count = 0
@@ -64,7 +64,7 @@ def __init__(self, cfg_id: int = 0) -> None:
         self.unreachable_blocks = set()
         self.start = self.create_block()
         self.end = self.create_block()
-        self._z3_vars = {}
+        self.z3_vars = {}
         self.precondition_constraints = []
 
     def add_arguments(self, args: Arguments) -> None:
@@ -76,7 +76,7 @@ def add_arguments(self, args: Arguments) -> None:
             # Parse types
             parser = Z3Parser()
             z3_vars = parser.parse_arguments(args)
-            self._z3_vars.update(z3_vars)
+            self.z3_vars.update(z3_vars)
 
     def create_block(
         self,
@@ -276,7 +276,7 @@ def update_edge_z3_constraints(self) -> None:
 
         for path_id, path in enumerate(self.get_paths()):
             # starting a new path
-            z3_environment = Z3Environment(self._z3_vars, self.precondition_constraints)
+            z3_environment = Z3Environment(self.z3_vars, self.precondition_constraints)
             for edge in path:
                 # traverse through edge
                 if edge.condition is not None:
diff --git a/python_ta/checkers/condition_logic_checker.py b/python_ta/checkers/condition_logic_checker.py
new file mode 100644
index 000000000..c2b8731e0
--- /dev/null
+++ b/python_ta/checkers/condition_logic_checker.py
@@ -0,0 +1,115 @@
+"""
+Check for redundant/impossible If or While conditions in functions based on z3 constraints
+"""
+
+from __future__ import annotations
+
+from typing import Any, Union
+
+try:
+    import z3
+
+    from ..cfg.graph import Z3Environment
+
+    z3_dependency_available = True
+except ImportError:
+    z3 = Any
+    Z3Environment = Any
+    z3_dependency_available = False
+
+from astroid import nodes
+from pylint.checkers import BaseChecker
+from pylint.checkers.utils import only_required_for_messages
+from pylint.lint import PyLinter
+
+
+class ConditionLogicChecker(BaseChecker):
+    name = "redundant-condition"
+    msgs = {
+        "R9900": (
+            """This condition will always evaluate to True.""",
+            "redundant-condition",
+            "Used when an If or While statement is always True. Requires the z3 configuration option to be True.",
+        ),
+        "R9901": (
+            """This condition will always evaluate to False.""",
+            "impossible-condition",
+            "Used when an If or While statement is always False. Requires the z3 configuration option to be True.",
+        ),
+    }
+    options = (
+        (
+            "z3",
+            {
+                "default": False,
+                "type": "yn",
+                "metavar": "<y or n>",
+                "help": "Use Z3 to perform logical feasibility analysis in program control flow.",
+            },
+        ),
+    )
+
+    @only_required_for_messages("redundant-condition", "impossible-condition")
+    def visit_if(self, node: nodes.If) -> None:
+        """Visit if statement"""
+        self._check_condition(node)
+
+    @only_required_for_messages("redundant-condition", "impossible-condition")
+    def visit_while(self, node: nodes.While) -> None:
+        """Visit while statement"""
+        self._check_condition(node)
+
+    def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None:
+        """Check whether a condition in an `if` or `while` statement is redundant
+        or impossible based on the feasible execution paths.
+
+        - A condition is redundant if for every feasible execution path
+        leading to the node, the condition must be True due to precedent constraints.
+        - A condition is impossible if for every feasible execution path
+        leading to the node, the condition must be False due to precedent constraints.
+        """
+        if (
+            not hasattr(node, "cfg_block")
+            or not z3_dependency_available
+            or not self.linter.config.z3
+        ):
+            return
+
+        node_block = node.cfg_block
+
+        # create node condition z3 constraint
+        condition_node = node.test
+        env = Z3Environment(node.frame().cfg.z3_vars, [])
+        z3_condition = env.parse_constraint(condition_node)
+
+        if z3_condition is None:
+            return
+
+        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.test)
+
+        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.test)
+
+    def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool:
+        """Check if the conjunction of the given constraints is unsatisfiable.
+
+        - prev_constraints (z3.ExprRef): Constraints from previous nodes.
+        - node_constraint (z3.ExprRef): The condition to check at the current node.
+        """
+        solver = z3.Solver()
+        solver.add(z3.And(prev_constraints, node_constraint))
+        return solver.check() == z3.unsat
+
+
+def register(linter: PyLinter) -> None:
+    """Required method to auto-register this checker to the linter."""
+    linter.register_checker(ConditionLogicChecker(linter))
diff --git a/python_ta/patches/transforms.py b/python_ta/patches/transforms.py
index c7f99ad47..0baec8c50 100644
--- a/python_ta/patches/transforms.py
+++ b/python_ta/patches/transforms.py
@@ -27,7 +27,10 @@ def new_get_ast(self, filepath, modname, data):
 
         # Run the CFGVisitor
         try:
-            ast.accept(CFGVisitor())
+            if z3:
+                ast.accept(CFGVisitor(options={"separate-condition-blocks": True}))
+            else:
+                ast.accept(CFGVisitor())
         except Exception as e:
             logging.warning(f"Could not run Z3Visitor: {e}")
 
diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py
new file mode 100644
index 000000000..73fbb438e
--- /dev/null
+++ b/tests/test_custom_checkers/test_impossible_condition_checker.py
@@ -0,0 +1,263 @@
+import astroid
+import pylint.testutils
+from astroid import nodes
+
+from python_ta.cfg import CFGVisitor
+from python_ta.checkers.condition_logic_checker import ConditionLogicChecker
+from python_ta.transforms.z3_visitor import Z3Visitor
+
+
+class TestImpossibleConditionChecker(pylint.testutils.CheckerTestCase):
+    CHECKER_CLASS = ConditionLogicChecker
+    CONFIG = {"z3": True}
+
+    def test_impossible_by_precondition(self):
+        src = """
+        def func(x: float):
+            '''
+            Preconditions:
+                - x > 5.0
+            '''
+            if x < 0.0:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_impossible_by_if_condition(self):
+        src = """
+        def func(x: int):
+            if x > 5:
+                if x < 3:
+                    print(x)
+        """
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_impossible_conditional_statement(self):
+        src = """
+        def func(x: int):
+            if x > 0 and x < 0:
+                print("impossible")
+        """
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_impossible_if_else(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x > 0
+            '''
+            if x <= 0:
+                return x
+            else:
+                return 0
+        """
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_impossible_by_while_condition(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x > 10
+            '''
+            while x > 0:
+                if x < 0:
+                    print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_impossible_condition_multiple_if_else(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x in {1, 2, 3}
+            '''
+            if x == 1:
+                print(1)
+            elif x == 2:
+                print(2)
+            elif x == 4:
+                print(2)
+            elif x == 3:
+                print(3)
+            else:
+                print(0)
+        """
+        _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_impossible_condition_repeat_checking_if_else(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x in {1, 2, 3}
+            '''
+            if x == 1:
+                print(1)
+            elif x == 2:
+                print(2)
+            elif x == 2:
+                print(2)
+            elif x == 3:
+                print(3)
+            else:
+                print(0)
+        """
+        _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="impossible-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_possible_condition(self):
+        src = """
+        def func(x: str):
+            '''
+            Preconditions:
+                - x[0:2] == "ab"
+            '''
+            if x == "abc":
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_partially_impossible_condition(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x > 5
+            '''
+            if x > 10 or x < 5:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_impossible_condition_variable_reassignment(self):
+        src = """
+        def func(x: int, y: bool):
+            '''
+            Preconditions:
+                - x > 10
+            '''
+            if not y:
+                x = -1
+            if x < 0:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_impossible_condition_partial_path(self):
+        src = """
+        def func(x: int):
+            if x > 5:
+                print(x)
+            else:
+                print(x)
+            if x < 0:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_not_impossible_by_reassignment(self):
+        src = """
+        def func(x: float):
+            '''
+            Preconditions:
+                - x in [1.0, 2.0]
+            '''
+            x = None
+            if x == 3.0:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        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)
+        """
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_unparsed_condition(self):
+        src = """
+        def func(a: int):
+            if a > 5:
+                print(a)
+        """
+
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def _apply_cfg_visitor(self, src: str) -> nodes.NodeNG:
+        z3v = Z3Visitor()
+        mod = z3v.visitor.visit(astroid.parse(src))
+        mod.accept(CFGVisitor(options={"separate-condition-blocks": True}))
+        return mod
diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py
new file mode 100644
index 000000000..465553f98
--- /dev/null
+++ b/tests/test_custom_checkers/test_redundant_condition_checker.py
@@ -0,0 +1,238 @@
+import astroid
+import pylint.testutils
+from astroid import nodes
+
+from python_ta.cfg import CFGVisitor
+from python_ta.checkers.condition_logic_checker import ConditionLogicChecker
+from python_ta.transforms.z3_visitor import Z3Visitor
+
+
+class TestRedundantConditionChecker(pylint.testutils.CheckerTestCase):
+    CHECKER_CLASS = ConditionLogicChecker
+    CONFIG = {"z3": True}
+
+    def test_redundant_by_precondition(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x > 10
+            '''
+            if x > 5:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_redundant_by_if_condition(self):
+        src = """
+        def func(x: int):
+            if x > 5:
+                if x > 3:
+                    print(x)
+        """
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_redundant_by_while_condition(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x > 10
+            '''
+            while x > 0:
+                if x != 0:
+                    print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_redundant_if_else(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x > 0
+            '''
+            if x > 0:
+                return x
+            else:
+                return 0
+        """
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_redundant_condition_within_statement(self):
+        src = """
+        def func(x: bool):
+            if x or not x:
+                return x
+        """
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_redundant_condition_multiple_if_else(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x in {1, 2, 3}
+            '''
+            if x == 1:
+                print(1)
+            elif x == 2:
+                print(2)
+            elif x != 2:
+                print(2)
+            elif x == 3:
+                print(3)
+            else:
+                print(0)
+        """
+        _, _, condition_node, _ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertAddsMessages(
+            pylint.testutils.MessageTest(msg_id="redundant-condition", node=condition_node.test),
+            ignore_position=True,
+        ):
+            self.checker.visit_if(condition_node)
+
+    def test_not_redundant_condition(self):
+        src = """
+        def func(x: str):
+            '''
+            Preconditions:
+                - x[0:2] == "ab"
+            '''
+            if x != "abc":
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_partially_redundant_condition(self):
+        src = """
+        def func(x: int):
+            '''
+            Preconditions:
+                - x > 10
+            '''
+            if x > 10 and x < 15:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_redundant_condition_variable_reassignment(self):
+        src = """
+        def func(x: int, y: bool):
+            '''
+            Preconditions:
+                - x > 10
+            '''
+            if not y:
+                x = -1
+            if x > 0:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_redundant_condition_partial_path(self):
+        src = """
+        def func(x: int):
+            if x > 5:
+                print(x)
+            else:
+                print(x)
+            if x > 0:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_not_redundant_by_reassignment(self):
+        src = """
+        def func(x: float):
+            '''
+            Preconditions:
+                - x in [1.0, 2.0]
+            '''
+            x = None
+            if x == 1.0 or x == 2.0:
+                print(x)
+        """
+        condition_node, *_ = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        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)
+        """
+
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def test_unparsed_condition(self):
+        src = """
+        def func(a: int):
+            if a > 5:
+                print(a)
+        """
+
+        *_, condition_node = self._apply_cfg_visitor(src).nodes_of_class(nodes.If)
+
+        with self.assertNoMessages():
+            self.checker.visit_if(condition_node)
+
+    def _apply_cfg_visitor(self, src: str) -> nodes.NodeNG:
+        z3v = Z3Visitor()
+        mod = z3v.visitor.visit(astroid.parse(src))
+        mod.accept(CFGVisitor(options={"separate-condition-blocks": True}))
+        return mod
diff --git a/tests/test_examples.py b/tests/test_examples.py
index 52d67322b..c38e4d8c3 100644
--- a/tests/test_examples.py
+++ b/tests/test_examples.py
@@ -82,6 +82,7 @@ def _symbols_by_file_pyta(paths: list[str], include_msg: bool = False) -> dict[s
         config={
             "output-format": "python_ta.reporters.JSONReporter",
             "enable": ["C9960"],
+            "z3": True,
         },
     )
 
@@ -149,7 +150,7 @@ def test_examples_files_pyta(test_file: str, pyta_examples_symbols: dict[str, se
     found_pylint_message = checker_name in file_symbols
     assert (
         found_pylint_message
-    ), f"Failed {test_file}. File does not add expected message  {file_symbols}."
+    ), f"Failed {test_file}. File does not add expected message {checker_name}: {file_symbols}."
 
 
 @pytest.mark.parametrize("test_file", get_file_paths(_PYCODESTYLE_PATH))
diff --git a/tests/test_z3_visitor.py b/tests/test_z3_visitor.py
index 3aaa7b700..b69e811c7 100644
--- a/tests/test_z3_visitor.py
+++ b/tests/test_z3_visitor.py
@@ -365,8 +365,8 @@ def test_cfg_z3_vars_initialization():
     cfg = ControlFlowGraph()
     cfg.add_arguments(node.args)
 
-    assert len(cfg._z3_vars) == 4
-    assert cfg._z3_vars["x"] == z3.Int("x")
-    assert cfg._z3_vars["y"] == z3.Real("y")
-    assert cfg._z3_vars["z"] == z3.Bool("z")
-    assert cfg._z3_vars["a"] == z3.String("a")
+    assert len(cfg.z3_vars) == 4
+    assert cfg.z3_vars["x"] == z3.Int("x")
+    assert cfg.z3_vars["y"] == z3.Real("y")
+    assert cfg.z3_vars["z"] == z3.Bool("z")
+    assert cfg.z3_vars["a"] == z3.String("a")