If a node is infeasible (assertion or assumption that is false or unsat), then that node needs to be prevented from getting added to work queue. There's conflict w/ control flow resync logic (which queues nodes for resynchronization), if they're deemed infeasible, these nodes are removed, but then the control flow sync adds the nodes again and causes infinite loop.
This could happen if we manually add assumptions to the verifier.
If a node is infeasible (assertion or assumption that is false or unsat), then that node needs to be prevented from getting added to work queue. There's conflict w/ control flow resync logic (which queues nodes for resynchronization), if they're deemed infeasible, these nodes are removed, but then the control flow sync adds the nodes again and causes infinite loop.
This could happen if we manually add assumptions to the verifier.