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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
