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
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,
