undesirable poison in return value

[regehr]

attached is src/tgt pair that doesn't verify when we invoke like this:

alive-tv src.ll tgt.ll --tgt-is-asm --disable-poison-input --disable-undef-input 

the problem is that there's a call to g() that returns some poison. I was hoping that --disable-poison-input and/or --tgt-is-asm would prevent poison values from being introduced, but this doesn't seem to happen.

is this something that needs to be fixed on the Alive side?

one thing that I tried is to mark g()'s return value as noundef. after doing this, the refinement check succeeds, but I have do make the change both in the source and target, and that's something we're trying to avoid here.

the target code is from @katrinafyi's tool, extracted from the ARM semantics!

src.ll.txt
tgt.ll.txt

[regehr]

thanks for the quick fix!!!!