[klee-dev] Testcase generation

[Martin Nowotny]

Hello,
I have a question regarding the testcase generation in klee.
For example I want to test the following program:

int foo()
{
   if(b>0) {
     // do something
     // already have an existing TC
   }
   else {
     //do something
     // not tested yet
   }
}

If I run klee normally it would give me 2 testcases, one where "b" is 
greater than zero and one not.
But let's say I already have an exisiting testcase for the true-branch, 
so I won't need any.
So what I thought, was that I can either change the outcome of the 
comparison directly in the Executor::executeInstruction,
or for the fact that the Solver will return an unknown case just not add 
the true branch to the Constraints.
Either way it does not seem to affect the outcome of the testcase, 
although it doesn't execute the true branch (I can see
this in the transferToBasicBlock destination).
I tried to figure out the processTestcase, but I didn't really.
Could you give me a hint how klee then in the end gives "b" for example 
the value 0 in the one case and 2147483647 in the other?
Or to be more precise, is it even possible to alter the testcase 
generation in a way that it fits the execution?

Thank you very much,
Martin