I have tested the parser on all SMT-LIB benchmark files of less than 100kb (321357 out of 363786) with a timeout of 5s. On these, the old parser (0645851) had 186 timeouts and the new parser (3fc85ec) had 99 timeouts. When setting the timeout to 30s, all files can be successfully parsed by the new parser while the old parser still has 17 timeouts.
Optimized parser: I optimized the parser as much as possible. The new parser is now 1.15x faster than the old parser. The antlr4 python runtime is known to be significantly slower than the Java antlr4 runtime. However, if we restrict parsing to files of less than 100kb this seems good enough for our use case since larger bug triggers may hardly be reducible by current program reducers and may also take the SMT solvers under test very long to solve.
Adjustment of current settings:
reject smt2 files of >20k and parser timeout of 30 secs
->
reject smt2 files of >100k and parser timeout of 30 secs
I have tested the parser on all SMT-LIB benchmark files of less than 100kb (321357 out of 363786) with a timeout of 5s. On these, the old parser (0645851) had 186 timeouts and the new parser (3fc85ec) had 99 timeouts. When setting the timeout to 30s, all files can be successfully parsed by the new parser while the old parser still has 17 timeouts.
Optimized parser: I optimized the parser as much as possible. The new parser is now 1.15x faster than the old parser. The antlr4 python runtime is known to be significantly slower than the Java antlr4 runtime. However, if we restrict parsing to files of less than 100kb this seems good enough for our use case since larger bug triggers may hardly be reducible by current program reducers and may also take the SMT solvers under test very long to solve.
Adjustment of current settings:
reject smt2 files of >20k and parser timeout of 30 secs
->
reject smt2 files of >100k and parser timeout of 30 secs