From the recent 2.6 SMT-LIB Standard sections 1.1.1 - 1.1.4, the following commands are missing:
The current implementation of generalized quantifiers in OpenJML utilize the define-fun-rec command. For older solvers, this command can be implemented as a series of declare-fun and assert forall commands. It is still useful to have the new commands as some solvers can perform additional optimizations.
From the recent 2.6 SMT-LIB Standard sections 1.1.1 - 1.1.4, the following commands are missing:
The current implementation of generalized quantifiers in OpenJML utilize the define-fun-rec command. For older solvers, this command can be implemented as a series of declare-fun and assert forall commands. It is still useful to have the new commands as some solvers can perform additional optimizations.