Unsoudness of fp.to_fp with sat.euf=true

[wintersteiger]

This is a simplified version of a problem reported in https://github.com/Z3Prover/z3/issues/4889.

This input:

...$ cat case_tactic.smt2
(declare-fun x () (_ FloatingPoint 11 53))
(declare-fun rm () RoundingMode)
(assert (= ((_ to_fp 11 53) rm (/ 1.0 2.0)) x))
(check-sat-using default)
(get-model)
(check-sat-using (then sat default))

produces:

...$ .../z3 model_validate=true case_tactic.smt2 tactic.default_tactic=smt sat.euf=true
sat
(
  (define-fun x () (_ FloatingPoint 11 53)
    (fp #b0 #b01111111110 #x0000000000000))
  (define-fun rm () RoundingMode
    roundNearestTiesToEven)
)
unsat

The model that the default tactic finds is correct (it means x == 0.5, which is right for any rounding mode). Adding (assert (= rm roundNearestTiesToEven)) does not change the result.

I can't imagine that the root cause of this is a buggy translation of to_fp to bit-vectors, I would find it more likely that there's some conceptual problem in theory_fpa.cpp.

Also, sat takes a whole bunch of time and then reports (sat "abort giveup") and I can imagine that it doesn't clean up properly and leaves some contradiction in the context. I have no idea how that tactic works though.

@NikolajBjorner any ideas?

[NikolajBjorner]

I can imagine that it doesn't clean up properly

I would also take this as starting assumption given that extracting clauses from sat.euf=true state is fresh. Therefore, I would not classify this as an fp bug.