> > Are we talking about "orders of magnitude" in the milli/micro-second > range or about really expensive queries?
Expensive. If it helps, I ran klee for 5 hours on the most recent version of find with the following settings: klee --simplify-sym-indices --write-cvcs --write-cov --output-module --max-memory=2000 --disable-inlining --optimize --use-forked-solver --use-cex-cache --libc=uclibc --posix-runtime --external-calls=all --only-output-states-covering-new --use-query-log=solver:smt2 --env-file=test.env --run-in-dir=/tmp/sandbox --write-smt2s --max-sym-array-size=4096 --max-time=300min --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal --search=random-path --search=nurs:covnew --use-batching-search --batch-instructions=10000 findutils-4.9.0/obj-llvm/find/find.bc -sym-args 0 3 20 -sym-files 1 40 -sym-stdin 40 There are 10 queries listed as taking over 100s in the solver-queries.smt2 file, but when I ask STP to solve them, it takes somewhere between 0.6 and 1.7 seconds to solve. Are you using the solvers in the container directly or via kleaver? > The results described above, directly in the container. However, I have replicated it on a full install of klee with Z3. Should I be using kleaver? Sorry for the duplicate message. I just realized I didn't reply all. Thank you, Will On Wed, Mar 9, 2022 at 10:57 AM Frank Busse <f.bu...@imperial.ac.uk> wrote: > 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 >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
