SymFPU attempts to generate bit-vector of size 0 in fp.to_ubv of size 1.

[aniemetz]

SymFPU attempts to generate a bit-vector of size 0 when converting an FP to an unsigned bit-vector of size one. This can be triggered both in Bitwuzla and cvc5:

For bitwuzla/bitwuzla@9c79f32:

(set-option :global-declarations true)
(set-option :produce-unsat-cores true)
(check-sat-assuming ( (distinct (bvredand ((_ fp.to_sbv 45) RTP (_ -oo 8 24))) ((_ fp.to_ubv 1) RTP (_ -oo 8 24))) ))

Fails with

bitwuzla/src/bzlasort.c:406: bzla_sort_bv: Assertion `width > 0' failed.
[bitwuzla>main] CAUGHT SIGNAL 6                                                                        
unknown                                                                                                
Aborted (core dumped)                     

For cvc5/cvc5@6de9bb2:

(set-option :global-declarations true)
(set-option :produce-unsat-cores true)
(check-sat-assuming ( (distinct (bvredand ((_ fp.to_sbv 45) RTP (_ -oo 8 24))) (= #b1 ((_ fp.to_ubv 1) RTP (_ -oo 8 24))) )))

Fails with

(error "constant of size 0")

We found this issue with murxla/murxla@fbb70b9.
I have a patch that attempts to fix this, will submit a PR after my tests on SMT-LIB are done.