Track names for witness terms in model (#8184)

Track names for witness terms in model (#8184)

This ensures that enough information is set to allow users to understand models with witness terms.

For example, for input:

(set-logic ALL)
(set-info :status sat)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)
(assert (= (str.len x) 999999999999999999999999))
(assert (= (str.len y) 999999999999999999999999))
(assert (= z (str.++ x y)))
(check-sat)
we now get:

sat
(
(define-fun x () String (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w1) ))
(define-fun y () String (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w0) ))
(define-fun z () String (str.++ (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w1) ) (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w0) )))
)