[klee-dev] Default counterexample value generated by solver

[Weiqi Wang]

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

-------------- next part --------------
HTML attachment scrubbed and removed