Bitwuzla issues when using a distinct solver for interpolation

When using Bitwuzla as main solver and another solver for interpolation, there are several problems. We get 4000+ exceptions when running the SV-COMP 25 set with all categories/specifications.

We need to document the sources of the exceptions and then delegate or investigate the problems.

Here is the html for the runs and the logfiles.

EDIT: Open issues

• Fix handling of quoted symbol names while parsing SMTLIB formulas (JavaSMT)
• Blacklist more SMTLIB keywords as variable/uf names and automatically escape all variable names that would be illegal (JavaSMT)
• Update JavaSMT in CPAchecker to a version that uses Bitwuzla 0.7.X or later