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 _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
