Comment by pschanely

That's right! We pick different choose execution paths arbitrarily and accumulate constraints in an SMT solver as we go. It's implemented with special objects that look just like ints, strings, etc; this might help:

https://twitter.com/pschanely/status/1176151748844691456