Further relax what is considered a value in the model (#8095)

Further relax what is considered a value in the model (#8095)

Fixes #8094.

This makes it so that "value-like" terms can appear as subterms in other terms that are then subsequently also considered values. For example (str.++ (witness ((x String)) (= (str.len x) 1000)) "A") is now considered a value.

This also changes the default option for when to use witness terms for strings in models, based on some user feedback.