Skip to content

SymFPU assertion failure during conversion from signed bit-vector. #2

@aniemetz

Description

@aniemetz

SymFPU fails with an assertion failure when converting a bit-vector of size 113 to a floating-point of sort Float128 with to_fp.
This can be triggered both with cvc5 and Bitwuzla.

cvc5 version/commit: af398235ef9f3a90999
SymFPU version/commit: 8fbe139 on cvc5 with working copy patch

cvc5 configure.sh options
debug --symfpu

Input file:

(set-logic ALL)
(assert (= (_ +zero 15 113) ((_ to_fp 15 113) RTZ #b01111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111)))
(check-sat)

Fails at rounder.h:330:
PRECONDITION(sigWidth >= targetSignificandWidth + 2);
with sigWidth = 114 and targetSignificandWidth = 113.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions