You should also take a look at --debug-crosscheck-core-solver, which
makes it possible to crosscheck the results of the default solver
against a different solver. This could be leveraged to build a
per-query portfolio solver.
Best,
Cristian
On 17/03/2026 07:14, Frank Busse wrote:
Hi,
On Mon, 16 Mar 2026 18:17:37 +0000
Yuxiang Lin <[email protected]> wrote:
The reason I want to ask this is that for the specific project I ran
KLEE on, I have encountered solver timeouts even with very long
solver timeout settings (e.g. 5 minutes). I have not done a deep
investigation on the offending queries yet, but I just thought that
portfolio solving might mitigate this problem to some extent.
You could log those queries (--log-timed-out-queries, should be on by
default) and send them to Z3/STP individually to see if that would
actually help.
Kind regards,
Frank
_______________________________________________
klee-dev mailing list -- [email protected]
To unsubscribe send an email to [email protected]
_______________________________________________
klee-dev mailing list -- [email protected]
To unsubscribe send an email to [email protected]
