Suggest Z3 chose 8 or 16 bits for integers

This patch does not change the meaning of type constraints for integer types, but by calling out the 8- and 16-bit cases explicitly, it does seem to encourage Z3 to try larger types first.

A possible stop-gap until a better solution is found.

```
Precondition: true
  %a = sext %x to Ty
  %b = trunc %a
=>
  %a.1 = zext %x to Ty
  %b = trunc %a.1

Done: 15
ERROR: Mismatch in values of i8 %b

Example:
%x i7 = 64 (0x40)
%a i16 = 65472 (0xffc0)
%a.1 i16 = 64 (0x40)
Source value: 192 (0xc0)
Target value: 64 (0x40)

----------------------------------------
Optimization: two
Precondition: true
  %0 = sub 0, %a
  %r = sub nsw %x, %0
=>
  %r = add nsw %x, %a


ERROR: Domain of poisoness of Target is smaller than Source's for i16 %r

Example:
%a i16 = 32768 (0x8000)
%x i16 = 32768 (0x8000)
%0 i16 = 32768 (0x8000)
Source value: 0 (0x0)
Target value: poison

----------------------------------------
Optimization: 3
Precondition: (C > 0)
  %0 = add %x, C
  %r = icmp slt %x, %0
=>
  %r = true


ERROR: Mismatch in values of i1 %r

Example:
%x i8 = 61 (0x3d)
C i8 = 95 (0x5f)
%0 i8 = 156 (0x9c)
Source value: 0 (0x0)
Target value: 1 (0x1)
```