[klee-dev] KLEE SMT query overhead

[William Leeson]

Hello,

I'm working on a project dealing with SMT solvers. We are collecting
queries from KLEE using the latest klee docker image with the
"--use-query-log=solver:smt2" flag on. We are then dividing this file into
individual queries. We run several SMT solvers on these queries and collect
the execution time.

I'm finding that the Elapsed time reported by KLEE in solver-queries.smt2
for a single query is  different from the time reported by the solver klee
is built on (stp_simple in the docker /tmp folder). Orders of magnitude
different. I confirmed this on a local install of KLEE with Z3-4.8.4 as the
backend solver.

I was wondering if this is to be expected. Is there some overhead KLEE
incurs when calling the solvers? Is the solver being fed more than Query #X
from solver-queries.smt2 (For example, is it an incremental solve with
previous queries taken into account?)

Thank you,
Will
-------------- next part --------------
HTML attachment scrubbed and removed