Unsoundness with floats

[LeventErkok]

@wintersteiger Not sure if this is the same issue as #6972

This benchmark:

(set-logic QF_FPBV)
(declare-fun s0 () RoundingMode)
(declare-fun s1 () (_ BitVec 8))
(define-fun s2 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) s0 s1))
(define-fun s3 () (_ BitVec 8) ((_ fp.to_sbv 8) s0 s2))
(define-fun s4 () Bool (= s1 s3))
(assert (not s4))
(check-sat)

is unsat, and z3 compiled 2 days ago answered it as unsat. But z3 compiled today says sat.

[wintersteiger]

No, it's not the same issue. This one is likely due to a fix in fp.to_sbv, which had previously suffered from an overflow type of problem for ages. Apparently, now it works for tiny 5-bit floats, but not for normally sized ones anymore.

[LeventErkok]

@wintersteiger I'm planning to do a release of an upstream tool, and wondering if I should hold off till you fix this issue.

If you're planning to fix this in a short-time frame then I'd rather hold-off on my side to make sure all is well. If it's going to take a while, that's perfectly fine as well. I can address this in a future release. Wanted to double check.

[LeventErkok]

As an additional note, it seems the problem only happens with fp.to_sbv, but not with fp.to_ubv. So, perhaps something is wrong with the signed-conversions only. I hope that helps narrow down the bug-hunt.

[wintersteiger]

Thanks for checking! Realistically this will take some time, but I can take a quick stab at it on the weekend to at least find out how much surgery is required.

I wouldn't have expected signed/unsigned to make a difference here, but maybe that's precisely why there's a bug :-)

[LeventErkok]

Thanks! Looking forward to hearing what you find out..

[wintersteiger]

Fixed! The previous "fix" was totally bogus, I must have been very tired when I added that.

[LeventErkok]

@wintersteiger Thanks for the quick turnaround! I can confirm this works just fine now.