#3832 merge fix-intutils-ovf-bug:
- fix several crashes and miscompilation bugs all related to integer optimizations - add a simple z3 bounded model checker for integer traces, which checks that the optimized trace and the input trace behave identically - this operates on all unit tests in test_optimizeintbound also generates some random tests