fix(subsumption): missed candidate basic blocks

[yxliang01]

This fixes a lot of candidate basic blocks incorrectly ignored for subsumption. Some fixing required for this patch and will be done after initial benchmarking.

[rasoolmaghareh]

I did a quick review for now and it seems to me that the logic is correct. Let's wait for @sanghu1790 example which is creating over-subsumption and then from there we can proceed with a fix of the over-subsumption issue.

[rasoolmaghareh]

Is this PR ready to be merged?

[rasoolmaghareh]

Looks good to me. Maybe please update the title of the pull request, squash the commits into 1 commit and add a comment in the commit message which explains the changes that you made in 2-3 lines

[ArpitaDutta]

I have tested this PR in the below program.

#include <klee/klee.h>
#include <assert.h>

int main(int argc, char **argv) {
  int counter;
  counter = 0;
  int choice;
  for (int i = 0; i < 3; i++) {
   klee_make_symbolic(&choice, sizeof(int), "choice");
    if (choice) {
      counter = counter + 1;
    } else {
      counter += i;
    }
  }

// 4 is the maximum value for counter
klee_assert(counter != 4);

  return 0;
}

The PR is missing the bug for wp-interpolantion when the --bb-unmerge is on. Also, the wp-interpolants are getting switched for the deletion for most of the program points by using this option.

The number of paths and other stats changes for the Deletion interpolation as well.

[rasoolmaghareh]

We have decided to merge this MR first and then address the WP interpolant generation in the presence of the bb-unmerge in another MR. This command line option is experimental and can cause WP interpolation to fall back to deletion.