ber <tt>2</tt>. When 
we evaluate <tt>x*2</tt>, we take the two <tt>SVals</tt> of the subexpressions, 
and create a new <tt>SVal</tt> that represents their multiplication (which in 
this case is a new symbolic expression, which we might call <tt>$1</tt>). When we 
evaluate the assignment to <tt>y</tt>, we again compute its lvalue (a <tt>MemRegion</tt>), 
and then bind the <tt>SVal</tt> for the RHS (which references the symbolic value <tt>$1</tt>) 
to the <tt>MemRegion</tt> in the symbolic store.
<br>
The se