Fake-oracle-eval
fake-oracle-eval is the function run by default when oracle-eval is invoked.
Oracle-eval is a constrained function, and
fake-oracle-eval is attached to it by default (see defattach).
Fake-oracle-eval doesn't do anything useful, but also doesn't require a
trust tag. To allow oracle-eval to do something useful, run
(ALLOW-REAL-ORACLE-EVAL); this introduces a trust tag and attaches the
function real-oracle-eval to oracle-eval.
See oracle-eval for details.
Definitions and Theorems
Function: fake-oracle-eval
(defun fake-oracle-eval (term alist state)
(declare (xargs :guard t :stobjs state)
(ignore term alist))
(mv *fake-oracle-eval-msg* nil state))
