WP propagate to support bb-unmerge

[TheHillBright]

Before this PR, when TX is run with bb-unmerge and WP, TX will soon fallback to deletion due to lack of support this PR adds.

[ArpitaDutta]

1. This commit has solved the previous issue of falling back to deletion.

2. Correctly detected the bug discussed in the last example program of PR #383.

3. However, I have a question regarding the below program, I am not getting the expected interpolants for the ipoint(var).

Every new iteration wrt. variable B (value 2 onwards) is into generating the nodes for the branch corresponding to ipoint(var).

Could you please look into this?

For example,

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

#define loop for(;;)

#define f(x) (x + 2)
#define p(x) (x != 5)

#define ipoint(var) { int var; klee_make_symbolic(&var, sizeof(int), "var"); if (var) goto END; }

#define MAXDEEP 4

main() {
    int B = 1, c, x = 0;
    loop {
       int choice;
       klee_make_symbolic(&choice, sizeof(int), "choice");
       if (choice) {
            if (B == MAXDEEP) goto END;
               B++;
       } else {
               c = B;
               while (c) {
                     ipoint(var);
                     x = f(x);
                     klee_assert(p(x));
                     c = c - 1;
            }
                 break;
       }//EndIf
    }//EndLoop
END:;
}