(smt.threads=2, proof=true) solution unsoundness on an instance with datatypes and define-funs-rec

[zhendongsu]

[597] % z3release small.smt2
unsat
[598] % z3release smt.threads=2 proof=true model_validate=true small.smt2
sat
[599] % cat small.smt2
(declare-datatypes ((D 0)) (((C))))
(define-funs-rec ((b ((a D)) Bool)) ((str.< "bb" "aa")))
(declare-fun e () D)
(assert (b e))
(check-sat)