Uninterpreted function: Difference between revisions

Revision as of 07:16, 27 April 2021

Revision as of 07:21, 27 April 2021

Line 11:

(assert (= (f 10) 1))

</syntaxhighlight>

The SMT solver 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 (logic)|signature]]), so it is possible that <code>f(10) = 1</code>. But by applying the input below:

<syntaxhighlight lang="text" line="1">

(declare-fun f (Int) Int)