Problems with common SMTLIB2 Strings for OpenSMT2 and Bitwuzla

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.

Apache License 2.0

186 stars 46 forks source link

Problems with common SMTLIB2 Strings for OpenSMT2 and Bitwuzla #372

Closed baierd closed 1 month ago

baierd commented 7 months ago

Both OpenSMT2 and Bitwuzla need the removal of certain parts of SMTLIB2 Strings before we can parse them. Examples are comments and set-logic. This is currently done lazily and incomplete. For example escape characters are not taken into account. We should ask for better support by the developers and/or improve our filtering (possibly by using the branch for the SMTLIB2 parser).

baierd commented 7 months ago

Progress for OpenSMT2 + tests in branch improve opensmt2 parsing

baierd commented 2 months ago

Whats the current state of this issue and what can we do? @daniel-raffler could you investigate please?