declare-fun vs declare-const in SMT2

Question

I get confused about the following two declarations. For me, they describe the same thing: an integer variable x.

• (declare-const x Int)
• (declare-fun x () Int)

Is there any context that make them different in performance or provide different model? Thanks.

Answer 1

Yes, (declare-const x Int) is just syntax sugar (declare-fun x () Int). There is no difference in performance. Note that declare-const is not part of the SMT-Lib 2.0 standard.