Skip to content

Incorrect answer on QF_FP formula with fp.roundToIntegral and RoundingMode #3197

@muchang

Description

@muchang

Hi,
For this formula:

(declare-fun a () (_ FloatingPoint 2 10))
(declare-fun b () RoundingMode)
(assert (distinct (fp.roundToIntegral b (fp.roundToIntegral b a)) (fp.roundToIntegral b a)))
(check-sat)

Z3 incorrectly gives sat, while this formula should be unsat.

OS: Ubuntu 18.04
Commit: 7d976e4

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions