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

2020-09-21 Thread 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

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

2020-09-16 Thread 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