[SMT-LIB] New draft of Version 2.5 of SMT-LIB released

[Florian Schanda]

On Wednesday 18 Mar 2015 04:47:50 Tinelli, Cesare wrote:
> Command declare-const
> ---------------------
> 
> A couple of people have asked why we added declare-const but not
> define-const. Neither one is needed and neither one introduces much
> simplification, but we added the former by popular demand (possibly
> created by the fact that Z3 has declare-const). In the spirit of keeping
> the command set small, we would like to introduce define-const only when,
> and if, we get enough requests for it.

I think define-const (if we have a declare-const) would be nice to have.

Thanks,

	Florian