		Search-engine friendly clone of the ACL2 documentation.

Check-config

Assert-unsat

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

Definitions and Theorems

Function: assert-unsat-fn

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