Nuno Lopes
Still not fixed. Another test case from @regehr: ```llvm define i8 @src() { entry: %retval = alloca i32, align 4 %call = tail call i32* @c(i32* undef) %0 = load...
And another one: ```llvm define i32* @src() { %retval = alloca i32*, align 8 %v = load i32*, i32** %retval, align 8 ret i32* %v } define i32* @tgt() {...
Another nice one (unit/fpbitcast2.opt): ``` Name: NaN 2 %v = fdiv float 0.000000, 0.000000 %r = bitcast float %v to i32 ret i32 %r => %r = i32 2139095040 ret...
see also: https://github.com/AliveToolkit/alive2/issues/201
Only the last one from fpbitcast2 is still broken.
sure! should I take over #746 then?
yes, I think that would be very useful, but it's not urgent 😀 It has a bit that is not obvious is that it needs to account for SMT random...
that's the plan. We've already added support for dumping Z3 logs. So it's just a matter of running Alive2 with the right arguments and then spam your email while you...
are you averaging over how many random seeds?
I don't think there's any reason for a perf change judging from the Z3 commits msgs. One think to keep in mind is that Z3 is memory bound; it has...