Wander Lairson Costa <[email protected]> writes: > 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 <[email protected]>
These isinstance() usages deserve to be buried. But I'm not sure yet how to replace them. So, for now: Reviewed-by: Nam Cao <[email protected]>
