Replace `define-const` by `define-fun` (resp. `declare-*`)

leonardoalt / yools

Tools for Yul.

GNU General Public License v3.0

137 stars 5 forks source link

Replace `define-const` by `define-fun` (resp. `declare-*`) #69

Open leonardoalt opened 2 years ago

leonardoalt commented 2 years ago

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.

leonardoalt commented 2 years ago

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.