(check-sat-using smt) An invalid model bug in QF_FP

[muchang]

This bug has to be triggered with (check-sat-using smt), so I filed as a new bug.

[514] % z3release model_validate=true small.smt2 
sat
(error "line 4 column 20: an invalid model was generated")
(
 (define-fun b () Float16
  (_ +zero 5 11))
 (define-fun a () Float16
  (fp #b0 #b10000 #b0000001000))
)
unsat
[515] % cat small.smt2 
(declare-fun a () Float16)
(declare-fun b () Float16)
(assert (= b (fp.roundToIntegral RNE a) (fp #b0 #b10000 #b0000000000)))
(check-sat-using smt)
(get-model)
(reset)
(define-fun b () Float16 (_ +zero 5 11))
(define-fun a () Float16 (fp #b0 #b10000 #b0000001000))
(assert (= b (fp.roundToIntegral RNE a) (fp #b0 #b10000 #b0000000000)))
(check-sat-using smt)
[516] %

Commit: 0c93c7a

[wintersteiger]

Can't reproduce this anymore. Even with lots of random seeds, this always produces correct models for me. b == 0 definitely was a bad model at the time, but even for the same a I can't get that bad b anymore. Given the time at which this was submitted, I suspect that this was due to a bit-vector issue which has since been fixed.