[klee-dev] Evaluate the constraints without expr

Paul Marinescu paul.marinescu at imperial.ac.uk
Tue Nov 19 13:56:00 GMT 2013


You're probably looking for TimingSolver::getInitialValues

Paul

On 19/11/13 04:40, jingde liu wrote:
> Hi,
> I want to seed a solution to evaluate the constraints of an
> ExecutionState ignore the expr. In klee, evaluate(ExecutionState, expr,
> Validity) evaluates the result of the expr (constraints--> expr), but
> now I only care about the satisfiability of the constraints. Another
> problem I faced is that I don't know how to track into the functions of
> SolverImpl, when I track the program it stop at the virtual declaration.
>
> Cheers,
> Jingde
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>





More information about the klee-dev mailing list