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