Function:
(defun svex-add-delay-top (x delay) (declare (xargs :guard (and (svex-p x) (natp delay)))) (let ((__function__ 'svex-add-delay-top)) (declare (ignorable __function__)) (mbe :logic (svex-add-delay x delay) :exec (if (zp delay) x (svex-add-delay x delay)))))