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.
