[klee-dev] displaying constraints for each test case

[Chris Murphy]

Hello. Is there a way for KLEE to display the query/constraint that is  
being solved with a particular test case? For instance, I have a  
simple function like this:

int test (int a, int b) {
    if (a > b) {
       if (a == 5) return 3;
       else return 2;
    }
    else return 1;
}

In addition to having the concrete values for each test case, I'd also  
like the output to include the fact that:
test case #1 solves !(a > b)
test case #2 solves (a > b) && !(a == 5)
test case #3 solves (a > b) && (a == 5)

By calling vc_printQueryStateToBuffer in  
STPSolverImpl::computeInitialValues I can see the raw queries as they  
fly by, but not the specific constraints that are associated with a  
given test case. Any thoughts?

Thanks!

Chris