From: Wander Lairson Costa Date: Mon, 23 Feb 2026 16:17:58 +0000 (-0300) Subject: rv/rvgen: fix isinstance check in Variable.expand() X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=8aee49c5a53a57014af08de6687a67de7fb679d8;p=thirdparty%2Fkernel%2Flinux.git rv/rvgen: fix isinstance check in Variable.expand() The Variable.expand() method in ltl2ba.py performs contradiction detection by checking if a negated variable already exists in the graph node's old set. However, the isinstance check was incorrectly testing the ASTNode wrapper instead of the wrapped operator, causing the check to always return False. The old set contains ASTNode instances which wrap LTL operators via their .op attribute. The fix changes isinstance(f, NotOp) to isinstance(f.op, NotOp) to correctly examine the wrapped operator type. This follows the established pattern used elsewhere in the file, such as the iteration at lines 572-574 which accesses o.op.is_temporal() on items from node.old. Signed-off-by: Wander Lairson Costa Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260223162407.147003-16-wander@redhat.com Signed-off-by: Gabriele Monaco --- diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py index f9855dfa3bc1c..7f538598a8681 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -395,7 +395,7 @@ class Variable: @staticmethod def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: for f in node.old: - if isinstance(f, NotOp) and f.op.child is n: + if isinstance(f.op, NotOp) and f.op.child is n: return node_set node.old |= {n} return node.expand(node_set)