Nuno Lopes
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...
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.
Thanks Dave! I agree this is a bug; this predicate should ensure power-of-2 OR poison. Right now it's missing the "OR poison" part. This is a long discussion to have...
Another example: ``` %1 = and i32 7, %0 %2 = sub %0, %1 %3 = icmp ult %2, 16 br %3, label %true, label %false true: %4 = and...
Another one: ``` %X0 = add nsw %B, %i %X = mul %X0, %S %Y0 = add %B, %j %Y = mul %Y0, %S => %t0 = sub %j, %i...
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...
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.
upstreamed patch: https://github.com/pytorch/pytorch/pull/67018
I've investigated this issue and there's no way around it without change PyTorch itself. A python program may do `non_torchy_tensor.set_(tochy_tensor)`. If the torchy tensor isn't materialized, we won't store non_torchy_tensor...
This seems to be an issue with the POR optimization, as the src function sees one more pointer than tgt (the loaded ptr) and thus undef ranges over fewer ptrs...