]> git.ipfire.org Git - thirdparty/kernel/linux.git/commit
rv/rvgen: fix isinstance check in Variable.expand()
authorWander Lairson Costa <wander@redhat.com>
Mon, 23 Feb 2026 16:17:58 +0000 (13:17 -0300)
committerGabriele Monaco <gmonaco@redhat.com>
Wed, 1 Apr 2026 08:16:19 +0000 (10:16 +0200)
commit8aee49c5a53a57014af08de6687a67de7fb679d8
tree18e9b7de2ba70bfde99613cc6bdaea5a269d2d99
parentd7ee96234b2ae6ed86a68f5e3792cb17829698ef
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 <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260223162407.147003-16-wander@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
tools/verification/rvgen/rvgen/ltl2ba.py