Potential performance issue of parser/symbol table

[rainoftime]

Hi, for this QF_UF instance (which consists of 32624 lines of declarations, and 1 line of assertion (assert true))

yy.txt

cvc4 4caca6f

time z3 xx.smt2
real    0m0.623s
user    0m0.572s
sys     0m0.040s

time cvc4 xx.smt2

real    0m12.241s
user    0m11.568s
sys     0m0.660s

[4tXJ7f]

What kind of machine are you running this on? How did you configure the build? A production build of commit 4caca6f processes the file in 0.35s on my Ryzen 7 1700, so it is significantly faster than your numbers. Z3 is still quite a bit faster than CVC4 on my machine but the slow parser is a known issue.