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 fix(subsumption): missed candidate basic blocks #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:;
}

[ArpitaDutta]

Not getting expected interpolants for the below program.

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <klee/klee.h>
#define loop for(;;)
#define ipoint(var) { int var; klee_make_symbolic(&var, sizeof(int), "var"); if (var) goto END; }

#define MAXDEEP 4

main() {
    int x =1, y=1;
    int B = 1, c = 0;
    
    loop {
      int choice;
       klee_make_symbolic(&choice, sizeof(int), "choice");
       if (choice) {
           	if (B == MAXDEEP) exit(0);
		printf("%d\n",B);
		B++; 
       } else {
	   	c = B;
	   	while (c) {
		       ipoint(var);		        
		       y= y+x;
		       x = (x + 1) % 2 ; 
		       klee_assert(y>=1);
		       c = c - 1;
           	}
	  	break;
       }//EndIf
    }//EndLoop
END:;
}