Spaces in :qid of quantifier produces problematic z3.log

[bobismijnnaam]

Hello, I have a problem with using spaces in the :qid attribute of quantifiers. Specifically, I think it might influence the logging output, as produced by trace=true proof=true. For example, the following input:

$ cat nopos.smt2
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)

(assert (forall ((i Int)) 
  (!(= (f i) (g (+ i 1))) 
  :pattern ((f i))
  :qid |oh no|)))

(assert (not (= (f 2) (g 3))))
(check-sat)
$ ~/Downloads/z3-4.8.17-x64-glibc-2.31/bin/z3 nopos.smt2 trace=true proof=true
unsat

Leads to an unescaped/unquoted qid in [mk-quant] entries, as below:

[mk-quant] #31 oh no 1 #30 #29

Complete z3.log output: z3.log. I used z3 4.8.17, but this is also present in at least 4.8.5. I'm not sure if z3 is violating a spec here, but I know that at least axiom profiler trips over this.

Maybe pipes around the name of [mk-quant] could be added to the z3 log format here, such that log parser can then detect when spaces are used? Or is the format of [mk-quant] fixed, i.e.:

[mk-quant] #number qid-possibly-with-spaces number #number #number

In that case, axiom profiler could maybe be enhanced to also parse this output. But then identifiers with multiple subsequent spaces might still be tricky to handle... In any case, I'd be very grateful for any help!