use declare-fun instead of declare-const in SMT translation
declare-const was only added in SMTLIB 2.5 as a shortcut for a declare-fun taking no parameters. Some solvers only support the base SMTLIB 2.0, so using the expanded syntax gives us access to more alternative solvers.
parent
b96aac29
Please register or sign in to comment