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

[Cristian Cadar]

Hi, I think what you want is --debug-crosscheck-core-solver.

Best,
Cristian

On 16/09/2020 18:54, Shuo Ding wrote:
> 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
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>