Soundness: sat query is answered unsat

[LeventErkok]

This query:

(set-logic ALL)
(declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
                                    ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
                                                  (proj_2_SBVTuple2 T2))))))
(define-fun s1 () (SBVTuple2 String (_ FloatingPoint  8 24))
                  (mkSBVTuple2 (_ char #x41) ((_ to_fp 8 24) roundNearestTiesToEven (/ 8514437.0 1048576.0))))

(declare-fun s0 () (SBVTuple2 String (_ FloatingPoint  8 24)))
(assert (= 1 (str.len (proj_1_SBVTuple2 s0))))
(define-fun s2 () Bool (= s0 s1))
(assert s2)
(check-sat)

produces unsat with a freshly compiled z3 from the master branch.

However, this query is actually satisfiable. If you run it with z3 from December 12, 2021; it successfully produces sat.

I've noticed that if I delete the last 3 lines, and replace them with:

(assert (= s0 s1))
(check-sat)

then z3 says sat with a correct model. So, something about that extra assignment to s2 is throwing it off.