Use smt::Real for partial order encoding and default to Z3
Add quadratic-size concurrency encoding
Create module for binary operations on Internal<T>
Fast constant propagation in commutative monoids