Dear KLEE Team,
I'm writing to ask about time-out queries generated by KLEE. I'm trying to identify program paths that cause the solver to time out. To dump the queries, I used the latest KLEE master branch with the following command: klee --search=dfs --posix-runtime --write-kqueries --libc=uclibc --max-solver-time=10s --max-time=600s lua.bc A -sym-files 1 40 Here is the output I received, which is associated to test000002 (confirmed by the test000002.solver.err). KLEE: ERROR: lstring.c:197: Query timed out (resolve). When I run kleaver to reproduce the timeout, I get a SAT result instead. My exact command is below. kleaver --max-solver-time=10s /tmp/out/lua-ttt/test000002.kquery I've searched the email archive but couldn't find relevant answers to my question. Could you please let me know how KLEE handles dumping queries on solver time-outs? Am I missing any options or settings? Thank you for your help. Best, Jie
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
