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
define-const is actually not smtlib2 and some solvers won't support that (here I'm referring to Bitwuzla). We should replace it by define-fun which is in the standard.
Same for declare-const -> declare-fun.
The text was updated successfully, but these errors were encountered:
This is easy to do, and we should do it in the future. However currently Bitwuzla doesn't support a few things that we require (eg Arrays as arguments of UFs), so fine to leave it as is for now.
define-const
is actually not smtlib2 and some solvers won't support that (here I'm referring to Bitwuzla). We should replace it bydefine-fun
which is in the standard.Same for
declare-const -> declare-fun
.The text was updated successfully, but these errors were encountered: