@bronevet you should take a look at this. I believe this was a bug. setLatticePost was being done outside the set<CFGNode> iteration. I brought it inside the loop. If it was the first cfgnode in the iteration, the post state will be set and in the else part, we use the unionLattice to merge the new dataflow information.