Gl-assert
During GL symbolic execution, check that a condition holds, causing
an error if it does not.
(gl-assert x), logically speaking, just returns (if x t
nil). In concrete execution, it causes an error if x is false, and in
symbolic execution, it forces a check that x is true and produces a
counterexample if not.
Definitions and Theorems
Function: gl-assert-fn$inline
(defun gl-assert-fn$inline (x msg gmsg)
(declare (xargs :guard t) (ignore gmsg))
(mbe :logic (and x t)
:exec
(if x t
(er hard? 'gl-assert "~@0" msg))))
