Update Bitwuzla to version 0.7.X #427
Conversation
…IG headers where some exceptions were not properly caught
lib/native/source/libbitwuzla/src/org/sosy_lab/java_smt/solvers/bitwuzla/api/Bitwuzla.java
Show resolved
Hide resolved
The new test executes the new simplify-method, but simplification returns an identical term. It is unclear, whether or how far Bitwuzla modifies a term at all.
There was a problem hiding this comment.
looks good so far.
I will compile and test, then merge this.
With some inter-branch-merging, we can build the x64 and arm64 version of Bitwuzla, as given from #395 without publishing the binaries twice.
|
ModelTest and FloatingPointFormulaManagerTest seem to fail with the latest version of Bitwuzla. Reasons:
|
The solver partially returns constant nested expressions. We need to simplify them before conversion to Java type.
This reverts commit 874f5a4. The term simplification would work and satisfy the ModelTest, but it is too slow and quote memory-inefficient.
To avoid bugs, Bitwuzla disabled uncommon sizes for FP types. See bitwuzla/bitwuzla@c4085cc .
|
@daniel-raffler can you take a look at the fialing tests with model evaluation and report to the developers of Bitwuzla. Thanks. After fixing it, we can compile Bitwuzla again and merge this PR. |
I'll have a look at it tomorrow. Thanks for all your work so far! |
We used to set this option to 0 to completely disable rewriting of formulas, but this is now causing issues in some of the tests. Leaving the option at its default value (= fully rewriting) seems to solve the problem.
This only seems to be any issue when we use the option Should I still report this as a bug? It's probably OK for Bitwuzla to return the terms unsimplified when the option is set to zero, and I didn't see any other issues when just leaving it at its default value. Then again there might be some performance implications if we just always leave rewriting on. |
|
Thanks for the quick fix. Looks good. |
Hello,
this will update Bitwuzla to a version just past release 0.7.0. The upgrade is minor, but includes a bug fix for bitwuzla/bitwuzla#149 which is currently affecting CPAchecker when trying to use different solvers for interpolation and regular solving (see this issue).
We may still want to wait for #395 to be merged to avoid having to update our bindings twice.