Skip to content

Commit

Permalink
Upgrade bitwuzla '0.6.1'
Browse files Browse the repository at this point in the history
  • Loading branch information
recoules committed Nov 14, 2024
1 parent 90fa035 commit 6642f7a
Show file tree
Hide file tree
Showing 5 changed files with 11 additions and 4 deletions.
7 changes: 7 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,10 @@
## 0.6.1 (2024-11-14)

Update [Bitwuzla](https://github.com/bitwuzla/bitwuzla/releases/tag/0.6.1) sources.

Vendor submodules:
- [Bitwuzla](https://github.com/bitwuzla/bitwuzla) tag:0.6.1

## 0.6.0 (2024-11-04)

Update [Bitwuzla](https://github.com/bitwuzla/bitwuzla/releases/tag/0.6.0) sources.
Expand Down
2 changes: 1 addition & 1 deletion bitwuzla-cxx.opam
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
version: "0.6.0"
version: "0.6.1"
synopsis: "SMT solver for AUFBVFP (C++ API)"
description: """

Expand Down
2 changes: 1 addition & 1 deletion dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
(generate_opam_files true)

(name bitwuzla-cxx)
(version 0.6.0)
(version 0.6.1)
(maintainers "Frédéric Recoules <[email protected]>")
(authors "Frédéric Recoules")
(source (github bitwuzla/ocaml-bitwuzla))
Expand Down
2 changes: 1 addition & 1 deletion vendor/bitwuzla
Submodule bitwuzla updated 91 files
+25 −5 NEWS.md
+26 −1 include/bitwuzla/cpp/bitwuzla.h
+1 −1 meson.build
+11 −0 src/api/cpp/bitwuzla.cpp
+0 −2 src/backtrack/assertion_stack.cpp
+0 −1 src/backtrack/assertion_stack.h
+0 −4 src/check/check_unsat_core.cpp
+0 −3 src/check/check_unsat_core.h
+15 −6 src/lib/bv/bitvector.cpp
+2 −2 src/lib/ls/ls.cpp
+11 −4 src/main/main.cpp
+16 −0 src/main/options.cpp
+2 −0 src/main/options.h
+0 −2 src/main/time_limit.cpp
+1 −0 src/meson.build
+0 −2 src/node/node.cpp
+1 −1 src/node/node.h
+12 −2 src/node/node_data.cpp
+8 −4 src/node/node_data.h
+0 −3 src/node/node_manager.h
+0 −1 src/node/node_unique_table.h
+5 −6 src/option/option.cpp
+0 −2 src/option/option.h
+8 −0 src/parser/smt2/parser.cpp
+2 −0 src/parser/smt2/symbol_table.cpp
+2 −0 src/parser/smt2/token.cpp
+2 −0 src/parser/smt2/token.h
+1 −1 src/preprocess/assertion_tracker.h
+0 −2 src/preprocess/pass/elim_extract.cpp
+0 −2 src/preprocess/pass/elim_lambda.cpp
+17 −4 src/preprocess/pass/elim_udiv.cpp
+13 −7 src/preprocess/pass/embedded_constraints.cpp
+2 −2 src/preprocess/pass/embedded_constraints.h
+0 −2 src/preprocess/pass/normalize.cpp
+0 −1 src/preprocess/pass/normalize.h
+0 −2 src/preprocess/pass/skeleton_preproc.cpp
+1 −1 src/preprocess/pass/skeleton_preproc.h
+0 −2 src/preprocess/pass/variable_substitution.h
+0 −2 src/preprocess/preprocessing_pass.cpp
+0 −1 src/preprocess/preprocessing_pass.h
+3 −1 src/preprocess/preprocessor.cpp
+30 −8 src/printer/printer.cpp
+46 −24 src/printer/printer.h
+0 −2 src/resource_terminator.cpp
+1 −4 src/rewrite/rewrites_array.cpp
+6 −5 src/rewrite/rewrites_bv.cpp
+0 −1 src/rewrite/rewrites_core.cpp
+5 −0 src/sat/kissat.cpp
+0 −1 src/sat/sat_solver.h
+3 −1 src/solver/abstract/abstraction_lemmas.h
+7 −4 src/solver/abstract/abstraction_module.cpp
+2 −1 src/solver/abstract/abstraction_module.h
+1 −3 src/solver/bv/bv_bitblast_solver.cpp
+0 −3 src/solver/bv/bv_bitblast_solver.h
+4 −2 src/solver/bv/bv_prop_solver.cpp
+0 −2 src/solver/bv/bv_prop_solver.h
+10 −11 src/solver/bv/bv_solver.cpp
+1 −1 src/solver/bv/bv_solver.h
+0 −5 src/solver/fp/fp_solver.cpp
+0 −2 src/solver/fp/symfpu_wrapper.cpp
+0 −3 src/solver/fp/word_blaster.cpp
+0 −1 src/solver/fp/word_blaster.h
+0 −1 src/solver/fun/fun_solver.h
+3 −0 src/solver/solver_engine.cpp
+0 −10 src/solver/solver_engine.h
+2 −1 src/solver/solver_state.cpp
+1 −1 src/solver/solver_state.h
+7 −3 src/solving_context.cpp
+0 −1 src/solving_context.h
+0 −1 src/type/type_data.cpp
+0 −1 src/type/type_manager.cpp
+41 −0 src/util/exceptions.h
+2 −0 src/util/logger.cpp
+0 −1 src/util/logger.h
+11 −0 src/util/printer.cpp
+22 −0 src/util/printer.h
+0 −2 src/util/statistics.h
+60 −0 src/util/util.cpp
+2 −52 src/util/util.h
+7 −0 test/regress/meson.build
+10 −0 test/regress/preprocess/elimudiv1.smt2
+9 −0 test/regress/preprocess/embedded1.smt2
+5 −0 test/regress/rewrite/bv/issue131.smt2
+5 −0 test/regress/rewrite/bv/issue134.smt2
+6 −0 test/regress/solver/abstract/eagerrefine1.smt2
+7 −0 test/regress/solver/abstract/murxla-67f411058e7b0ea7.min.smt2
+9 −0 test/regress/solver/abstract/unsatcore1.smt2
+57 −2 test/unit/api/test_api.cpp
+34 −20 test/unit/lib/bitvector/test_bv.cpp
+53 −18 test/unit/printer/test_printer.cpp
+3 −2 test/unit/rewrite/test_rewriter_bv.cpp
2 changes: 1 addition & 1 deletion vendor/dune
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
(foreign_library
(archive_name bitwuzla-utils)
(language cxx)
(names hash_pair logger printer resources statistics)
(names hash_pair logger printer resources statistics util)
(flags :standard -std=c++17 -I. -I.. -DNDEBUG)
(extra_deps ../../../.bitwuzla_tree)))
(subdir
Expand Down

0 comments on commit 6642f7a

Please sign in to comment.