guard-theorem-no-simplify-dollar-tests

(in-package "ACL2")

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

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

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