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.