Function:
(defun apply-m-assumption-n-output-transform! (m n aignet transform state) (declare (xargs :stobjs (aignet state))) (declare (xargs :guard (and (natp m) (natp n)))) (declare (xargs :guard (<= (+ m n) (num-outs aignet)))) (let ((__function__ 'apply-m-assumption-n-output-transform!)) (declare (ignorable __function__)) (mbe :logic (non-exec (apply-m-assumption-n-output-transform m n aignet nil transform state)) :exec (b* (((local-stobjs aignet2) (mv aignet aignet2 state)) ((mv aignet2 state) (apply-m-assumption-n-output-transform m n aignet aignet2 transform state)) ((mv aignet aignet2) (swap-stobjs aignet aignet2))) (mv aignet aignet2 state)))))