Invalid model for QF_FP formula

[muchang]

Hi,
For this formula:

(define-sort FPN () (_ FloatingPoint 50 53))
(declare-fun a () FPN)
(declare-fun b () FPN)
(declare-fun c () FPN)
(assert (= (fp.add roundTowardPositive b a) c))
(check-sat)

Z3 gives an invalid model:

[634] % z3 model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
[635] % 
[635] % cat small.smt2
(define-sort FPN () (_ FloatingPoint 50 53))
(declare-fun a () FPN)
(declare-fun b () FPN)
(declare-fun c () FPN)
(assert (= (fp.add roundTowardPositive b a) c))
(check-sat)
[636] %

OS: Ubuntu 18.04
Commit: 9e7af79

[NikolajBjorner]

there are too many invalid model for FP open at this point. They are extremely likely to be duplicates. So I will just close newbies. You can append to the older bugs if you want.

[zhendongsu]

Okay, that makes sense, Nikolaj, but it would be nice to get them fixed as the first ones were reported quite a while ago. Thanks.

[NikolajBjorner]

Wintersteiger has no cycles for FP related work until mid May.
Z3 is open source and takes contributions such as bug fixes, so yes "it would be nice" and there is an even nicer way to ensure it happens.

[zhendongsu]

I appreciate the encouragement, Nikolaj :), but it's probably best to leave you folks to do the harder work, at least for now.

[martin-cs]

@zhendongsu : FWIW I am working on the equivalent issues for CVC4. Fixing them is a non-trivial amount of work and has very little pay-off as the vast majority of use-cases for the theory of floating-point use just a handful of formats. Completely agree that it would be nice but these are just not a high-priority issue until there is demand for (50 53) floats.

[martin-cs]

@zhendongsu : if you want to help, identifying the minimum number of formats / equivalence classes of format that exhibit unusual behaviour (for example, where sqrt can return subnormal numbers, subnormal range of exponents larger than normal, etc.) would make fixing these much easier.