This is inspired by the implementation in Z3.
The main idea is that we only need to assert that if we reach some node
in step l+1, then we must have used one of the incoming edges (clauses
where this node is a head) and we must have been in the source of the
edge in step l.
(We also assert that we start at entry at step 0.)
Then we check for each step if we can be in the exit node.
These conditions are sufficient, we do not need the constraints about
forward reachability (if I am at some node then I need to be in one of
its successors in the next step).
This is inspired by the implementation in Z3. The main idea is that we only need to assert that if we reach some node in step l+1, then we must have used one of the incoming edges (clauses where this node is a head) and we must have been in the source of the edge in step l. (We also assert that we start at entry at step 0.) Then we check for each step if we can be in the exit node. These conditions are sufficient, we do not need the constraints about forward reachability (if I am at some node then I need to be in one of its successors in the next step).