Update Bitwuzla to version 0.6.0

[daniel-raffler]

Hello everyone,
Bitwuzla has released a new version 0.6.0 yesterday and we should update our bindings. The new release adds support for quantification over array variables and a new abstraction module for abstracting bit-vector arithmetic operators. A full changelog can be found here.

This pull request updates the Bitwuzla version to 0.6.0 and fixes a minor bug when passing boolean arguments to the solver using the solver.bitwuzla.furtherOptions option. (This was needed to actually use the new option with --option solver.bitwuzla.furtherOptions="ABSTRACTION=1, ABSTRACTION_BV_SIZE=32")

@kfriedberger: Could you handle uploading the solver binaries please?

[kfriedberger]

lgtm. Well done.
I will compile and update Bitwuzla in the next days.

[daniel-raffler]

Here's a quick performance test for the new "abstraction" feature:

(The brown line is with abstractions enabled)

We may still add our own option to enable this, or possibly even turn it on by default. Bitwuzla offers a large number of different configuration options:

      abstraction(this,
                  Option::ABSTRACTION,
                  false,
                  "enable abstraction module",
                  "abstraction"),
      abstraction_bv_size(
          this,
          Option::ABSTRACTION_BV_SIZE,
          32,
          0,
          UINT64_MAX,
          "enable abstraction for bit-vector terms of given minimum size",
          "abstraction-bv-size"),
      abstraction_eager_refine(this,
                               Option::ABSTRACTION_EAGER_REFINE,
                               false,
                               "add all violated abstraction lemmas at once",
                               "abstraction-eager-refine"),
      abstraction_value_limit(this,
                              Option::ABSTRACTION_VALUE_LIMIT,
                              8,
                              0,
                              UINT64_MAX,
                              "value instantiation limit bv-size/<n> until "
                              "adding original term as refinement",
                              "abstraction-value-limit"),
      abstraction_value_only(this,
                             Option::ABSTRACTION_VALUE_ONLY,
                             false,
                             "only add value instantiations",
                             "abstraction-value-only"),
      abstraction_assert(this,
                         Option::ABSTRACTION_ASSERT,
                         false,
                         "assertion abstraction",
                         "abstraction-assert"),
      abstraction_assert_refs(this,
                              Option::ABSTRACTION_ASSERT_REFS,
                              100,
                              1,
                              UINT64_MAX,
                              "number of assertion refinements per check",
                              "abstraction-assert-refs"),
      abstraction_initial_lemmas(this,
                                 Option::ABSTRACTION_INITIAL_LEMMAS,
                                 false,
                                 "use initial lemma refinements only",
                                 "abstraction-initial-lemmas"),
      abstraction_inc_bitblast(this,
                               Option::ABSTRACTION_INC_BITBLAST,
                               false,
                               "incrementally bit-blast bvmul and bvadd",
                               "abstraction-inc-bitblast"),
      abstraction_bv_add(this,
                         Option::ABSTRACTION_BV_ADD,
                         false,
                         "term abstraction for bvadd",
                         "abstraction-bvadd"),
      abstraction_bv_mul(this,
                         Option::ABSTRACTION_BV_MUL,
                         true,
                         "term abstraction for bvmul",
                         "abstraction-bvmul"),
      abstraction_bv_udiv(this,
                          Option::ABSTRACTION_BV_UDIV,
                          true,
                          "term abstraction for bvudiv",
                          "abstraction-bvudiv"),
      abstraction_bv_urem(this,
                          Option::ABSTRACTION_BV_UREM,
                          true,
                          "term abstraction for bvurem",
                          "abstraction-bvurem"),
      abstraction_eq(this,
                     Option::ABSTRACTION_EQUAL,
                     false,
                     "term abstraction for =",
                     "abstraction-eq"),
      abstraction_ite(this,
                      Option::ABSTRACTION_ITE,
                      false,
                      "term abstraction for ite",
                      "abstraction-ite"),

However, it should to be enough to just enable it with ABSTRACTION=1 and then set the minimum bitvector size for abstraction with ABSTRACTION_BV_SIZE=XXX.