magic-fix

(in-package "SMT")

(include-book "xdoc/top" :dir :system)

(include-book "std/util/define" :dir :system)

(defsection smt-magic-fix
  :parents (verified)
  :short ""
  (define magic-fix
    ((type symbolp) (x t))
    (declare (ignore type))
    x)
  (in-theory (enable magic-fix))
  (in-theory (disable (:type-prescription magic-fix))))