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
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
