``` [607] % z3 small.smt2 unsat [608] % z3 rewriter.udiv2mul=true small.smt2 sat [609] % [609] % cat small.smt2 (declare-fun a () (_ BitVec 9)) (assert (let ((b (bvudiv ((_ zero_extend 7) a) (_ bv29487 16)))) (bvule (bvudiv b b) b))) (check-sat) [610] % ``` OS: Ubuntu 18.04 Commit: dd3e574