		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Inc1-4-pc

Signature
(inc1-4-pc stat1 feat) → *

Definitions and Theorems

Function: inc1-4-pc

(defun inc1-4-pc (stat1 feat)
  (declare (xargs :stobjs (stat1)))
  (declare (xargs :non-executable t
                  :guard (and (stat1p stat1)
                              (b* ((stat (stat-from-stat1 stat1)))
                                (and (statp stat)
                                     (featp feat)
                                     (stat-validp stat feat))))))
  (prog2$
       (acl2::throw-nonexec-error 'inc1-4-pc
                                  (list stat1 feat))
       (let ((__function__ 'inc1-4-pc))
         (declare (ignorable __function__))
         (if (mbt (stat1p stat1))
             (stat1-from-stat (b* ((stat (stat-from-stat1 stat1)))
                                (write-pc (+ (read-pc stat feat) 4)
                                          stat feat)))
           stat1))))