Re: [klee-dev] KLEE SMT query overhead

2022-03-09 Thread William Leeson
> > 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

Re: [klee-dev] KLEE SMT query overhead

2022-03-09 Thread Frank Busse
Hi, On Tue, 8 Mar 2022 13:58:57 -0500 William Leeson 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 >

[klee-dev] KLEE SMT query overhead

2022-03-09 Thread 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