Please disregard my message. I found what I wanted with the -write-cvcs flag.
Chris
Quoting Chris Murphy <cdmurphy at seas.upenn.edu>:
>
> 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
>
