Revision as of 07:38, 27 April 2021 edit Jochen Burghardt (talk \| contribs) Extended confirmed users 24,306 edits →Example: slightly rephrase to avoid "we", per MOS:WE ← Previous edit		Revision as of 08:24, 27 April 2021 edit undo Hooman Mallahzadeh (talk \| contribs) Extended confirmed users 4,638 edits m →Example: lower case. Next edit →
Line 17: (assert (= (f 10) 42)) </syntaxhighlight> ~~The~~the SMT solver 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. ==Discussion==

Uninterpreted function: Difference between revisions