Support for integers larger than 64 bits

[rsas]

According to the comment in value.py

https://github.com/nunoplopes/alive/blob/master/value.py#L289

only integers up to 64 bits are supported. Consequently, I couldn't check for the following optimization that was produced when compiling LLVM:

Name: 1
Pre: Known(%6, false)
%0 = i64 %x1
%1 = and i64 18446744073709551612, %0
%2 = icmp eq i64 0, %1
%3 = i80 %x2
%4 = and i80 302231454903657293676544, %3
%5 = icmp eq i80 0, %4
%6 = or i1 %2, %5
  =>
%2 = false

Are there any fundamental reasons to not support >64 bit integers?

[nunoplopes]

The reason is that we currently have to check all bit-widths from 1 to 64. Increasing the upper bound will increase the running time of the tool. As a short-term hack, you can increase the value to, say, 128 bits.
We cannot provide a better solution in the short term, but we'll surely look into this issue in the next few months.

[nunoplopes]

BTW, your example will now work out of the box. If all variables are typed, we'll accept whatever bit-width and do the proof.

[rsas]

Thanks Nuno!