testsmt/yinyang

Parser performance issues

Closed this issue · 1 comments

wintered commented

Experiments on larger formulas, e.g., QF_FP 40kB+ formulas with highly nested expressions exposed hotspots while parsing.

Actions:

  • Identify SMT-LIB formulas on which the parser times out
  • Profiling
  • Fix the hotspots
wintered commented

addressed in #24