Optimization check never finishes

[chfast]

Hi there,

I wanted to use alive to verify an optimization but I know very little about how it works.

The optimization looks like:

Name: Mul128MatchLo
Pre: hasOneUse(%xl) && hasOneUse(%xh) && hasOneUse(%yl) && hasOneUse(%yh)
%xl = and i64 %X, 4294967295
%xh = lshr i64 %X, 32
%yl = and i64 %Y, 4294967295
%yh = lshr i64 %Y, 32
%mul = mul nuw i64 %xl, %yl
%and3 = and i64 %mul, 4294967295
%shr4 = lshr i64 %mul, 32
%mul5 = mul nuw i64 %yl, %xh
%add = add i64 %shr4, %mul5
%and7 = and i64 %add, 4294967295
%mul8 = mul nuw i64 %yh, %xl
%add9 = add i64 %and7, %mul8
%shl = shl i64 %add9, 32
%L = or i64 %shl, %and3
  =>
%L = mul i64 %X, %Y

It might be to heavy for Z3, because it looks like it hangs and does not report anything back. There is not Done: progress reported and it's impossible to terminate it with Ctrl+C.

[nunoplopes]

This is quite heavy for Z3 indeed. We could potentially have a progress bar, yes, though that's non-trivial at the moment.
In practice, the longer you run it, the higher the chances it is correct, since Z3 couldn't find a counterexample in that time.

[chfast]

I've seen in some examples the progress indicator Done: going from 1 to 63. Where can I find information what it means?
For my case, there is not even Done: 1 displayed.

[nunoplopes]

That indicates the progress through different bitwidths (1 to 64). Your example is of fixed bitwidth, so there's only 1 iteration of Alive to be done.

[regehr]

in practice, reducing bitwidth is often a good way to check an optimization like this.
in your case this isn't trivial since there are bitwidth-dependent constants, but even so that is likely to be the way to go here.