smt2: fix bitwuzla invocation

[mattyoung101]

What are the reasons/motivation for this change?

Bitwuzla no longer shares options in common with Boolector. It now requires "--lang smt2" instead of "--smt2", and always runs incrementally by default (see: Bitwuzla news)

I found this because I'm using Bitwuzla 0.5.0-dev-main@69e4be28-dirty (through the AUR bitwuzla-git package), and it currently does not run correctly through eqy.

Explain how this is achieved.

smtio.py is modified to invoke Bitwuzla correctly, taking into account the fact it uses incremental solving by default

If applicable, please suggest to reviewers how they can test the change.

This should be testable by using any sby tools with Bitwuzla. I was using eqy and confirmed it worked with a very small testbench of mine (it's a bit hard to share because it's a Yosys plugin that generates the design on the fly).

[donn]

See YosysHQ/oss-cad-suite-build#87 (comment)

[mattyoung101]

Thanks for the link, unfortunately missed it when searching the issue tracker before making this PR. Do we know if the upstream Bitwuzla performance regression has been fixed? As I understand it, that was the main reason blocking oss-cad-suite from upgrading to a newer Bitwuzla? (edit: and possibly the Meson build system?)

[donn]

Honestly don't know, you and I are in the same boat- you could try running @jix's benchmark (it's downloadable)

[KrystalDelusion]

I clicked the button to run CI, although I suspect that the test-verific run which does run SBY tests will either fail because it's using the older version of Bitwuzla used in OSS CAD suite, or just pass without testing Bitwuzla specifically 😅

[mattyoung101]

@KrystalDelusion Looks like the CI pipeline has passed, although that probably does mean that Bitwuzla is not tested directly by the Verific tests 😅