Reads
Mining JIT Traces: Missing Optimizations with Z3