You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In a recent PR, we have changed the SMT retries logic in Kore to scale the timeout exponentially.
When combined with the work to empower the simplifications Booster by using the SMT solver there as well, this leads to very long queries that still result in Unknown in Kore.
In order to have finer control, we need to introduce a command-line option that would allow to configure the scaling strategy:
--smt-timeout-scaling linear will use the factors 2, 3, 4, ...
--smt-timeout-scaling exp will use the factors 2, 4, 8, ...
The text was updated successfully, but these errors were encountered:
In a recent PR, we have changed the SMT retries logic in Kore to scale the timeout exponentially.
When combined with the work to empower the simplifications Booster by using the SMT solver there as well, this leads to very long queries that still result in
Unknown
in Kore.In order to have finer control, we need to introduce a command-line option that would allow to configure the scaling strategy:
--smt-timeout-scaling linear
will use the factors2, 3, 4, ...
--smt-timeout-scaling exp
will use the factors2, 4, 8, ...
The text was updated successfully, but these errors were encountered: