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
While trying to disable mbqi by disabling both smt.mbqi and auto_config I noticed the following:
When I set the params on the solver using Z3_solver_set_params (without a push), the options are ignored (enabling tracing and checking the log shows mbqi activity). If I add a push (Z3_solver_push) to the program then the options are respected (no mbqi takes place).
Here the release notes mention something similar (push is required for the command to take effect).
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
While trying to disable mbqi by disabling both
smt.mbqi
andauto_config
I noticed the following:When I set the params on the solver using
Z3_solver_set_params
(without a push), the options are ignored (enabling tracing and checking the log shows mbqi activity). If I add a push (Z3_solver_push
) to the program then the options are respected (no mbqi takes place).Here the release notes mention something similar (push is required for the command to take effect).
z3/RELEASE_NOTES.md
Line 46 in 8c5abdf
Setting the parameters globally via
Z3_global_param_set
works as expected (regardless of push).Is this a known quirk, bug, or working as intended? I appreciate any insight!
Beta Was this translation helpful? Give feedback.
All reactions