must-not-prove

(in-package "ACL2")

(defsection must-not-prove
  :parents (std/testing errors)
  :short "A top-level @(tsee assert$)-like command to ensure that
          a formula does not get proved."
  :long "<p>This takes the same arguments as @(tsee thm).
   It wraps the @(tsee thm) into a @(tsee must-fail).</p>

   @(def must-not-prove)"
  (defmacro must-not-prove
    (&rest args)
    `(must-fail (thm ,@ARGS))))