## Symbolic Execution of Models

But ACL2 is more than a programming language.

Initialize **x** to 5 and let **y** be **any legal value**.

Because ACL2 is a mathematical language, we can simplify the expression

(lookup 'z (mc (s 'mult 5 y) 29))

and get (+ y y y y y). This is **symbolic execution** because not all
of the parameters are known.