[HACK_FIX] Using (get-model) breaks the logs

[JonasAlaif]

The following smt2 file, run through all z3 versions, results in a log which fails to parse the quantifier instantiation at the second assert:

(push)(pop) ; This switches to incremental, which makes the log cleaner?
(declare-fun f (Int) Bool)

(assert (forall ((i Int))
    (!  (not (f i))
        :pattern ((f i))
    )))

(check-sat)
(get-model)

(assert (f 0))
(check-sat)

The resulting log: z3.log. The issue is that z3 creates string and ident terms in a separate namespace for the (get-model) but fails to note this in the log. Thus the term IDs clash with the term ID for the quantifier, and when the later instantiation line refers to the quantifier by its ID we find a string term and not a quantifier.
Related z3 source code here.

[JonasAlaif]

This issue is due to a bug in z3.

Description

z3 creates terms for the string literals it will print for (get-model) and logs them as new terms in the logfile. See here. Internally in z3 these are likely in a different namespace/object, but in the logfile these terms appear as term IDs without a namespace (e.g. #13). The issue is that these IDs clash with existing terms which still exist and thus the "term ID" to TermIdx mapping is broken in our tool.

Hack fix

The only way to differentiate these "false" new terms is by their name. Therefore we do this and forbid the set of names z3 uses for these special terms in .smt2 files to avoid misidentifying user terms as these special ones. The special terms are still parsed (though they could also be ignored) but are given a new fake namespace.