Hi,
On Tue, 8 Mar 2022 13:58:57 -0500 William Leeson <wel...@virginia.edu> wrote: > 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. Are we talking about "orders of magnitude" in the milli/micro-second range or about really expensive queries? > 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?) There is no incremental solving in upstream KLEE. The time is measured by another pseudo-solver in the solving chain (QueryLoggingSolver) in front of the core solvers (STP, Z3, MetaSMT). Hence, there is overhead involved, e.g. the conversion of KLEE's native expressions into solver-specific queries or for STP even a call of fork() depending on the configuration. Are you using the solvers in the container directly or via kleaver? Kind regards, Frank _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
