Hi Qiuping,
Can you open an issue on GitHub where you provide more details
(including the LLVM bitcode file that you are running)? The way I would
suggest to start debugging this is to look where the two paths diverge,
and first check whether there is any non-determinism in the program itself.
Best,
Cristian
On 02/11/13 16:20, Qiuping Yi wrote:
Hi,
I ran klee on 'findutils' under the same input without any symbolic
variable, and want to get a determinate execution. However, I get two
different executions randomly(one path with a bigger probability). Why?
How can I get a determinate execution? Thank you very much.
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
