[klee-dev] Crosschecking core solvers and printing the query causing the mismatch

[Shuo Ding]

Hi All,

My goal is to compare the outputs of two core solvers (e.g. Z3 and STP) and get the query issued to those core solvers causing the mismatch. However, it seems that the -debug-validate-solver option does something slightly different from what I need.

By looking at the code in ConstructSolverChain.cpp (https://github.com/klee/klee/blob/v2.1/lib/Solver/ConstructSolverChain.cpp) of version 2.1, it seems that this implementation compares:

(1) the output of the whole solver chain with the output of the oracle solver (line 72), and

(2) the output of almost the whole solver chain with the output of the solver chain's core solver (line 58).

However, I want to compare two core solvers, and get the query issued to them causing the mismatch.

I guess I can just reorder those solvers to realize that (using --log-partial-queries-early=true to ensure that the mismatched query can be logged). However, I cannot test whether this solution works until I actually find a mismatch. Could someone confirm this or give me some suggestions?

Also, I'm assuming that the debug validating solver will terminate KLEE when it sees a mismatch, as I can see there are some assertions in the implementation of the debug validating solver. Is this correct?

Thanks!

Sincerely,
Shuo

-------------- next part --------------
HTML attachment scrubbed and removed