As an example of uninterpreted functions for SMT-LIB, we give this input to an [[Satisfiability modulo theories|SMT Solverssolver]]:
(declare-fun f (Int) Int)
(assert (= (f 10) 1))
The SMT Solversolver would return "This input is satisfiable". That happens because <code>f</code> is an uninterpreted function (i.e., all that is known about <code>f</code> is its signature), so it is possible that <code>f(10) = 1</code>. But by applying the input below:
(declare-fun f (Int) Int)
Line 15:
(assert (= (f 10) 42))
The SMT Solversolver would return "This input is unsatisfiable". That happens because although <code>f</code> has no interpretation, but it is impossible that it returns different values for the same input.
