Hi Jie,
Sorry for the delayed answer here. This is something that we and others
have occasionally observed. The issue is that by saving the query to a
file and then reading it from that file, the solver may end up with a
slightly different (albeit semantically equivalent) query to solve. In
most cases, the semantically-equivalent query still leads to a timeout,
but not always. In addition, KLEE may internally set various options
for the solver (either explicitly or implicitly).
To reproduce the timeout in such cases, you will need to save the exact
sequence of API calls sent to the solver. We are actually building
support in my group for this scenario, but it's not something that will
be available in the near future.
Best,
Cristian
On 13/09/2025 23:16, Jie wrote:
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
