Baier D.

While the bug is fixed for now, there are 2 problems with CVC5 that caused this problem. 1. `getSort()` sometimes returns null. 2. `Sort`s are not equal, while being equal....

Bitwuzla has several critical issues that need to be resolved before it can be merged: - Bitwuzla does not add `||` around symbol names with non valid characters. Example: `main::a`...

@kfriedberger could you review the model, especially the ValueAssignments for UFs and Arrays for me please? I would like some feedback for my implementation.

It seems like trivial Boolean based formulas are rewritten/simplified by Bitwuzla even if the option `BITWUZLA_OPT_REWRITE_LEVEL` is set to `no rewrites`. However, since dumping of formulas is currently being done...

Update on the symbol naming: if there is a space in a symbol name, we expect that the symbol name will be wrapped in `||` (similar to the `main::a` problem...

Update on the formula dump: I've added the "proper" printout (which adds all that is needed to parse it as SMTLIB2), but it still does fail in changing the symbol...

I've temporarily disabled the tests for quantifiers, FP and some singular ones for parsing/symbol names. Besides that, the PR is ready for review.

Quantifiers are now fixed and seem to work properly. Elimination is not possible because Bitwuzla does not support this feature.

I've published the new version 0.3.1 and updated our code for it. The only 2 issues are the parsing problem mentioned above and that we can't use formulas on stacks...

Formulas in the new version of Bitwutzla just released are now capable of being used thread independently. We should update our wrapper and code before merging this.