[klee-dev] Default counterexample value generated by solver

[Cristian Cadar]

Hi Weiqi,

There is an open PR trying to implement this behaviour, but 
unfortunately it has not been finalized yet (perhaps you'd like to work 
on it?):
https://github.com/klee/klee/pull/1117

Best,
Cristian

P.S. Kleaver does not pick the smallest valid value, the value generally 
comes from the solver

On 20/09/2021 16:59, Weiqi Wang wrote:
> Hi,
> 
> I observed that when asked for a counterexample, kleaver picks the 
> smallest valid value. I’m wondering if there’s a way to “seed the 
> solver” so that it prioritizes the value given in the seed? For example, 
> given constraint x != 1, the counterexample value would be 0. With a 
> seed value 3, the solver picks 3 instead.
> 
> Best,
> 
> Weiqi
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>