Ensure That Subsumption Checks Are at the Correct Points

[domainexpert]

As search tree branching could be the result of non-control-flow branching, the storage of interpolant and subsumption check should be based on instruction id instead of basic block id.

[domainexpert]

I think for this issue it is important to try to come up first with a unit test or regression test case that exhibit the problem (if any). (KLEE's unit tests are invoked using make unittests and the regression suite using make check.)

[domainexpert]

The index of interpolant and subsumption check already use the pointer address of the first instruction in the state / interpolation tree node. Updated comment in #18 to clarify this issue. Closed it.