call a function argument on the remaining arguments
Major Section:  ACL2-BUILT-INS

Oracle-funcall evaluates its first argument to produce an ACL2 function symbol, and then applies that function symbol to the values of the rest of the arguments. The return value is of the form (mv call-result state).

(oracle-funcall 'cons 3 4) ==> (mv '(3 . 4) <state>)
(oracle-funcall (car '(floor foo bar)) (+ 6 7) 5) ==> (mv 2 <state>)

Oracle-funcall is a macro; each of its calls macroexpands to a call of the related utility oracle-apply that takes the ACL2 state as an argument, as follows:

(oracle-funcall fn x1 x2 .. xk)
macroexpands to
(oracle-apply fn (list x1 x2 .. xk) state)

Note that calls of oracle-funcall and oracle-apply return two values: the result of the function application, and a modified state.

See oracle-apply for details, including information about guards.