SMT-LIB 2.5 は Z3 などが元々導入していた declare-fun の省略記法である declare-const を採用したけれど、 define-fun の省略記法の define-const の方は採用しなかったんだなぁ……