guard-theorem-no-simplify-tests

(in-package "ACL2")

(must-succeed* (defun foo
    (x)
    (if (consp x)
      (foo (cddr x))
      x))
  (assert-equal (guard-theorem-no-simplify 'foo nil (w state) t t)
    '(if (not (consp x))
      't
      (if (consp (cdr x))
        't
        (equal (cdr x) 'nil)))))

(must-succeed* (defun foo
    (x)
    (if (consp x)
      (foo (cddr x))
      x))
  (assert-event (mv-let (erp val)
      (magic-ev-fncall 'guard-theorem-no-simplify
        (list 'foo nil (w state) t t)
        state
        t
        t)
      (and (null erp)
        (equal val
          '(if (not (consp x))
            't
            (if (consp (cdr x))
              't
              (equal (cdr x) 'nil))))))))

(assert-equal (guard-theorem-no-simplify 'len nil (w state) t t)
  '(if (not (consp x))
    't
    (acl2-numberp (len (cdr x)))))

(assert-equal (guard-theorem-no-simplify 'binary-+ nil (w state) t t)
  ''t)