Mode to make string literals revealed by default (and not require reveal_strlit)

[txiang61]

Why are string literals from the SMT encoding hidden by default?

error: assertion failed
   |
   |             assert(""@ == ""@ + ""@);
   |                    ^^^^^^^^^^^^^^^^ assertion failed

Which requires a reveal_strlit("") for the assert to prove. Can we add a mode for having it revealed by default so we can chose which one to have?

[utaal]

Thanks @txiang61: I've renamed this, and moved it to feature requests.

In brief, the reason for the string literals to be hidden by default is that we expect they will often appear in printing code, for example, where we may often not need to reason about them, so it is an unnecessary (performance) burden on the solver for it to have information on the strings' context.