Revision as of 21:30, 20 November 2021 edit 67.198.37.16 (talk) →See also: Theory of pure equality ← Previous edit		Revision as of 17:58, 7 December 2021 edit undo 27.85.207.129 (talk) Corrected some grammatical errors that made the conclusion confusing. Next edit →
Line 17: (assert (= (f 10) 42)) </syntaxhighlight> the SMT solver would return "This input is unsatisfiable". That happens because ~~although~~ <code>f</code> has no interpretation, ~~but~~as it is impossible that it returns different values for the same input. ==Discussion==

Uninterpreted function: Difference between revisions