		Search-engine friendly clone of the ACL2 documentation.

Check-config

Assert-sat

Signature
(assert-sat formula &key (config 'config)) → *
Arguments: formula — Guard (lit-list-listp formula).; config — Guard (config-p config).

Definitions and Theorems

Function: assert-sat-fn

(defun assert-sat-fn (formula config)
  (declare (xargs :guard (and (lit-list-listp formula)
                              (config-p config))))
  (let ((__function__ 'assert-sat))
    (declare (ignorable __function__))
    (or (equal (simple-sat formula :config config)
               :sat)
        (raise "Expected formula ~x0 to be satisfiable!"
               formula))))