nunoplopes/alive — pull request #12 by davemenendez (2014-10-11 05:58:33+00:00)
Title: 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)
```