[klee-dev] Generate all solutions

[Sylvain Gault]

Hello,

I would like to use klee as a front-end to an SMT solver. Basically,
what I currently do is:
- declare input as symbolic;
- write the computation in C;
- test whether the output is the one I want with an "if";
- make klee find an input that activate the "true" branch of the if.

And it works quite well, it produce a solution.
But then I would like to obtain all the input assignments that would
activate that same path.

Is there an easy way to do this?
I have the feeling that a hack-ish way to do this would be to get the
query to kleaver that activate that path (I think I saw an option for
that) and feed it repetidely to kleaver (or another SMT solver), each
time adding a clause negating the previous solutionS.

I think this is a hackish solution because the solver would probably
make the same computation over and over again. While outputing the
solution and backtracking to find the next one directly would probably
be a lot more efficient. But I may be wrong.

Thanks in advance.

Regards,
Sylvain Gault