bitwuzla/bitwuzla

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”.

Bitwuzla

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, uninterpreted functions and their combinations.

If you are using Bitwuzla in your work, or if you incorporate it into software of your own, we invite you to send us a description and link to your project/software, so that we can link it as third party application on bitwuzla.github.io.

Website

More information about Bitwuzla is available at: https://bitwuzla.github.io

Documentation

Documentation for Bitwuzla is available at: https://bitwuzla.github.io/docs

Download

The latest version of Bitwuzla is available on GitHub: https://github.com/bitwuzla/bitwuzla

Build and Installation Instructions

Bitwuzla can be built on Linux and macOS. Windows support is planned and WIP.

For detailed build and installation instructions see docs/install.rst.

Citing Bitwuzla

A comprehensive system description of Bitwuzla was presented and published at CAV 2023. Please use the following Bibtex for citing Bitwuzla.

@inproceedings{DBLP:conf/cav/NiemetzP23,
  author       = {Aina Niemetz and
                  Mathias Preiner},
  editor       = {Constantin Enea and
                  Akash Lal},
  title        = {Bitwuzla},
  booktitle    = {Computer Aided Verification - 35th International Conference, {CAV}
                  2023, Paris, France, July 17-22, 2023, Proceedings, Part {II}},
  series       = {Lecture Notes in Computer Science},
  volume       = {13965},
  pages        = {3--17},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-37703-7\_1},
  doi          = {10.1007/978-3-031-37703-7\_1},
  timestamp    = {Fri, 21 Jul 2023 17:55:59 +0200},
  biburl       = {https://dblp.org/rec/conf/cav/NiemetzP23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Contributing

Please refer to our contributing guidelines.

bitwuzla's Issues

Crash with `CAUGHT SIGNAL 11`

First of all, thank you very much for making bitwuzla and boolector available!

I recently started adding support for these two solvers to our bounded model checking infrastructure for Chisel3 in the chiseltest library. Most of our tests work well, but one makes both bitwuzla and boolector crash with a similar error message:

((((m@0 [bitwuzla>main] CAUGHT SIGNAL 11
unknown
fish: Job 1, 'bitwuzla --incremental boolecto…' terminated by signal SIGSEGV (Address boundary error)

The SMT query looks like this:

(set-option :produce-models true)
(set-logic QF_ABV)
(push 1)
(define-fun m@0 () (Array (_ BitVec 2) (_ BitVec 8)) ((as const (Array (_ BitVec 2) (_ BitVec 8))) (_ bv0 8)))
(define-fun _resetCount@0 () Bool false)
(declare-fun reset@0 () Bool)
(declare-fun readAddr@0 () (_ BitVec 2))
(define-fun m.out_MPORT.addr@0 () (_ BitVec 2) readAddr@0)
(define-fun m.out_MPORT.data@0 () (_ BitVec 8) (select m@0 m.out_MPORT.addr@0))
(define-fun out@0 () (_ BitVec 8) m.out_MPORT.data@0)
(define-fun _T@0 () Bool (= out@0 (_ bv1 8)))
(define-fun _T_2@0 () Bool (not reset@0))
(define-fun _T_3@0 () Bool (not _T@0))
(define-fun _resetPhase@0 () Bool (not (bvuge (ite _resetCount@0 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assert@0 () Bool (not (=> _T_2@0 _T@0)))
(define-fun _resetActive@0 () Bool (=> _resetPhase@0 reset@0))
(define-fun m.out_MPORT.en@0 () Bool true)
(assert _resetActive@0)
(push 1)
(assert assert@0)
(check-sat)
(pop 1)
(define-fun m@1 () (Array (_ BitVec 2) (_ BitVec 8)) m@0)
(define-fun _resetCount@1 () Bool (ite _resetPhase@0 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _resetCount@0 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _resetCount@0))
(declare-fun reset@1 () Bool)
(declare-fun readAddr@1 () (_ BitVec 2))
(define-fun m.out_MPORT.addr@1 () (_ BitVec 2) readAddr@1)
(define-fun m.out_MPORT.data@1 () (_ BitVec 8) (select m@1 m.out_MPORT.addr@1))
(define-fun out@1 () (_ BitVec 8) m.out_MPORT.data@1)
(define-fun _T@1 () Bool (= out@1 (_ bv1 8)))
(define-fun _T_2@1 () Bool (not reset@1))
(define-fun _T_3@1 () Bool (not _T@1))
(define-fun _resetPhase@1 () Bool (not (bvuge (ite _resetCount@1 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assert@1 () Bool (not (=> _T_2@1 _T@1)))
(define-fun _resetActive@1 () Bool (=> _resetPhase@1 reset@1))
(define-fun m.out_MPORT.en@1 () Bool true)
(assert _resetActive@1)
(push 1)
(assert assert@1)
(check-sat)
(get-value (m@0))

Besides produce-models, the only other option I pass as a command line argument is --incremental.

Tool versions:

> bitwuzla --version
1.0-prereleas
> boolector --version
3.2.2

I am using pre-built binaries from oss-cad-suite.

Out Of Memory killer

Dear developers,

We recently faced an issue using Bitwuzla (+ CaDiCal if it matters) on complex formulas like this one: query.txt.
The process takes around ~1m30 to fill ~64GB of RAM before being killed by the operating system.

Being killed by OOM is an issue, even more when Bitwuzla is natively linked to the application with a binding because the latter has no chance to react.

• Is there a way for Bitwuzla to detect a very high memory consumption and return unknown before being killed?

• I have join a query example. If you have time, you may have a look to understand why the memory consumption is so high. For comparison, Z3 can run 2+ days without finding a solution but its memory consumption increase very slowly.

Regards,
Frédéric Recoules

Can someone answer this please?

Write a Python program to accept an integer number and display the digits at the ones, tens and hundreds place of that number.
For example, if the user enters 86421 then the output should be:

The digit at the ones place of 86421 is 1

The digit at the tens place of 86421 is 2

The digit at the hundreds place of 86421 is 4

expected '_' at 'Array'

Hi, Bitwuzla is giving me the error expected '_' at 'Array' for the code below, anything I'm missing? Maybe arrays are not supported in UFs?

(declare-fun _f_0 ((Array (_ BitVec 256) (_ BitVec 8))) (_ BitVec 256))

Cannot import pybitwuzla

Hi, I would like to use the python API of bitwuzla. However, after I follow steps showing on the Github main page (Building Bitwuzla with Python Bindings), I still cannot import the pybitwuzla model. I think I have successfully build it as after the make command, it shows Built target pybitwuzla.
Are there any extra steps required?

Thanks for you help!

Unsure how to generate all satisfying models

Hi!

I have a .btor with the following contents:

1 var 64
2 constd 6 18
3 sll 64 1 2
4 add 64 -1 3
5 constd 6 31
6 srl 64 4 5
7 xor 64 4 6
8 constd 64 21
9 mul 64 7 8
10 constd 6 11
11 srl 64 9 10
12 xor 64 9 11
13 constd 6 6
14 sll 64 12 13
15 add 64 12 14
16 constd 6 22
17 srl 64 15 16
18 xor 64 15 17
19 consth 64 ffffffff
20 and 64 19 18
21 consth 64 deadbeef
22 eq 1 20 21
23 root 1 22

I'd like to generate all possible satisfying assignments of the bitvector 1. If I call bitwuzla, I get:

$ bin/bitwuzla ~/chacha20/mowhash.btor -x --btor -m
sat
1 46d2694a4431f014

I tried using -i for incremental solving (which should be somehow related to finding all solutions, not just one), but it's not clear to me how this incremental mode works, I was unable to find documentation about it.

How, if at all possible, can I ask bitwuzla to generate all possible assignments of the bitvector 1?

Potential bug with `push` and `pop`

Uncovered while trying to add Bitwuzla to Rosette: emina/rosette#260

Given test.smt2:

(push 1)
(pop 1)
(push 1)
(push 1)
(pop 2)
(define-fun e0 () (_ BitVec 8) (_ bv10 8))
(declare-fun c1 () (_ BitVec 8))
(declare-fun c2 () (_ BitVec 8))
(define-fun e3 () (_ BitVec 8) (bvadd c1 c2))
(define-fun e4 () Bool (= e0 e3))
(assert e4)
(define-fun e5 () (_ BitVec 8) (_ bv20 8))
(define-fun e6 () (_ BitVec 8) (_ bv2 8))
(define-fun e7 () (_ BitVec 8) (bvmul e6 c2))
(define-fun e8 () (_ BitVec 8) (bvadd c1 e7))
(define-fun e9 () Bool (= e5 e8))
(assert e9)
(check-sat)
(get-model)
(push 1)
(define-fun e10 () (_ BitVec 8) (_ bv3 8))
(define-fun e11 () (_ BitVec 8) (bvmul e10 c1))
(define-fun e12 () (_ BitVec 8) (bvadd c2 e11))
(define-fun e13 () Bool (= e0 e12))
(assert e13)
(define-fun e14 () (_ BitVec 8) (_ bv21 8))
(define-fun e15 () (_ BitVec 8) (bvmul e6 c1))
(define-fun e16 () (_ BitVec 8) (bvadd e7 e15))
(define-fun e17 () Bool (= e14 e16))
(assert e17)
(check-sat)
(pop 1)
(check-sat)
(get-model)
(push 1)
(declare-fun c10 () Bool)
(assert c10)
(declare-fun c11 () Bool)
(define-fun e12 () Bool (not c11))
(assert e12)
(declare-fun c13 () Bool)
(assert c13)
(check-sat)
(get-model)
(pop 1)
(check-sat)
(get-model)

Output of bitwuzla -m < test.smt2:

sat
(
  (define-fun c1 () (_ BitVec 8) #b00000000)
  (define-fun c2 () (_ BitVec 8) #b00001010)
)
unsat
sat
(
  (define-fun c1 () (_ BitVec 8) #b00000000)
  (define-fun c2 () (_ BitVec 8) #b00001010)
)
sat
(
  (define-fun c1 () (_ BitVec 8) #b00000000)
  (define-fun c2 () (_ BitVec 8) #b00001010)
  (define-fun c10 () Bool true)
  (define-fun c11 () Bool false)
  (define-fun c13 () Bool true)
)
sat
[error] expected non-null object

Output of boolector -i -m < test.smt2:

sat
(
  (define-fun BTOR_5@c1 () (_ BitVec 8) #b00000000)
  (define-fun BTOR_5@c2 () (_ BitVec 8) #b00001010)
)
unsat
sat
(
  (define-fun BTOR_5@c1 () (_ BitVec 8) #b00000000)
  (define-fun BTOR_5@c2 () (_ BitVec 8) #b00001010)
)
sat
(
  (define-fun BTOR_5@c1 () (_ BitVec 8) #b00000000)
  (define-fun BTOR_5@c2 () (_ BitVec 8) #b00001010)
  (define-fun BTOR_8@c10 () Bool true)
  (define-fun BTOR_8@c11 () Bool false)
  (define-fun BTOR_8@c13 () Bool true)
)
sat
(
  (define-fun BTOR_5@c1 () (_ BitVec 8) #b00000000)
  (define-fun BTOR_5@c2 () (_ BitVec 8) #b00001010)
  (define-fun BTOR_8@c10 () Bool false)
  (define-fun BTOR_8@c11 () Bool false)
  (define-fun BTOR_8@c13 () Bool false)
)
(
  (define-fun BTOR_5@c1 () (_ BitVec 8) #b00000000)
  (define-fun BTOR_5@c2 () (_ BitVec 8) #b00001010)
  (define-fun BTOR_8@c10 () Bool false)
  (define-fun BTOR_8@c11 () Bool false)
  (define-fun BTOR_8@c13 () Bool false)
)

Any idea what's happening here? Thank you!

reference bitwuzla show undefined symbol error

Hi my friends, I referenced this project in the triton project. When I used import triton, the following error was prompted

triton.cpython-311-x86_64-linux-gnu.so: undefined symbol: _ZN4bzla9BitVector7from_siEmlb

This seems to make me generate a bitwuzla so file, but I followed the steps of the official website and only generated *.A file. How do I fix this error

Bitwuzla and Boolector conflicts

I have the following "multiple definition" errors when I try linking both Boolector and Bitwuzla at the same time. Is it possible to resolve these naming conflicts so that both solvers could be used?

/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlaopt.c.o): in function `clone_data_as_opt_help_ptr':
bzlaopt.c:(.text+0x60): multiple definition of `clone_data_as_opt_help_ptr'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btoropt.c.o):btoropt.c:(.text+0x60): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlarwcache.c.o): in function `hash_rw_cache_tuple':
bzlarwcache.c:(.text+0x0): multiple definition of `hash_rw_cache_tuple'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorrwcache.c.o):btorrwcache.c:(.text+0x0): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlarwcache.c.o): in function `compare_rw_cache_tuple':
bzlarwcache.c:(.text+0x30): multiple definition of `compare_rw_cache_tuple'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorrwcache.c.o):btorrwcache.c:(.text+0x30): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlaslvaigprop.c.o): in function `get_assignment_bv':
bzlaslvaigprop.c:(.text+0x600): multiple definition of `get_assignment_bv'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorslvaigprop.c.o):btorslvaigprop.c:(.text+0x510): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlaslvquant.c.o): in function `thread_terminate':
bzlaslvquant.c:(.text+0x10): multiple definition of `thread_terminate'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorslvquant.c.o):btorslvquant.c:(.text+0x10): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlaslvquant.c.o): in function `compute_var_deps':
bzlaslvquant.c:(.text+0x20e0): multiple definition of `compute_var_deps'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorslvquant.c.o):btorslvquant.c:(.text+0x2050): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlaslvquant.c.o): in function `mk_concrete_lambda_model':
bzlaslvquant.c:(.text+0x39a0): multiple definition of `mk_concrete_lambda_model'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorslvquant.c.o):btorslvquant.c:(.text+0x3680): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlaslvquant.c.o): in function `mk_concrete_ite_model':
bzlaslvquant.c:(.text+0x4070): multiple definition of `mk_concrete_ite_model'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorslvquant.c.o):btorslvquant.c:(.text+0x3d50): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlaslvquant.c.o): in function `thread_work':
bzlaslvquant.c:(.text+0x78a0): multiple definition of `thread_work'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorslvquant.c.o):btorslvquant.c:(.text+0x72a0): first defined here
/usr/bin/ld: /home/fedor/esbmc-fork/bitwuzla-release/lib/libbitwuzla.a(bzlaslvsls.c.o): in function `clone_data_as_sls_constr_data_ptr':
bzlaslvsls.c:(.text+0x4ff0): multiple definition of `clone_data_as_sls_constr_data_ptr'; /home/fedor/esbmc-fork/boolector-release/lib/libboolector.a(btorslvsls.c.o):btorslvsls.c:(.text+0x4ea0): first defined here

Some unit tests fail unless bitwuzla is built with assertions

I've tried this:

./configure.py --testing
cd build
meson compile
meson tesst

Some of the tests fail. The statistics show:

Ok:                 3763
Expected Fail:      0   
Fail:               10  
Unexpected Pass:    0   
Skipped:            0   
Timeout:            0 

In the test logs, the failures are all failed to die or died but not with expected error.

All the tests pass if we build with assertions. So it looks like the ASSERT_DEATH tests should
be skipped when assertions are disabled?

Is it possible to force output format in new version?

I'd like to force dec output format like in boolector with option -d.
BTOR_OPT_OUTPUT_NUMBER_FORMAT has no effect.

Compile errors from bitwuzla-bin package in opam-repository.

The following compile errors / warnings are generated in the opam repository CI for this package.
Platform Debian 12 x86_64 with OCaml 4.14 and 5.0.

# g++ -Wall -Wextra -O3 -DNDEBUG -fPIC -I../build -c ../src/reap.cpp
# make[1]: Leaving directory '/home/opam/.opam/5.0/.opam-switch/build/bitwuzla-bin.0.0.0/_build/default/vendor/cadical/build'
# In file included from ../src/lookahead.cpp:1:
# In constructor 'CaDiCaL::CubesWithStatus::CubesWithStatus(CaDiCaL::CubesWithStatus&&)',
#     inlined from 'CaDiCaL::CubesWithStatus CaDiCaL::Internal::generate_cubes(int, int)' at ../src/lookahead.cpp:391:12:
# ../src/internal.hpp:100:8: warning: 'cubes.CaDiCaL::CubesWithStatus::status' may be used uninitialized [-Wmaybe-uninitialized]
#   100 | struct CubesWithStatus {
#       |        ^~~~~~~~~~~~~~~
# ../src/lookahead.cpp: In member function 'CaDiCaL::CubesWithStatus CaDiCaL::Internal::generate_cubes(int, int)':
# ../src/lookahead.cpp:389:21: note: 'cubes' declared here
#   389 |     CubesWithStatus cubes;
#       |                     ^~~~~
# In file included from ../src/reap.cpp:1:
# ../src/reap.hpp:15:10: error: 'size_t' does not name a type
#    15 |   inline size_t size() {
#       |          ^~~~~~
# ../src/reap.hpp:5:1: note: 'size_t' is defined in header '<cstddef>'; did you forget to '#include <cstddef>'?
#     4 | #include <vector>
#   +++ |+#include <cstddef>
#     5 | 
# ../src/reap.hpp:23:3: error: 'size_t' does not name a type
#    23 |   size_t num_elements;
#       |   ^~~~~~
# ../src/reap.hpp:23:3: note: 'size_t' is defined in header '<cstddef>'; did you forget to '#include <cstddef>'?
# ../src/reap.hpp: In member function 'bool Reap::empty()':
# ../src/reap.hpp:12:13: error: 'num_elements' was not declared in this scope
#    12 |     return !num_elements;
#       |             ^~~~~~~~~~~~
# ../src/reap.cpp: In member function 'void Reap::release()':
# ../src/reap.cpp:16:3: error: 'num_elements' was not declared in this scope
#    16 |   num_elements = 0;
#       |   ^~~~~~~~~~~~
# ../src/reap.cpp: In constructor 'Reap::Reap()':
# ../src/reap.cpp:23:3: error: 'num_elements' was not declared in this scope
#    23 |   num_elements = 0;
#       |   ^~~~~~~~~~~~
# ../src/reap.cpp: In member function 'void Reap::push(unsigned int)':
# ../src/reap.cpp:45:3: error: 'num_elements' was not declared in this scope
#    45 |   num_elements++;
#       |   ^~~~~~~~~~~~
# ../src/reap.cpp: In member function 'unsigned int Reap::pop()':
# ../src/reap.cpp:113:7: error: 'num_elements' was not declared in this scope
#   113 |     --num_elements;
#       |       ^~~~~~~~~~~~
# ../src/reap.cpp: In member function 'void Reap::clear()':
# ../src/reap.cpp:126:3: error: 'num_elements' was not declared in this scope
#   126 |   num_elements = 0;
#       |   ^~~~~~~~~~~~
# make[1]: *** [makefile:34: reap.o] Error 1
# make: *** [makefile:3: all] Error 2



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build bitwuzla-bin 0.0.0
+- 
+- The following changes have been performed
| - install conf-cmake 1
| - install conf-g++   1.0
| - install conf-git   1.1
| - install conf-gmp   4
| - install dune       3.10.0
+- 
# Run eval $(opam env) to update the current shell environment

The former state can be restored with:
    /usr/bin/opam switch import "/home/opam/.opam/5.0/.opam-switch/backup/state-20230914011238.export"
[WARNING] OPAMCONFIRMLEVEL was ignored because CLI 2.0 was requested and it was introduced in 2.1.
[WARNING] OPAMCONFIRMLEVEL was ignored because CLI 2.0 was requested and it was introduced in 2.1.
"/usr/bin/env" "bash" "-c" "opam reinstall bitwuzla-bin.0.0.0;
        res=$?;
        test "$res" != 31 && exit "$res";
        export OPAMCLI=2.0;
        build_dir=$(opam var prefix)/.opam-switch/build;
        failed=$(ls "$build_dir");
        partial_fails="";
        for pkg in $failed; do
          if opam show -f x-ci-accept-failures: "$pkg" | grep -qF "\"debian-12\""; then
            echo "A package failed and has been disabled for CI using the 'x-ci-accept-failures' field.";
          fi;
          test "$pkg" != 'bitwuzla-bin.0.0.0' && partial_fails="$partial_fails $pkg";
        done;
        test "${partial_fails}" != "" && echo "opam-repo-ci detected dependencies failing: ${partial_fails}";
        exit 1" failed with exit status 1
2023-09-14 01:14.55: Job failed: Failed: Build failed
2023-09-14 01:14.55: Log analysis:
2023-09-14 01:14.55: >>> 
[ERROR] The compilation of bitwuzla-bin.0.0.0 failed at "dune build -p bitwuzla-bin -j 47 @install".
 (score = 20)
2023-09-14 01:14.55: >>> 
# ../src/reap.hpp:15:10: error: 'size_t' does not name a type
 (score = 30)
2023-09-14 01:14.55: >>> 
# ../src/reap.hpp:23:3: error: 'size_t' does not name a type
 (score = 30)
2023-09-14 01:14.55: >>> 
# ../src/reap.hpp:12:13: error: 'num_elements' was not declared in this scope
 (score = 30)
2023-09-14 01:14.55: >>> 
# ../src/reap.cpp:16:3: error: 'num_elements' was not declared in this scope
 (score = 30)
2023-09-14 01:14.55: >>> 
# ../src/reap.cpp:23:3: error: 'num_elements' was not declared in this scope
 (score = 30)
2023-09-14 01:14.55: >>> 
# ../src/reap.cpp:45:3: error: 'num_elements' was not declared in this scope
 (score = 30)
2023-09-14 01:14.55: >>> 
# ../src/reap.cpp:113:7: error: 'num_elements' was not declared in this scope
 (score = 30)
2023-09-14 01:14.55: >>> 
# ../src/reap.cpp:126:3: error: 'num_elements' was not declared in this scope
 (score = 30)
2023-09-14 01:14.55: 'size_t' does not name a type

Full logs available at https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/e4ab39cf1252709989554bf19c88b572a43bf624.

`define-const` not supported?

Hi! Just tried the following example

(define-const a Int 2)
(check-sat)

but getting

$ bitwuzla --smt2 a.smt2
bitwuzla: a.smt2:1:2: expected command at 'define-const'

Anything I should be doing differently or is define-const not supported?

SymFPU attempts to generate bit-vector of size 0 in fp.to_ubv of size 1.

This is a SymFPU issue (martin-cs/symfpu#8), not a Bitwuzla issue, submitted to keep track of this problem.
This also fails in cvc5 (cvc5/cvc5-projects#531).

Bitwuzla 9c79f32
Found with murxla/murxla@fbb70b9

SymFPU attempts to generate a bit-vector of size 0 when converting an FP to an unsigned bit-vector of size one with:

(set-option :global-declarations true)
(set-option :produce-unsat-cores true)
(check-sat-assuming ( (distinct (bvredand ((_ fp.to_sbv 45) RTP (_ -oo 8 24))) ((_ fp.to_ubv 1) RTP (_ -oo 8 24))) ))

Fails with

bitwuzla/src/bzlasort.c:406: bzla_sort_bv: Assertion `width > 0' failed.
[bitwuzla>main] CAUGHT SIGNAL 6                                                                        
unknown                                                                                                
Aborted (core dumped)                     

Set RUNPATH when installing into custom dir given by --prefix

As is customly done, Bitwuzla's configure.py script allows installing into a non-standard location via --prefix. It will also install a pkg-config file bitwuzla.pc in there. For ESBMC I'm using this setup with Bitwuzla installed into a custom directory, but due to libbitwuzla.so linking to the other libs without providing a RUNPATH entry to find them, I'm getting

src/esbmc/esbmc: error while loading shared libraries: libbitwuzlabb.so: cannot open shared object file: No such file or directory

See also esbmc/esbmc#1302.

Over at Meson, in mesonbuild/meson#4027 (comment) (the issue has been fixed in v0.55) I've seen that it seems that it might be possible to include -Wl,-rpath,${libdir} or similar into the pkg-config file and I'm wondering whether that would be a viable approach for the configure script to do when Bitwuzla is being installed into a custom prefix.

If not, please feel free to close this issue and we'll try to deal with it on our side somehow.

"Quantifiers support is disabled"

Today I tried using bitwuzla_mk_var and BITWUZLA_KIND_EXISTS for the first time, in the context of some simple FP expressions.

When I tried to run bitwuzla, it said:

[bzlacore] bzla_check_sat: Quantifiers support is disabled.

changing BITWUZLA_OPT_ENGINE to "quant" didn't seem to help.

So, I am wondering, how can I enable quantifiers support?

Solving limits

Hi!

Is there a way to specify timeout and memory limit for query?

Build issue on MacOS with clang++ 16.0.6

[39/66] Compiling C++ object src/libbitwuzla.a.p/solver_bv_bv_prop_solver.cpp.o
FAILED: src/libbitwuzla.a.p/solver_bv_bv_prop_solver.cpp.o 
c++ -Isrc/libbitwuzla.a.p -Isrc -I../src -I../include -Isrc/lib -I../src/lib -Isubprojects/symfpu -I../subprojects/symfpu -Isubprojects/cadical-rel-1.5.2/src -I../subprojects/cadical-rel-1.5.2/src -Isubprojects/symfpu/symfpu/core -Isubprojects/symfpu/symfpu/utils -I/usr/local/Cellar/gmp/6.2.1_1/include -fcolor-diagnostics -DNDEBUG -Wall -Winvalid-pch -Wextra -Wpedantic -std=c++17 -O3 -MD -MQ src/libbitwuzla.a.p/solver_bv_bv_prop_solver.cpp.o -MF src/libbitwuzla.a.p/solver_bv_bv_prop_solver.cpp.o.d -o src/libbitwuzla.a.p/solver_bv_bv_prop_solver.cpp.o -c ../src/solver/bv/bv_prop_solver.cpp
../src/solver/bv/bv_prop_solver.cpp:278:21: error: conditional expression is ambiguous; 'std::__1::optional<std::__1::reference_wrapper<const std::__1::basic_string<char> > >::value_type' (aka 'std::__1::reference_wrapper<const std::__1::basic_string<char> >') can be converted to 'basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >' and vice versa
      node.symbol() ? *node.symbol() : "@t" + std::to_string(node.id());
                    ^ ~~~~~~~~~~~~~~   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1 error generated.

clang++ verison:

Homebrew clang version 16.0.6
Target: x86_64-apple-darwin20.6.0
Thread model: posix
InstalledDir: /usr/local/Cellar/llvm/16.0.6/bin

I can fix it with this patch:

diff --git a/src/solver/bv/bv_prop_solver.cpp b/src/solver/bv/bv_prop_solver.cpp
index 64d189d3..78004136 100644
--- a/src/solver/bv/bv_prop_solver.cpp
+++ b/src/solver/bv/bv_prop_solver.cpp
@@ -275,7 +275,7 @@ BvPropSolver::mk_node(const Node& node)
   }
 
   std::string symbol =
-      node.symbol() ? *node.symbol() : "@t" + std::to_string(node.id());
+      node.symbol() ? (*node.symbol()).get() : "@t" + std::to_string(node.id());
 
   switch (node.kind())
   {

Parser quietly failing

Hello, i upgraded to the newest bitwuzla version and the parser seems to quietly fail for certain cases.

I was not able to pin point exactly what causes the error but a small example that seems to reproduce the problem would be:

(set-logic QF_ABV)
(declare-fun a () (_ BitVec 1))
(declare-fun b () (_ BitVec 1))
(declare-fun c () (_ BitVec 1))
(declare-fun d () (_ BitVec 1))

(assert (= #b1 (bvnot (ite (= (concat (bvxor (bvor (bvand a c) (bvand b (bvnot c))) (bvand (bvxor c d) c)) (bvnot (bvxor c d))) (bvsub (concat a c) (concat b d))) (_ bv1 1) (_ bv0 1)))))

(check-sat)

If i paste this into a file and run bitwuzla -p <input_file> i get the following output:
(set-logic ALL) (check-sat) (exit)

I do not get an error an using the cpp parser interface also returns an empty error message string.

get-value of array: unknown symbol `uf1`

When I try to get-value an array in the following SMT query, the result contains symbol uf1 which was never defined in the query:

((m@0 (store uf1 #b11111 #b11111110)))

If I add a (get-value (uf1)), bitwuzla reports undefined symbol 'uf1' as expected.

(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun m@0 () (Array (_ BitVec 5) (_ BitVec 8)))
(declare-fun m_readValue_data_pipe_0@0 () (_ BitVec 8))
(declare-fun _cycles@0 () Bool)
(declare-fun m_readValue_do_rand_r1@0 () Bool)
(declare-fun out_1@0 () (_ BitVec 8))
(define-fun _resetCount@0 () Bool false)
(declare-fun reset@0 () Bool)
(declare-fun writeAddr@0 () (_ BitVec 5))
(declare-fun readAddr@0 () (_ BitVec 5))
(declare-fun in@0 () (_ BitVec 8))
(declare-fun m_readValue_rand_data@0 () (_ BitVec 8))
(define-fun m.readValue.addr@0 () (_ BitVec 5) readAddr@0)
(define-fun m.readValue.data@0 () (_ BitVec 8) (select m@0 m.readValue.addr@0))
(define-fun _cycles_active@0 () Bool (not (bvuge (ite _cycles@0 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun _after_1@0 () Bool (not _cycles_active@0))
(define-fun _GEN_1@0 () Bool true)
(define-fun m_readValue_rand_data.en@0 () Bool m_readValue_do_rand_r1@0)
(define-fun _T@0 () Bool (= readAddr@0 writeAddr@0))
(define-fun _T_2@0 () Bool (not reset@0))
(define-fun _T_3@0 () Bool (not _T@0))
(define-fun out@0 () (_ BitVec 8) (ite m_readValue_do_rand_r1@0 m_readValue_rand_data@0 m_readValue_data_pipe_0@0))
(define-fun _T_4@0 () Bool (= out@0 out_1@0))
(define-fun _T_7@0 () Bool (not _T_4@0))
(define-fun _resetPhase@0 () Bool (not (bvuge (ite _resetCount@0 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assume@0 () Bool (=> _T_2@0 _T@0))
(define-fun assert@0 () Bool (not (=> (and _T_2@0 _after_1@0) _T_4@0)))
(define-fun _resetActive@0 () Bool (=> _resetPhase@0 reset@0))
(define-fun m.readValue.en@0 () Bool true)
(define-fun m.MPORT.en@0 () Bool true)
(define-fun m.MPORT.addr@0 () (_ BitVec 5) writeAddr@0)
(define-fun m.MPORT.mask@0 () Bool true)
(define-fun m.MPORT.data@0 () (_ BitVec 8) in@0)
(assert assume@0)
(assert _resetActive@0)
(define-fun m@1 () (Array (_ BitVec 5) (_ BitVec 8)) (ite (and m.MPORT.en@0 m.MPORT.mask@0) (store m@0 m.MPORT.addr@0 m.MPORT.data@0) m@0))
(define-fun m_readValue_data_pipe_0@1 () (_ BitVec 8) (ite true m.readValue.data@0 m_readValue_data_pipe_0@0))
(define-fun _cycles@1 () Bool (ite reset@0 false (ite _cycles_active@0 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _cycles@0 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _cycles@0)))
(define-fun m_readValue_do_rand_r1@1 () Bool (not _GEN_1@0))
(define-fun out_1@1 () (_ BitVec 8) in@0)
(define-fun _resetCount@1 () Bool (ite _resetPhase@0 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _resetCount@0 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _resetCount@0))
(declare-fun reset@1 () Bool)
(declare-fun writeAddr@1 () (_ BitVec 5))
(declare-fun readAddr@1 () (_ BitVec 5))
(declare-fun in@1 () (_ BitVec 8))
(declare-fun m_readValue_rand_data@1 () (_ BitVec 8))
(define-fun m.readValue.addr@1 () (_ BitVec 5) readAddr@1)
(define-fun m.readValue.data@1 () (_ BitVec 8) (select m@1 m.readValue.addr@1))
(define-fun _cycles_active@1 () Bool (not (bvuge (ite _cycles@1 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun _after_1@1 () Bool (not _cycles_active@1))
(define-fun _GEN_1@1 () Bool true)
(define-fun m_readValue_rand_data.en@1 () Bool m_readValue_do_rand_r1@1)
(define-fun _T@1 () Bool (= readAddr@1 writeAddr@1))
(define-fun _T_2@1 () Bool (not reset@1))
(define-fun _T_3@1 () Bool (not _T@1))
(define-fun out@1 () (_ BitVec 8) (ite m_readValue_do_rand_r1@1 m_readValue_rand_data@1 m_readValue_data_pipe_0@1))
(define-fun _T_4@1 () Bool (= out@1 out_1@1))
(define-fun _T_7@1 () Bool (not _T_4@1))
(define-fun _resetPhase@1 () Bool (not (bvuge (ite _resetCount@1 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assume@1 () Bool (=> _T_2@1 _T@1))
(define-fun assert@1 () Bool (not (=> (and _T_2@1 _after_1@1) _T_4@1)))
(define-fun _resetActive@1 () Bool (=> _resetPhase@1 reset@1))
(define-fun m.readValue.en@1 () Bool true)
(define-fun m.MPORT.en@1 () Bool true)
(define-fun m.MPORT.addr@1 () (_ BitVec 5) writeAddr@1)
(define-fun m.MPORT.mask@1 () Bool true)
(define-fun m.MPORT.data@1 () (_ BitVec 8) in@1)
(assert assume@1)
(assert _resetActive@1)
(define-fun m@2 () (Array (_ BitVec 5) (_ BitVec 8)) (ite (and m.MPORT.en@1 m.MPORT.mask@1) (store m@1 m.MPORT.addr@1 m.MPORT.data@1) m@1))
(define-fun m_readValue_data_pipe_0@2 () (_ BitVec 8) (ite true m.readValue.data@1 m_readValue_data_pipe_0@1))
(define-fun _cycles@2 () Bool (ite reset@1 false (ite _cycles_active@1 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _cycles@1 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _cycles@1)))
(define-fun m_readValue_do_rand_r1@2 () Bool (not _GEN_1@1))
(define-fun out_1@2 () (_ BitVec 8) in@1)
(define-fun _resetCount@2 () Bool (ite _resetPhase@1 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _resetCount@1 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _resetCount@1))
(declare-fun reset@2 () Bool)
(declare-fun writeAddr@2 () (_ BitVec 5))
(declare-fun readAddr@2 () (_ BitVec 5))
(declare-fun in@2 () (_ BitVec 8))
(declare-fun m_readValue_rand_data@2 () (_ BitVec 8))
(define-fun m.readValue.addr@2 () (_ BitVec 5) readAddr@2)
(define-fun m.readValue.data@2 () (_ BitVec 8) (select m@2 m.readValue.addr@2))
(define-fun _cycles_active@2 () Bool (not (bvuge (ite _cycles@2 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun _after_1@2 () Bool (not _cycles_active@2))
(define-fun _GEN_1@2 () Bool true)
(define-fun m_readValue_rand_data.en@2 () Bool m_readValue_do_rand_r1@2)
(define-fun _T@2 () Bool (= readAddr@2 writeAddr@2))
(define-fun _T_2@2 () Bool (not reset@2))
(define-fun _T_3@2 () Bool (not _T@2))
(define-fun out@2 () (_ BitVec 8) (ite m_readValue_do_rand_r1@2 m_readValue_rand_data@2 m_readValue_data_pipe_0@2))
(define-fun _T_4@2 () Bool (= out@2 out_1@2))
(define-fun _T_7@2 () Bool (not _T_4@2))
(define-fun _resetPhase@2 () Bool (not (bvuge (ite _resetCount@2 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assume@2 () Bool (=> _T_2@2 _T@2))
(define-fun assert@2 () Bool (not (=> (and _T_2@2 _after_1@2) _T_4@2)))
(define-fun _resetActive@2 () Bool (=> _resetPhase@2 reset@2))
(define-fun m.readValue.en@2 () Bool true)
(define-fun m.MPORT.en@2 () Bool true)
(define-fun m.MPORT.addr@2 () (_ BitVec 5) writeAddr@2)
(define-fun m.MPORT.mask@2 () Bool true)
(define-fun m.MPORT.data@2 () (_ BitVec 8) in@2)
(assert assume@2)
(assert _resetActive@2)
(assert assert@2)
(check-sat)
(get-value (m@0))
(get-value (uf1))

Internal model name prefixes leaking

The following smt file[1] has the output[2] when I expect the output[3].

[1]

(set-info :smt-lib-version 2.6)
(set-option :produce-models true)
(set-option :global-declarations true)
(set-logic QF_BV)

(push 1)
(declare-fun a () (_ BitVec 32))
(assert (= a (_ bv0 32)))
(check-sat)
(get-model)

[2]

sat
(model
  (define-fun BTOR_1@a () (_ BitVec 32) #b00000000000000000000000000000000)
)

[3]

sat
(model
  (define-fun a () (_ BitVec 32) #b00000000000000000000000000000000)
)

Mallob Support

Hi there (sorry I sent the issue too early), I am interested in adding support for Mallob as a backend to Bitwuzla. Mallob has an IPASIR interface bridge, and multiple (incremental) SAT formulae can be solved at the same time with a single running instance of Mallob.

Is this something you are generally interested in merging? If so, should I add a generic IPASIR interface to Bitwuzla, or should I rather implement a Mallob-specific interface (then perhaps with a few more specialized methods)?

Solution unsoundness on a BV formula

Commit: f53625a
OS: Ubuntu 20.04
File: bug.txt

$ bitwuzla -i bug.txt
sat
$ boolector -i bug.txt
unsat
$ z3 bug.txt
unsat
$ cvc5 --lang=smt2 bug.txt
unsat
$ mathsat bug.txt
unsat

Assertion fails at bitwuzla/src/bzlafp.cpp:728

Hi,
For this following instance, bitwuzla 1230d80 debug build

$ bitwuzla small.smt2
bitwuzla: /home/bitwuzla/src/bzlafp.cpp:728: static void BzlaFPTraits::invariant(const bool&): Assertion `p' failed.
[bitwuzla>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)
$ cat small.smt2
(assert ((fp (_ bv0 1) (_ bv0 3) (_ bv0 2))))

[Feature request] add option to disable default value filtering in array model

Dear developers,

Would it be possible to add a new option to disable the optimization that filter out the entries that are equal to the default value in array model?

It should be "as simple as" checking the option before setting the flag has_default_value in recursively_compute_function_model.

bitwuzla/src/bzlamodel.c

Line 368 in 3ea759d

has_default_value = true;

It is because in our use case, the symbolic indexes that are addressed are as important that the stored value itself.
And since bitwuzla already has this information and make some efforts to filter them while we have to make some efforts to get this information back, it would be smarter to just keep it at the source.

Regards,
Frédéric

const-ness of bitwuzla_mk_term "args"

This is a very minor request, but I think the header definition of bitwuzla_mk_term() should be changed to have its last argument changed to be const, i.e. "const BitwuzlaTerm *args[]"

How do I set a timeout limit for bitwuzla？

Boolector vs Bitwuzla

Hi,

I was running some experiment to replace boolector by bitwuzla in our symbolic execution engine and I found that boolector is consistently faster than bitwuzla. The formulas generated are QF_ABV (because we do not need UF and do not support FP yet).

I would not generalize it (the experiments are too small with not enough variety), but here is a set of formulas (smt2.zip) for which bitwuzla takes in average 20% more time than boolector on my computer.

I ran the following script to confirm my observation:

#!/bin/bash
for i in $(seq 1 10); do
    for f in $(ls xx*); do
	$1 -m -x -i < $f
    done
done

time ./run.sh boolector > /dev/null

real	1m28,656s
user	1m24,222s
sys	0m4,498s

time ./run.sh bitwuzla > /dev/null

real	1m46,321s
user	1m41,050s
sys	0m5,340s

I used boolector tag 3.2.2 and bitwuzla 95fb736.

@aniemetz @mpreiner @arminbiere Do you know from where it could come from?

Build fail when "./contrib/setup-symfpu.sh"

Hi,

The error log are listed below.

Cloning into '/home/zhangxd/bitwuzla/deps/symfpu'...
remote: Enumerating objects: 136, done.
remote: Total 136 (delta 0), reused 0 (delta 0), pack-reused 136
Receiving objects: 100% (136/136), 116.60 KiB | 0 bytes/s, done.
Resolving deltas: 100% (67/67), done.
Checking connectivity... done.
Note: checking out '8fbe139bf0071cbe0758d2f6690a546c69ff0053'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by performing another checkout.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -b with the checkout command again. Example:

git checkout -b

HEAD is now at 8fbe139... Avoid an overflow in roundToIntegral in obscure formats, fix CVC4 bug 2932

This may be because there is not such a commitment.

Yours,

Segmentation fault and heap-buffer-overflow at /src/parser/bzlasmt2.c:1737

Hi, for this non-standard instance, bitwuzla f834fc4 (debug build)

$ cat delta.smt2
(assert (/ 1 0))
$ bitwuzla delta.smt2
[bitwuzla>main] CAUGHT SIGNAL 11
unknown
Segmentation fault (core dumped)
$ bitwuzla-asan delta.smt2
=================================================================
==12144==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x602000006e28 at pc 0x7f2cb587afa0 bp 0x7ffc2f3dcc10 sp 0x7ffc2f3dcc00
READ of size 8 at 0x602000006e28 thread T0
    #0 0x7f2cb587af9f in item2str_smt2 /root/bitwuzla/src/parser/bzlasmt2.c:1737
    #1 0x7f2cb58901a4 in parse_term_aux_smt2 /root/bitwuzla/src/parser/bzlasmt2.c:4795
    #2 0x7f2cb5890478 in parse_term_smt2 /root/bitwuzla/src/parser/bzlasmt2.c:4815
    #3 0x7f2cb589f443 in read_command_smt2 /root/bitwuzla/src/parser/bzlasmt2.c:5895
    #4 0x7f2cb58a195f in parse_smt2_parser /root/bitwuzla/src/parser/bzlasmt2.c:6113
    #5 0x7f2cb55def69 in parse_aux /root/bitwuzla/src/bzlaparse.c:67
    #6 0x7f2cb55e2457 in bzla_parse /root/bitwuzla/src/bzlaparse.c:270
    #7 0x7f2cb580a847 in bitwuzla_parse /root/bitwuzla/src/api/c/bitwuzla.c:3407
    #8 0x55c8f8f7a69c in bitwuzla_main /root/bitwuzla/src/bzlamain.c:1563
    #9 0x55c8f8f6faec in main /root/bitwuzla/src/bitwuzlamain.c:18
    #10 0x7f2cb50eb0b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)
    #11 0x55c8f8f6fa0d in _start (/root/bitwuzla/build/bin/bitwuzla+0x6a0d)

0x602000006e28 is located 8 bytes to the left of 2-byte region [0x602000006e30,0x602000006e32)
allocated by thread T0 here:
    #0 0x7f2cb5c5d808 in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:144
    #1 0x7f2cb58f49f4 in bzla_mem_malloc /root/bitwuzla/src/utils/bzlamem.c:74
    #2 0x7f2cb58f5222 in bzla_mem_strdup /root/bitwuzla/src/utils/bzlamem.c:167
    #3 0x7f2cb588fa23 in parse_open_term /root/bitwuzla/src/parser/bzlasmt2.c:4709
    #4 0x7f2cb588fe26 in parse_term_aux_smt2 /root/bitwuzla/src/parser/bzlasmt2.c:4778
    #5 0x7f2cb5890478 in parse_term_smt2 /root/bitwuzla/src/parser/bzlasmt2.c:4815
    #6 0x7f2cb589f443 in read_command_smt2 /root/bitwuzla/src/parser/bzlasmt2.c:5895
    #7 0x7f2cb58a195f in parse_smt2_parser /root/bitwuzla/src/parser/bzlasmt2.c:6113
    #8 0x7f2cb55def69 in parse_aux /root/bitwuzla/src/bzlaparse.c:67
    #9 0x7f2cb55e2457 in bzla_parse /root/bitwuzla/src/bzlaparse.c:270
    #10 0x7f2cb580a847 in bitwuzla_parse /root/bitwuzla/src/api/c/bitwuzla.c:3407
    #11 0x55c8f8f7a69c in bitwuzla_main /root/bitwuzla/src/bzlamain.c:1563
    #12 0x55c8f8f6faec in main /root/bitwuzla/src/bitwuzlamain.c:18
    #13 0x7f2cb50eb0b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)

SUMMARY: AddressSanitizer: heap-buffer-overflow /root/bitwuzla/src/parser/bzlasmt2.c:1737 in item2str_smt2
Shadow bytes around the buggy address:
  0x0c047fff8d70: fa fa 00 02 fa fa 00 05 fa fa 00 fa fa fa 00 03
  0x0c047fff8d80: fa fa 00 01 fa fa 00 01 fa fa 00 01 fa fa 00 01
  0x0c047fff8d90: fa fa 06 fa fa fa 06 fa fa fa 03 fa fa fa 05 fa
  0x0c047fff8da0: fa fa 04 fa fa fa 04 fa fa fa 00 06 fa fa 00 03
  0x0c047fff8db0: fa fa fd fa fa fa fd fa fa fa fd fa fa fa 00 fa
=>0x0c047fff8dc0: fa fa 02 fa fa[fa]02 fa fa fa fa fa fa fa fa fa
  0x0c047fff8dd0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff8de0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff8df0: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff8e00: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c047fff8e10: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07
  Heap left redzone:       fa
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object redzone:    bb
  ASan internal:           fe
  Left alloca redzone:     ca
  Right alloca redzone:    cb
  Shadow gap:              cc
==12144==ABORTING

OS: Ubuntu 20.04
gcc (Ubuntu 9.4.0-1ubuntu1~20.04) 9.4.0

re-bound lets

I'm experimenting to understand "let binding" in smtlib better and have crafted a case which I think Bitwuzla is handling incorrectly:

(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "crafted")
(set-info :status sat)

; variables get bound twice
(assert 
	(let 
		(
			(x (_ bv1 6) ) 
		)
		(let 
			(
				(x (_ bv0 6))  
				(y x)
			)
			(not (= x y)) 
		)
	)
)
(check-sat)

I'm not entirely sure if this is allowed - Mathsat gives an error. But checking the specification I didn't notice anything prohibiting it.

Segfault with Bitvector Arrays

In commit 3130e49 on Amazon Linux compiled with gcc-7.3.1, declaring an array and then defining a function with a quantifier results in a segfault, even when the function does not use the array. Example below:

(declare-const s (Array (_ BitVec 8) (_ BitVec 8)))
(define-fun f 
  ((a (_ BitVec 8)))
  Bool
  (forall ((j (_ BitVec 8))) (bvult (_ bv0 8) a)))
  
(assert (f (_ bv0 8)))
(check-sat)

In debug mode, this gives

Assertion failed: (free_vars.size() > 0), function compute_variable_dependencies, file bzlaslvquant.cpp, line 2052.
[bitwuzla>main] CAUGHT SIGNAL 6
unknown
Abort

Removing the forall or the declaration of s gets rid of the segfault. I have also run into segfaults using Array constants in function bodies, but I'm hoping fixing this will fix that problem as well since the same assertion fails in debug mode.

Impact of Incremental mode

The documentation says:

Enabling this option turns off some optimization techniques.

Could you detail more about the advantage and drawbacks of incremental mode? I will certainly do some benchmarks, but if you already have some insight on what could work pretty well or what would be a disaster, I am more than interested.

Perfomance deterioration from OCaml binding vs process

I faced a strange situation where a "big" part of an array is initialized (~1kB) but not used in any assertion (e.g. this formula). If I feed the SMT file to the solver (bitwuzla -m -i), it solves it quickly but, if I build the formula from the OCaml api, the solving time is multiplied by 10 (only considering the time of check-sat query).

So, using the C API, would you say that creating "junk" expressions that are not involved in any assertion can slowdown the resolution? Is there a way that a term is processed even if it is not part of the assertions?
Of course, the problem may come from the OCaml binding itself or even the way I build the formula.
Still, the build takes less time than sending the formula through pipe, so I do not know what I could have messed.

---

I know the situation can be avoided here with a simple preprocessing but we will not always be able to say that the array initialization is not required. Another approach we are using is laziness: we do not initialize the array, but if the solver return sat, we check for each address returned in the model that it does not conflict with the initialization. If there is a conflict, we add an assertion (= (select array address) value) and query the solver again (mode incremental). The number of bytes sent can be tuned to avoid doing too many loops in the worst case where each initialized byte were meaningful.

Do you have some ideas, with the knowledge of solver internals, of other techniques we can use to deal with big initialized arrays?

Stuck rewriting in rewrite_eq_exp

When using bitwuzla as backend for yosys-smtbmc, I encountered an input for which bitwuzla hangs essentially forever during the initial rewrite for a (define-fun ...), even before the following (check-sat) is issued. I manually minimized the yosys-smtbmc generated SMT2 by removing everything unnecessary to trigger this behavior. I then reduced the width of the involved signals from 32 to 24 bits. With 24 bits, it does get past the (define-fun ...) but still takes 30 seconds just to process it. Both variants are attached. When I take a stack trace during the rewriting, I see deeply nested rewrite_eq_exp calls. I tested with the latest main version of bitwuzla.

I also filed a corresponding issue for boolector Boolector/boolector#205 which shows exactly the same behavior with an identically named function in the stack trace, so I assume the issue is with code that is common to both solvers.

hang_min_32.smt2.txt
hang_min_24.smt2.txt

check-model does nothing in release build

Not sure if this is intentional, but while debugging #51 I noticed that check-model seems to be a nop in release mode. I think this is because assertions get stripped in release mode, and cm.check() is wrapped in an assert here: https://github.com/bitwuzla/bitwuzla/blob/main/src/solving_context.cpp#L57C24-L57C24

To reproduce:

$ vim src/check/check_model.cpp
... insert a return false; at top of CheckModel::check() ...
$ ./configure.py release
$ meson compile
$ ./src/main/bitwuzla -m --check-model
(check-sat)
sat
^D
$ cd ..
$ ./configure.py debug
$ meson compile
$ ./src/main/bitwuzla -m --check-model
(check-sat)
bitwuzla: ../src/solving_context.cpp:57: bzla::Result bzla::SolvingContext::solve(): Assertion `cm.check()' failed.
Aborted (core dumped)

Not sure what the intended behavior is here; I noticed that check-model defaults to false on release builds, but if it is indeed a nop maybe it should just be disabled as an option for release ?

bitwuzla_set_termination_callback: wrong behavior or documentation

The documentation states that The callback function, returns a value > 0 if bitwuzla has been terminated. but it seems that returning a negative value still terminate the solving.

Note. I would have understood if the type was unsigned but the signature states int32_t.

Here is an example that illustrates the problem (using CaDiCal):
it is a hard solving problem a * b = p that should take a very long time but it directly returns unknown while the termination callback always returns -1.

#include <stdio.h>
#include <bitwuzla.h>

int32_t minus_one(void *state)
{
  return -1;
}

int main (int argc, char *argv[])
{
  Bitwuzla *bitwuzla = bitwuzla_new();
  bitwuzla_set_option(bitwuzla, BITWUZLA_OPT_PRODUCE_MODELS, 2);
  bitwuzla_set_option(bitwuzla, BITWUZLA_OPT_INCREMENTAL, 1);

  const BitwuzlaSort *bv64 = bitwuzla_mk_bv_sort(bitwuzla, 64);
  const BitwuzlaSort *bv128 = bitwuzla_mk_bv_sort(bitwuzla, 128);

  const BitwuzlaTerm *a = bitwuzla_mk_const(bitwuzla, bv64, "a");
  const BitwuzlaTerm *b = bitwuzla_mk_const(bitwuzla, bv64, "b");

  const BitwuzlaTerm *a128 =
    bitwuzla_mk_term1_indexed1(bitwuzla,
			       BITWUZLA_KIND_BV_ZERO_EXTEND,
			       a, 64);
  const BitwuzlaTerm *b128 =
    bitwuzla_mk_term1_indexed1(bitwuzla,
			       BITWUZLA_KIND_BV_ZERO_EXTEND,
			       b, 64);

  const BitwuzlaTerm *ab128 =
    bitwuzla_mk_term2(bitwuzla,
		      BITWUZLA_KIND_BV_MUL,
		      a128, b128);

  const BitwuzlaTerm *p =
    bitwuzla_mk_bv_value(bitwuzla, bv128,
			 "87e03acc9f5050086f083d2d5d6b9d47",
			 BITWUZLA_BV_BASE_HEX);

  const BitwuzlaTerm *o128 =
    bitwuzla_mk_bv_one(bitwuzla, bv128);

  bitwuzla_assert(bitwuzla, bitwuzla_mk_term2(bitwuzla,
					      BITWUZLA_KIND_DISTINCT,
					      a128, o128));
  bitwuzla_assert(bitwuzla, bitwuzla_mk_term2(bitwuzla,
					      BITWUZLA_KIND_DISTINCT,
					      b128, o128));
  bitwuzla_assert(bitwuzla, bitwuzla_mk_term2(bitwuzla,
					      BITWUZLA_KIND_EQUAL,
					      ab128, p));

  bitwuzla_set_termination_callback(bitwuzla, &minus_one, NULL);

  switch (bitwuzla_check_sat(bitwuzla)) {
  case BITWUZLA_SAT:
    printf("sat\n");
    break;
  case BITWUZLA_UNSAT:
    printf("unsat\n");
    break;
  case BITWUZLA_UNKNOWN:
    printf("unknown\n");
    break;
  }

  bitwuzla_delete(bitwuzla);
  return 0;
}

My workaround is currently to return 0 also for negative values:

int32_t x = termination_callback(state);
return x & ~(x >> (8 * sizeof(int32_t) - 1));

C api & OCaml binding

Dear developers,

I am currently working on writing an OCaml binding for Bitwuzla.
At first, I am working on a low-level binding, simply wrapping the same functionalities of the C api.
Then, I would like to develop on top of it a higher-level, more Caml-friendly, api but it will not be my priority.

The goal is to provide and publish an Opam package, easing the compilation/installation of Bitwuzla.
At the end, it would be used as an SMT back-end for the binary analysis platform BinSec.
Would you support such initiative?
As far as I understand, the license allows me to publish it on my own, but I would prefer to work with you.
If it is alright for you, the github repository may also be published as part of the Bitwuzla group.

Here are some remarks/questions about the C api:

• compared to use/release Boolector api, the memory references do not need to be tracked anymore?
• does bitwuzla_reset have a significant performance impact over bitwuzla_delete + bitwuzla_new? Also, if I reset a bitwuzla instance, is the termination_callback cleared ? (I assume so)
• there is no bitwuzla_sort_dump utilities, I think it is missing
• the bitwuzla_sort_fun_get_domain and bitwuzla_term_fun_get_domain_sort seems to be of little utility since no exposed function manipulates "tuple sort" (I tried to create a const of the returned sort, it worked, but is printed as ())
• for consistency, I would consider changing the signature of bitwuzla_sort_fun_get_domain_sorts (and term variant) to something that return the size too: BitwuzlaSort **(*)(BitwuzlaSort*, uint32_t*). Yet, you do not need to change the fact that it returns a null terminated array as long as it is not counted in the returned size
• there are no utilities to get the bits of a bitvector value term. It is not a problem for my binding since I know how to extract it: I am creating an OCaml Zarith bigint by copying the internal mpz_t (sometimes inverted) bits. Yet, for other uses, a bitwuzla_value_get_bv_bits and/or bitwuzla_value_get_bv_bits_int64 may be useful

Best regards,
Frédéric Recoules

Error encountered: Assertion `cm.check()' failed

Hello, and thanks for the great solver !

Per the release of 0.1.0, I've ported a project that was running fine with yices and cvc5 to also support the new bitwuzla. Unfortunately, I'm hitting this error:

bitwuzla: ../src/solving_context.cpp:57: bzla::Result bzla::SolvingContext::solve(): Assertion `cm.check()' failed.
Aborted

I've used ddSMT (thanks for that too!) to reduce the triggering input to this:

(declare-const p (_ BitVec 1))
(declare-fun m () (Array (_ BitVec 1) (Array (_ BitVec 1) (_ BitVec 1))))
(assert (= (_ bv0 1) (ite (distinct (_ bv0 1) (select (select m (_ bv0 1)) (_ bv0 1))) (_ bv0 1) (_ bv1 1))))
(assert (= p (ite (distinct (_ bv0 1) (select (select (store m (_ bv0 1) (store (select m (_ bv0 1)) (_ bv0 1) (ite (= (_ bv0 1) (select (select (store m (_ bv0 1) (store (select m (_ bv0 1)) (_ bv0 1) (select (select (store m (_ bv0 1) (store (select m (_ bv0 1)) (_ bv0 1) (select (select (store m (_ bv0 1) (store (select m (_ bv0 1)) (_ bv0 1) (ite (= (_ bv0 1) (select (select m (_ bv0 1)) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (select (select m (_ bv0 1)) (_ bv0 1))) (select (select m (_ bv0 1)) (_ bv0 1))))) (_ bv0 1)) (_ bv0 1)))) (_ bv0 1)) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (_ bv0 1)) (_ bv0 1))) (_ bv1 1) (_ bv0 1))))
(assert (= (_ bv0 1) p))
(check-sat)
(get-model)

I have confirmed that (after prepending with a set-logic QF_ABV) this file is determined sat by Z3, CVC5, and Yices. I have built Bitwuzla from source on commit 5a0e2d7177272a1d483f1b4a1126b1f38fd01fb7.

Any thoughts for avoiding this would be welcome.

Nested Arrays Support

Hello, I noticed Bitwuzla (as of commit 1230d80) does not seem to have nested arrays support:

$ bitwuzla
(set-logic QF_ABV)
(declare-fun x () (Array Bool (Array Bool Bool)))
bitwuzla: <stdin>:2:32: expected '_' at 'Array'

I assume (but would love confirmation) that this is the same underlying issue as #38 .

Opening this to express additional interest in such a feature, as I have an application where it would be quite convenient to support nested arrays.

Specifically, I want to assert equality between subranges of two arrays. In Z3, CVC5, Yices2 I can do this by making each array into an array of arrays ('block the memory into regions') and asserting equality between the second-level arrays like (= (select m1 a1) (select m2 a2)). But maybe I'm missing an approach. If you have a better suggested way of doing this in Bitwuzla I would also love to hear any suggestions there. I can try using quantifiers, but have found CVC5/Z3 at least really choke quickly in non-QF ABV and would ideally like to use an encoding that works reasonably well in all solvers.

Thanks for the great project!

Assertion fails: src/bzlafp.cpp:721

Greetings,
For this instance, bitwuzla 1230d80 debug build

$ bitwuzla small.smt2       
bitwuzla: /root/smt/bitwuzla/src/bzlafp.cpp:721: static void BzlaFPTraits::postcondition(const bool&): Assertion `p' failed.
[bitwuzla>main] CAUGHT SIGNAL 6
unknown
Aborted (core dumped)
$ cat small.smt2  
(assert ((fp.sqrt RNE (fp (_ bv0 1) (_ bv0 3) (_ bv1 3)))))

`get-value` on array does not return a value in incremental query

Hi, thanks for fixing all the previous bugs. Almost all the tests in chiseltest now pass.

The remaining problem I face is in the following query, where the last get-value returns a symbol instead of a value:

((dut_entries@0 (declare-const dut_entries@0 (Array (_ BitVec 2) (_ BitVec 32))) ))

When I make the query non-incremental, then I get a value in the expected format:

((dut_entries@0 (store ((as const (Array (_ BitVec 2) (_ BitVec 32))) #b00000000000000000000000000000000) #b01 #b11111111111111111111111111111110)))

The --incremental query:

(set-option :produce-models true)
(set-logic QF_ABV)
(push 1)
(declare-fun dut_entries@0 () (Array (_ BitVec 2) (_ BitVec 32)))
(declare-fun dut_deqIndex_value@0 () (_ BitVec 2))
(declare-fun dut_enqIndex_value@0 () (_ BitVec 2))
(declare-fun dut_maybeFull@0 () Bool)
(declare-fun tracker_elementCount@0 () (_ BitVec 2))
(declare-fun tracker_isActive@0 () Bool)
(declare-fun tracker_packetValue@0 () (_ BitVec 32))
(declare-fun tracker_packetCount@0 () (_ BitVec 2))
(define-fun _resetCount@0 () Bool false)
(declare-fun reset@0 () Bool)
(declare-fun io_enq_valid@0 () Bool)
(declare-fun io_enq_bits@0 () (_ BitVec 32))
(declare-fun io_deq_ready@0 () Bool)
(declare-fun startTracking@0 () Bool)
(declare-fun dut_entries_io_deq_bits_MPORT_rand_data@0 () (_ BitVec 32))
(declare-fun dut__GEN_4_invalid@0 () (_ BitVec 2))
(declare-fun dut__GEN_7_invalid@0 () Bool)
(declare-fun dut__GEN_8_invalid@0 () (_ BitVec 32))
(define-fun dut_entries.io_deq_bits_MPORT.addr@0 () (_ BitVec 2) dut_deqIndex_value@0)
(define-fun dut_entries.io_deq_bits_MPORT.data@0 () (_ BitVec 32) (select dut_entries@0 dut_entries.io_deq_bits_MPORT.addr@0))
(define-fun dut_entries_io_deq_bits_MPORT_addr@0 () (_ BitVec 2) dut_deqIndex_value@0)
(define-fun dut_entries_io_deq_bits_MPORT_oob@0 () Bool (not (bvugt (_ bv3 2) dut_entries_io_deq_bits_MPORT_addr@0)))
(define-fun dut_entries_io_deq_bits_MPORT_rand_data.en@0 () Bool dut_entries_io_deq_bits_MPORT_oob@0)
(define-fun dut_indicesEqual@0 () Bool (= dut_enqIndex_value@0 dut_deqIndex_value@0))
(define-fun dut__empty_T@0 () Bool (not dut_maybeFull@0))
(define-fun dut_empty@0 () Bool (and dut_indicesEqual@0 dut__empty_T@0))
(define-fun dut_full@0 () Bool (and dut_indicesEqual@0 dut_maybeFull@0))
(define-fun dut__io_enq_ready_T@0 () Bool (not dut_full@0))
(define-fun dut_io_deq_ready@0 () Bool io_deq_ready@0)
(define-fun dut_io_deq_valid@0 () Bool (not dut_empty@0))
(define-fun dut__T@0 () Bool (and dut_io_deq_ready@0 dut_io_deq_valid@0))
(define-fun dut_io_enq_ready@0 () Bool (or dut__io_enq_ready_T@0 dut_io_deq_ready@0))
(define-fun dut_io_enq_valid@0 () Bool io_enq_valid@0)
(define-fun dut__T_1@0 () Bool (and dut_io_enq_ready@0 dut_io_enq_valid@0))
(define-fun dut__T_2@0 () Bool (distinct dut__T@0 dut__T_1@0))
(define-fun dut__T_3@0 () Bool (and dut_indicesEqual@0 dut__T_2@0))
(define-fun dut__GEN_0@0 () Bool (ite dut__T_3@0 dut__empty_T@0 dut_maybeFull@0))
(define-fun dut_wrap@0 () Bool (= dut_deqIndex_value@0 (_ bv2 2)))
(define-fun dut__value_T@0 () (_ BitVec 3) (bvadd ((_ zero_extend 1) dut_deqIndex_value@0) (_ bv1 3)))
(define-fun dut__value_T_1@0 () (_ BitVec 2) ((_ extract 1 0) dut__value_T@0))
(define-fun dut__GEN_1@0 () (_ BitVec 2) (ite dut_wrap@0 (_ bv0 2) dut__value_T_1@0))
(define-fun dut__GEN_2@0 () (_ BitVec 2) (ite dut__T@0 dut__GEN_1@0 dut_deqIndex_value@0))
(define-fun dut_wrap_1@0 () Bool (= dut_enqIndex_value@0 (_ bv2 2)))
(define-fun dut__value_T_2@0 () (_ BitVec 3) (bvadd ((_ zero_extend 1) dut_enqIndex_value@0) (_ bv1 3)))
(define-fun dut__value_T_3@0 () (_ BitVec 2) ((_ extract 1 0) dut__value_T_2@0))
(define-fun dut__GEN_3@0 () (_ BitVec 2) (ite dut_wrap_1@0 (_ bv0 2) dut__value_T_3@0))
(define-fun dut__GEN_4_invalid.en@0 () Bool (not dut__T_1@0))
(define-fun dut__GEN_7_invalid.en@0 () Bool (not dut__T_1@0))
(define-fun dut__GEN_8_invalid.en@0 () Bool (not dut__T_1@0))
(define-fun dut__GEN_9@0 () (_ BitVec 2) (ite dut__T_1@0 dut__GEN_3@0 dut_enqIndex_value@0))
(define-fun dut_io_deq_bits@0 () (_ BitVec 32) (ite dut_entries_io_deq_bits_MPORT_oob@0 dut_entries_io_deq_bits_MPORT_rand_data@0 dut_entries.io_deq_bits_MPORT.data@0))
(define-fun dut_entries.io_deq_bits_MPORT.en@0 () Bool true)
(define-fun dut_entries.MPORT.en@0 () Bool (and dut_io_enq_ready@0 dut_io_enq_valid@0))
(define-fun dut_entries.MPORT.addr@0 () (_ BitVec 2) (ite (not dut__T_1@0) dut__GEN_4_invalid@0 dut_enqIndex_value@0))
(define-fun dut_entries.MPORT.mask@0 () Bool (ite (not dut__T_1@0) dut__GEN_7_invalid@0 true))
(define-fun dut_io_enq_bits@0 () (_ BitVec 32) io_enq_bits@0)
(define-fun dut_entries.MPORT.data@0 () (_ BitVec 32) (ite (not dut__T_1@0) dut__GEN_8_invalid@0 dut_io_enq_bits@0))
(define-fun tracker_deq_valid@0 () Bool (and dut_io_deq_ready@0 dut_io_deq_valid@0))
(define-fun tracker__nextElementCount_T@0 () Bool (not tracker_deq_valid@0))
(define-fun tracker_enq_valid@0 () Bool (and dut_io_enq_ready@0 dut_io_enq_valid@0))
(define-fun tracker__nextElementCount_T_1@0 () Bool (and tracker_enq_valid@0 tracker__nextElementCount_T@0))
(define-fun tracker__nextElementCount_T_2@0 () (_ BitVec 3) (bvadd ((_ zero_extend 1) tracker_elementCount@0) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_3@0 () (_ BitVec 2) ((_ extract 1 0) tracker__nextElementCount_T_2@0))
(define-fun tracker__nextElementCount_T_4@0 () Bool (not tracker_enq_valid@0))
(define-fun tracker__nextElementCount_T_5@0 () Bool (and tracker__nextElementCount_T_4@0 tracker_deq_valid@0))
(define-fun tracker__nextElementCount_T_6@0 () (_ BitVec 3) (bvsub ((_ zero_extend 1) tracker_elementCount@0) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_7@0 () (_ BitVec 2) ((_ extract 1 0) tracker__nextElementCount_T_6@0))
(define-fun tracker__nextElementCount_T_8@0 () (_ BitVec 2) (ite tracker__nextElementCount_T_5@0 tracker__nextElementCount_T_7@0 tracker_elementCount@0))
(define-fun tracker_nextElementCount@0 () (_ BitVec 2) (ite tracker__nextElementCount_T_1@0 tracker__nextElementCount_T_3@0 tracker__nextElementCount_T_8@0))
(define-fun tracker__T@0 () Bool (not tracker_isActive@0))
(define-fun tracker__T_1@0 () Bool (and tracker__T@0 tracker_enq_valid@0))
(define-fun tracker_startTracking@0 () Bool startTracking@0)
(define-fun tracker__T_2@0 () Bool (and tracker__T_1@0 tracker_startTracking@0))
(define-fun tracker__T_3@0 () Bool (= tracker_elementCount@0 (_ bv0 2)))
(define-fun tracker__T_4@0 () Bool (and tracker_deq_valid@0 tracker__T_3@0))
(define-fun tracker_enq_bits@0 () (_ BitVec 32) dut_io_enq_bits@0)
(define-fun tracker_deq_bits@0 () (_ BitVec 32) dut_io_deq_bits@0)
(define-fun tracker__T_5@0 () Bool (= tracker_enq_bits@0 tracker_deq_bits@0))
(define-fun tracker_reset@0 () Bool reset@0)
(define-fun tracker__T_7@0 () Bool (not tracker_reset@0))
(define-fun tracker__T_8@0 () Bool (not tracker__T_5@0))
(define-fun tracker__GEN_0@0 () Bool (ite tracker__T_4@0 tracker_isActive@0 true))
(define-fun tracker__GEN_1@0 () (_ BitVec 32) (ite tracker__T_4@0 tracker_packetValue@0 tracker_enq_bits@0))
(define-fun tracker__GEN_2@0 () (_ BitVec 2) (ite tracker__T_4@0 tracker_packetCount@0 tracker_nextElementCount@0))
(define-fun tracker__GEN_3@0 () Bool (ite tracker__T_2@0 tracker__GEN_0@0 tracker_isActive@0))
(define-fun tracker__GEN_5@0 () (_ BitVec 2) (ite tracker__T_2@0 tracker__GEN_2@0 tracker_packetCount@0))
(define-fun tracker__T_9@0 () Bool (and tracker_isActive@0 tracker_deq_valid@0))
(define-fun tracker__packetCount_T@0 () (_ BitVec 3) (bvsub ((_ zero_extend 1) tracker_packetCount@0) (_ bv1 3)))
(define-fun tracker__packetCount_T_1@0 () (_ BitVec 2) ((_ extract 1 0) tracker__packetCount_T@0))
(define-fun tracker__T_10@0 () Bool (= tracker_packetCount@0 (_ bv1 2)))
(define-fun tracker__T_11@0 () Bool (= tracker_packetValue@0 tracker_deq_bits@0))
(define-fun tracker__T_14@0 () Bool (not tracker__T_11@0))
(define-fun tracker__GEN_6@0 () Bool (ite tracker__T_10@0 false tracker__GEN_3@0))
(define-fun tracker__GEN_8@0 () Bool (ite tracker__T_9@0 tracker__GEN_6@0 tracker__GEN_3@0))
(define-fun tracker__T_15@0 () Bool (= tracker_elementCount@0 (_ bv3 2)))
(define-fun tracker__T_16@0 () Bool (not tracker__nextElementCount_T_1@0))
(define-fun tracker__T_19@0 () Bool (not tracker__T_16@0))
(define-fun tracker_assert@0 () Bool (not (=> (and (and tracker__T_2@0 tracker__T_4@0) tracker__T_7@0) tracker__T_5@0)))
(define-fun tracker_assert_1@0 () Bool (not (=> (and (and tracker__T_9@0 tracker__T_10@0) tracker__T_7@0) tracker__T_11@0)))
(define-fun tracker_assert_2@0 () Bool (not (=> (and tracker__T_15@0 tracker__T_7@0) tracker__T_16@0)))
(define-fun _resetPhase@0 () Bool (not (bvuge (ite _resetCount@0 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun io_enq_ready@0 () Bool dut_io_enq_ready@0)
(define-fun io_deq_valid@0 () Bool dut_io_deq_valid@0)
(define-fun io_deq_bits@0 () (_ BitVec 32) dut_io_deq_bits@0)
(define-fun dut_reset@0 () Bool reset@0)
(define-fun _resetActive@0 () Bool (=> _resetPhase@0 reset@0))
(assert _resetActive@0)
(push 1)
(assert (not (and (not tracker_assert@0) (and (not tracker_assert_1@0) (not tracker_assert_2@0)))))
(check-sat)
(pop 1)
(define-fun dut_entries@1 () (Array (_ BitVec 2) (_ BitVec 32)) (ite (and dut_entries.MPORT.en@0 dut_entries.MPORT.mask@0) (store dut_entries@0 dut_entries.MPORT.addr@0 dut_entries.MPORT.data@0) dut_entries@0))
(define-fun dut_deqIndex_value@1 () (_ BitVec 2) (ite dut_reset@0 (_ bv0 2) dut__GEN_2@0))
(define-fun dut_enqIndex_value@1 () (_ BitVec 2) (ite dut_reset@0 (_ bv0 2) dut__GEN_9@0))
(define-fun dut_maybeFull@1 () Bool (ite dut_reset@0 false dut__GEN_0@0))
(define-fun tracker_elementCount@1 () (_ BitVec 2) (ite tracker_reset@0 (_ bv0 2) tracker_nextElementCount@0))
(define-fun tracker_isActive@1 () Bool (ite tracker_reset@0 false tracker__GEN_8@0))
(define-fun tracker_packetValue@1 () (_ BitVec 32) (ite tracker__T_2@0 tracker__GEN_1@0 tracker_packetValue@0))
(define-fun tracker_packetCount@1 () (_ BitVec 2) (ite tracker__T_9@0 tracker__packetCount_T_1@0 tracker__GEN_5@0))
(define-fun _resetCount@1 () Bool (ite _resetPhase@0 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _resetCount@0 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _resetCount@0))
(declare-fun reset@1 () Bool)
(declare-fun io_enq_valid@1 () Bool)
(declare-fun io_enq_bits@1 () (_ BitVec 32))
(declare-fun io_deq_ready@1 () Bool)
(declare-fun startTracking@1 () Bool)
(declare-fun dut_entries_io_deq_bits_MPORT_rand_data@1 () (_ BitVec 32))
(declare-fun dut__GEN_4_invalid@1 () (_ BitVec 2))
(declare-fun dut__GEN_7_invalid@1 () Bool)
(declare-fun dut__GEN_8_invalid@1 () (_ BitVec 32))
(define-fun dut_entries.io_deq_bits_MPORT.addr@1 () (_ BitVec 2) dut_deqIndex_value@1)
(define-fun dut_entries.io_deq_bits_MPORT.data@1 () (_ BitVec 32) (select dut_entries@1 dut_entries.io_deq_bits_MPORT.addr@1))
(define-fun dut_entries_io_deq_bits_MPORT_addr@1 () (_ BitVec 2) dut_deqIndex_value@1)
(define-fun dut_entries_io_deq_bits_MPORT_oob@1 () Bool (not (bvugt (_ bv3 2) dut_entries_io_deq_bits_MPORT_addr@1)))
(define-fun dut_entries_io_deq_bits_MPORT_rand_data.en@1 () Bool dut_entries_io_deq_bits_MPORT_oob@1)
(define-fun dut_indicesEqual@1 () Bool (= dut_enqIndex_value@1 dut_deqIndex_value@1))
(define-fun dut__empty_T@1 () Bool (not dut_maybeFull@1))
(define-fun dut_empty@1 () Bool (and dut_indicesEqual@1 dut__empty_T@1))
(define-fun dut_full@1 () Bool (and dut_indicesEqual@1 dut_maybeFull@1))
(define-fun dut__io_enq_ready_T@1 () Bool (not dut_full@1))
(define-fun dut_io_deq_ready@1 () Bool io_deq_ready@1)
(define-fun dut_io_deq_valid@1 () Bool (not dut_empty@1))
(define-fun dut__T@1 () Bool (and dut_io_deq_ready@1 dut_io_deq_valid@1))
(define-fun dut_io_enq_ready@1 () Bool (or dut__io_enq_ready_T@1 dut_io_deq_ready@1))
(define-fun dut_io_enq_valid@1 () Bool io_enq_valid@1)
(define-fun dut__T_1@1 () Bool (and dut_io_enq_ready@1 dut_io_enq_valid@1))
(define-fun dut__T_2@1 () Bool (distinct dut__T@1 dut__T_1@1))
(define-fun dut__T_3@1 () Bool (and dut_indicesEqual@1 dut__T_2@1))
(define-fun dut__GEN_0@1 () Bool (ite dut__T_3@1 dut__empty_T@1 dut_maybeFull@1))
(define-fun dut_wrap@1 () Bool (= dut_deqIndex_value@1 (_ bv2 2)))
(define-fun dut__value_T@1 () (_ BitVec 3) (bvadd ((_ zero_extend 1) dut_deqIndex_value@1) (_ bv1 3)))
(define-fun dut__value_T_1@1 () (_ BitVec 2) ((_ extract 1 0) dut__value_T@1))
(define-fun dut__GEN_1@1 () (_ BitVec 2) (ite dut_wrap@1 (_ bv0 2) dut__value_T_1@1))
(define-fun dut__GEN_2@1 () (_ BitVec 2) (ite dut__T@1 dut__GEN_1@1 dut_deqIndex_value@1))
(define-fun dut_wrap_1@1 () Bool (= dut_enqIndex_value@1 (_ bv2 2)))
(define-fun dut__value_T_2@1 () (_ BitVec 3) (bvadd ((_ zero_extend 1) dut_enqIndex_value@1) (_ bv1 3)))
(define-fun dut__value_T_3@1 () (_ BitVec 2) ((_ extract 1 0) dut__value_T_2@1))
(define-fun dut__GEN_3@1 () (_ BitVec 2) (ite dut_wrap_1@1 (_ bv0 2) dut__value_T_3@1))
(define-fun dut__GEN_4_invalid.en@1 () Bool (not dut__T_1@1))
(define-fun dut__GEN_7_invalid.en@1 () Bool (not dut__T_1@1))
(define-fun dut__GEN_8_invalid.en@1 () Bool (not dut__T_1@1))
(define-fun dut__GEN_9@1 () (_ BitVec 2) (ite dut__T_1@1 dut__GEN_3@1 dut_enqIndex_value@1))
(define-fun dut_io_deq_bits@1 () (_ BitVec 32) (ite dut_entries_io_deq_bits_MPORT_oob@1 dut_entries_io_deq_bits_MPORT_rand_data@1 dut_entries.io_deq_bits_MPORT.data@1))
(define-fun dut_entries.io_deq_bits_MPORT.en@1 () Bool true)
(define-fun dut_entries.MPORT.en@1 () Bool (and dut_io_enq_ready@1 dut_io_enq_valid@1))
(define-fun dut_entries.MPORT.addr@1 () (_ BitVec 2) (ite (not dut__T_1@1) dut__GEN_4_invalid@1 dut_enqIndex_value@1))
(define-fun dut_entries.MPORT.mask@1 () Bool (ite (not dut__T_1@1) dut__GEN_7_invalid@1 true))
(define-fun dut_io_enq_bits@1 () (_ BitVec 32) io_enq_bits@1)
(define-fun dut_entries.MPORT.data@1 () (_ BitVec 32) (ite (not dut__T_1@1) dut__GEN_8_invalid@1 dut_io_enq_bits@1))
(define-fun tracker_deq_valid@1 () Bool (and dut_io_deq_ready@1 dut_io_deq_valid@1))
(define-fun tracker__nextElementCount_T@1 () Bool (not tracker_deq_valid@1))
(define-fun tracker_enq_valid@1 () Bool (and dut_io_enq_ready@1 dut_io_enq_valid@1))
(define-fun tracker__nextElementCount_T_1@1 () Bool (and tracker_enq_valid@1 tracker__nextElementCount_T@1))
(define-fun tracker__nextElementCount_T_2@1 () (_ BitVec 3) (bvadd ((_ zero_extend 1) tracker_elementCount@1) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_3@1 () (_ BitVec 2) ((_ extract 1 0) tracker__nextElementCount_T_2@1))
(define-fun tracker__nextElementCount_T_4@1 () Bool (not tracker_enq_valid@1))
(define-fun tracker__nextElementCount_T_5@1 () Bool (and tracker__nextElementCount_T_4@1 tracker_deq_valid@1))
(define-fun tracker__nextElementCount_T_6@1 () (_ BitVec 3) (bvsub ((_ zero_extend 1) tracker_elementCount@1) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_7@1 () (_ BitVec 2) ((_ extract 1 0) tracker__nextElementCount_T_6@1))
(define-fun tracker__nextElementCount_T_8@1 () (_ BitVec 2) (ite tracker__nextElementCount_T_5@1 tracker__nextElementCount_T_7@1 tracker_elementCount@1))
(define-fun tracker_nextElementCount@1 () (_ BitVec 2) (ite tracker__nextElementCount_T_1@1 tracker__nextElementCount_T_3@1 tracker__nextElementCount_T_8@1))
(define-fun tracker__T@1 () Bool (not tracker_isActive@1))
(define-fun tracker__T_1@1 () Bool (and tracker__T@1 tracker_enq_valid@1))
(define-fun tracker_startTracking@1 () Bool startTracking@1)
(define-fun tracker__T_2@1 () Bool (and tracker__T_1@1 tracker_startTracking@1))
(define-fun tracker__T_3@1 () Bool (= tracker_elementCount@1 (_ bv0 2)))
(define-fun tracker__T_4@1 () Bool (and tracker_deq_valid@1 tracker__T_3@1))
(define-fun tracker_enq_bits@1 () (_ BitVec 32) dut_io_enq_bits@1)
(define-fun tracker_deq_bits@1 () (_ BitVec 32) dut_io_deq_bits@1)
(define-fun tracker__T_5@1 () Bool (= tracker_enq_bits@1 tracker_deq_bits@1))
(define-fun tracker_reset@1 () Bool reset@1)
(define-fun tracker__T_7@1 () Bool (not tracker_reset@1))
(define-fun tracker__T_8@1 () Bool (not tracker__T_5@1))
(define-fun tracker__GEN_0@1 () Bool (ite tracker__T_4@1 tracker_isActive@1 true))
(define-fun tracker__GEN_1@1 () (_ BitVec 32) (ite tracker__T_4@1 tracker_packetValue@1 tracker_enq_bits@1))
(define-fun tracker__GEN_2@1 () (_ BitVec 2) (ite tracker__T_4@1 tracker_packetCount@1 tracker_nextElementCount@1))
(define-fun tracker__GEN_3@1 () Bool (ite tracker__T_2@1 tracker__GEN_0@1 tracker_isActive@1))
(define-fun tracker__GEN_5@1 () (_ BitVec 2) (ite tracker__T_2@1 tracker__GEN_2@1 tracker_packetCount@1))
(define-fun tracker__T_9@1 () Bool (and tracker_isActive@1 tracker_deq_valid@1))
(define-fun tracker__packetCount_T@1 () (_ BitVec 3) (bvsub ((_ zero_extend 1) tracker_packetCount@1) (_ bv1 3)))
(define-fun tracker__packetCount_T_1@1 () (_ BitVec 2) ((_ extract 1 0) tracker__packetCount_T@1))
(define-fun tracker__T_10@1 () Bool (= tracker_packetCount@1 (_ bv1 2)))
(define-fun tracker__T_11@1 () Bool (= tracker_packetValue@1 tracker_deq_bits@1))
(define-fun tracker__T_14@1 () Bool (not tracker__T_11@1))
(define-fun tracker__GEN_6@1 () Bool (ite tracker__T_10@1 false tracker__GEN_3@1))
(define-fun tracker__GEN_8@1 () Bool (ite tracker__T_9@1 tracker__GEN_6@1 tracker__GEN_3@1))
(define-fun tracker__T_15@1 () Bool (= tracker_elementCount@1 (_ bv3 2)))
(define-fun tracker__T_16@1 () Bool (not tracker__nextElementCount_T_1@1))
(define-fun tracker__T_19@1 () Bool (not tracker__T_16@1))
(define-fun tracker_assert@1 () Bool (not (=> (and (and tracker__T_2@1 tracker__T_4@1) tracker__T_7@1) tracker__T_5@1)))
(define-fun tracker_assert_1@1 () Bool (not (=> (and (and tracker__T_9@1 tracker__T_10@1) tracker__T_7@1) tracker__T_11@1)))
(define-fun tracker_assert_2@1 () Bool (not (=> (and tracker__T_15@1 tracker__T_7@1) tracker__T_16@1)))
(define-fun _resetPhase@1 () Bool (not (bvuge (ite _resetCount@1 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun io_enq_ready@1 () Bool dut_io_enq_ready@1)
(define-fun io_deq_valid@1 () Bool dut_io_deq_valid@1)
(define-fun io_deq_bits@1 () (_ BitVec 32) dut_io_deq_bits@1)
(define-fun dut_reset@1 () Bool reset@1)
(define-fun _resetActive@1 () Bool (=> _resetPhase@1 reset@1))
(assert _resetActive@1)
(push 1)
(assert (not (and (not tracker_assert@1) (and (not tracker_assert_1@1) (not tracker_assert_2@1)))))
(check-sat)
(pop 1)
(define-fun dut_entries@2 () (Array (_ BitVec 2) (_ BitVec 32)) (ite (and dut_entries.MPORT.en@1 dut_entries.MPORT.mask@1) (store dut_entries@1 dut_entries.MPORT.addr@1 dut_entries.MPORT.data@1) dut_entries@1))
(define-fun dut_deqIndex_value@2 () (_ BitVec 2) (ite dut_reset@1 (_ bv0 2) dut__GEN_2@1))
(define-fun dut_enqIndex_value@2 () (_ BitVec 2) (ite dut_reset@1 (_ bv0 2) dut__GEN_9@1))
(define-fun dut_maybeFull@2 () Bool (ite dut_reset@1 false dut__GEN_0@1))
(define-fun tracker_elementCount@2 () (_ BitVec 2) (ite tracker_reset@1 (_ bv0 2) tracker_nextElementCount@1))
(define-fun tracker_isActive@2 () Bool (ite tracker_reset@1 false tracker__GEN_8@1))
(define-fun tracker_packetValue@2 () (_ BitVec 32) (ite tracker__T_2@1 tracker__GEN_1@1 tracker_packetValue@1))
(define-fun tracker_packetCount@2 () (_ BitVec 2) (ite tracker__T_9@1 tracker__packetCount_T_1@1 tracker__GEN_5@1))
(define-fun _resetCount@2 () Bool (ite _resetPhase@1 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _resetCount@1 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _resetCount@1))
(declare-fun reset@2 () Bool)
(declare-fun io_enq_valid@2 () Bool)
(declare-fun io_enq_bits@2 () (_ BitVec 32))
(declare-fun io_deq_ready@2 () Bool)
(declare-fun startTracking@2 () Bool)
(declare-fun dut_entries_io_deq_bits_MPORT_rand_data@2 () (_ BitVec 32))
(declare-fun dut__GEN_4_invalid@2 () (_ BitVec 2))
(declare-fun dut__GEN_7_invalid@2 () Bool)
(declare-fun dut__GEN_8_invalid@2 () (_ BitVec 32))
(define-fun dut_entries.io_deq_bits_MPORT.addr@2 () (_ BitVec 2) dut_deqIndex_value@2)
(define-fun dut_entries.io_deq_bits_MPORT.data@2 () (_ BitVec 32) (select dut_entries@2 dut_entries.io_deq_bits_MPORT.addr@2))
(define-fun dut_entries_io_deq_bits_MPORT_addr@2 () (_ BitVec 2) dut_deqIndex_value@2)
(define-fun dut_entries_io_deq_bits_MPORT_oob@2 () Bool (not (bvugt (_ bv3 2) dut_entries_io_deq_bits_MPORT_addr@2)))
(define-fun dut_entries_io_deq_bits_MPORT_rand_data.en@2 () Bool dut_entries_io_deq_bits_MPORT_oob@2)
(define-fun dut_indicesEqual@2 () Bool (= dut_enqIndex_value@2 dut_deqIndex_value@2))
(define-fun dut__empty_T@2 () Bool (not dut_maybeFull@2))
(define-fun dut_empty@2 () Bool (and dut_indicesEqual@2 dut__empty_T@2))
(define-fun dut_full@2 () Bool (and dut_indicesEqual@2 dut_maybeFull@2))
(define-fun dut__io_enq_ready_T@2 () Bool (not dut_full@2))
(define-fun dut_io_deq_ready@2 () Bool io_deq_ready@2)
(define-fun dut_io_deq_valid@2 () Bool (not dut_empty@2))
(define-fun dut__T@2 () Bool (and dut_io_deq_ready@2 dut_io_deq_valid@2))
(define-fun dut_io_enq_ready@2 () Bool (or dut__io_enq_ready_T@2 dut_io_deq_ready@2))
(define-fun dut_io_enq_valid@2 () Bool io_enq_valid@2)
(define-fun dut__T_1@2 () Bool (and dut_io_enq_ready@2 dut_io_enq_valid@2))
(define-fun dut__T_2@2 () Bool (distinct dut__T@2 dut__T_1@2))
(define-fun dut__T_3@2 () Bool (and dut_indicesEqual@2 dut__T_2@2))
(define-fun dut__GEN_0@2 () Bool (ite dut__T_3@2 dut__empty_T@2 dut_maybeFull@2))
(define-fun dut_wrap@2 () Bool (= dut_deqIndex_value@2 (_ bv2 2)))
(define-fun dut__value_T@2 () (_ BitVec 3) (bvadd ((_ zero_extend 1) dut_deqIndex_value@2) (_ bv1 3)))
(define-fun dut__value_T_1@2 () (_ BitVec 2) ((_ extract 1 0) dut__value_T@2))
(define-fun dut__GEN_1@2 () (_ BitVec 2) (ite dut_wrap@2 (_ bv0 2) dut__value_T_1@2))
(define-fun dut__GEN_2@2 () (_ BitVec 2) (ite dut__T@2 dut__GEN_1@2 dut_deqIndex_value@2))
(define-fun dut_wrap_1@2 () Bool (= dut_enqIndex_value@2 (_ bv2 2)))
(define-fun dut__value_T_2@2 () (_ BitVec 3) (bvadd ((_ zero_extend 1) dut_enqIndex_value@2) (_ bv1 3)))
(define-fun dut__value_T_3@2 () (_ BitVec 2) ((_ extract 1 0) dut__value_T_2@2))
(define-fun dut__GEN_3@2 () (_ BitVec 2) (ite dut_wrap_1@2 (_ bv0 2) dut__value_T_3@2))
(define-fun dut__GEN_4_invalid.en@2 () Bool (not dut__T_1@2))
(define-fun dut__GEN_7_invalid.en@2 () Bool (not dut__T_1@2))
(define-fun dut__GEN_8_invalid.en@2 () Bool (not dut__T_1@2))
(define-fun dut__GEN_9@2 () (_ BitVec 2) (ite dut__T_1@2 dut__GEN_3@2 dut_enqIndex_value@2))
(define-fun dut_io_deq_bits@2 () (_ BitVec 32) (ite dut_entries_io_deq_bits_MPORT_oob@2 dut_entries_io_deq_bits_MPORT_rand_data@2 dut_entries.io_deq_bits_MPORT.data@2))
(define-fun dut_entries.io_deq_bits_MPORT.en@2 () Bool true)
(define-fun dut_entries.MPORT.en@2 () Bool (and dut_io_enq_ready@2 dut_io_enq_valid@2))
(define-fun dut_entries.MPORT.addr@2 () (_ BitVec 2) (ite (not dut__T_1@2) dut__GEN_4_invalid@2 dut_enqIndex_value@2))
(define-fun dut_entries.MPORT.mask@2 () Bool (ite (not dut__T_1@2) dut__GEN_7_invalid@2 true))
(define-fun dut_io_enq_bits@2 () (_ BitVec 32) io_enq_bits@2)
(define-fun dut_entries.MPORT.data@2 () (_ BitVec 32) (ite (not dut__T_1@2) dut__GEN_8_invalid@2 dut_io_enq_bits@2))
(define-fun tracker_deq_valid@2 () Bool (and dut_io_deq_ready@2 dut_io_deq_valid@2))
(define-fun tracker__nextElementCount_T@2 () Bool (not tracker_deq_valid@2))
(define-fun tracker_enq_valid@2 () Bool (and dut_io_enq_ready@2 dut_io_enq_valid@2))
(define-fun tracker__nextElementCount_T_1@2 () Bool (and tracker_enq_valid@2 tracker__nextElementCount_T@2))
(define-fun tracker__nextElementCount_T_2@2 () (_ BitVec 3) (bvadd ((_ zero_extend 1) tracker_elementCount@2) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_3@2 () (_ BitVec 2) ((_ extract 1 0) tracker__nextElementCount_T_2@2))
(define-fun tracker__nextElementCount_T_4@2 () Bool (not tracker_enq_valid@2))
(define-fun tracker__nextElementCount_T_5@2 () Bool (and tracker__nextElementCount_T_4@2 tracker_deq_valid@2))
(define-fun tracker__nextElementCount_T_6@2 () (_ BitVec 3) (bvsub ((_ zero_extend 1) tracker_elementCount@2) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_7@2 () (_ BitVec 2) ((_ extract 1 0) tracker__nextElementCount_T_6@2))
(define-fun tracker__nextElementCount_T_8@2 () (_ BitVec 2) (ite tracker__nextElementCount_T_5@2 tracker__nextElementCount_T_7@2 tracker_elementCount@2))
(define-fun tracker_nextElementCount@2 () (_ BitVec 2) (ite tracker__nextElementCount_T_1@2 tracker__nextElementCount_T_3@2 tracker__nextElementCount_T_8@2))
(define-fun tracker__T@2 () Bool (not tracker_isActive@2))
(define-fun tracker__T_1@2 () Bool (and tracker__T@2 tracker_enq_valid@2))
(define-fun tracker_startTracking@2 () Bool startTracking@2)
(define-fun tracker__T_2@2 () Bool (and tracker__T_1@2 tracker_startTracking@2))
(define-fun tracker__T_3@2 () Bool (= tracker_elementCount@2 (_ bv0 2)))
(define-fun tracker__T_4@2 () Bool (and tracker_deq_valid@2 tracker__T_3@2))
(define-fun tracker_enq_bits@2 () (_ BitVec 32) dut_io_enq_bits@2)
(define-fun tracker_deq_bits@2 () (_ BitVec 32) dut_io_deq_bits@2)
(define-fun tracker__T_5@2 () Bool (= tracker_enq_bits@2 tracker_deq_bits@2))
(define-fun tracker_reset@2 () Bool reset@2)
(define-fun tracker__T_7@2 () Bool (not tracker_reset@2))
(define-fun tracker__T_8@2 () Bool (not tracker__T_5@2))
(define-fun tracker__GEN_0@2 () Bool (ite tracker__T_4@2 tracker_isActive@2 true))
(define-fun tracker__GEN_1@2 () (_ BitVec 32) (ite tracker__T_4@2 tracker_packetValue@2 tracker_enq_bits@2))
(define-fun tracker__GEN_2@2 () (_ BitVec 2) (ite tracker__T_4@2 tracker_packetCount@2 tracker_nextElementCount@2))
(define-fun tracker__GEN_3@2 () Bool (ite tracker__T_2@2 tracker__GEN_0@2 tracker_isActive@2))
(define-fun tracker__GEN_5@2 () (_ BitVec 2) (ite tracker__T_2@2 tracker__GEN_2@2 tracker_packetCount@2))
(define-fun tracker__T_9@2 () Bool (and tracker_isActive@2 tracker_deq_valid@2))
(define-fun tracker__packetCount_T@2 () (_ BitVec 3) (bvsub ((_ zero_extend 1) tracker_packetCount@2) (_ bv1 3)))
(define-fun tracker__packetCount_T_1@2 () (_ BitVec 2) ((_ extract 1 0) tracker__packetCount_T@2))
(define-fun tracker__T_10@2 () Bool (= tracker_packetCount@2 (_ bv1 2)))
(define-fun tracker__T_11@2 () Bool (= tracker_packetValue@2 tracker_deq_bits@2))
(define-fun tracker__T_14@2 () Bool (not tracker__T_11@2))
(define-fun tracker__GEN_6@2 () Bool (ite tracker__T_10@2 false tracker__GEN_3@2))
(define-fun tracker__GEN_8@2 () Bool (ite tracker__T_9@2 tracker__GEN_6@2 tracker__GEN_3@2))
(define-fun tracker__T_15@2 () Bool (= tracker_elementCount@2 (_ bv3 2)))
(define-fun tracker__T_16@2 () Bool (not tracker__nextElementCount_T_1@2))
(define-fun tracker__T_19@2 () Bool (not tracker__T_16@2))
(define-fun tracker_assert@2 () Bool (not (=> (and (and tracker__T_2@2 tracker__T_4@2) tracker__T_7@2) tracker__T_5@2)))
(define-fun tracker_assert_1@2 () Bool (not (=> (and (and tracker__T_9@2 tracker__T_10@2) tracker__T_7@2) tracker__T_11@2)))
(define-fun tracker_assert_2@2 () Bool (not (=> (and tracker__T_15@2 tracker__T_7@2) tracker__T_16@2)))
(define-fun _resetPhase@2 () Bool (not (bvuge (ite _resetCount@2 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun io_enq_ready@2 () Bool dut_io_enq_ready@2)
(define-fun io_deq_valid@2 () Bool dut_io_deq_valid@2)
(define-fun io_deq_bits@2 () (_ BitVec 32) dut_io_deq_bits@2)
(define-fun dut_reset@2 () Bool reset@2)
(define-fun _resetActive@2 () Bool (=> _resetPhase@2 reset@2))
(assert _resetActive@2)
(push 1)
(assert (not (and (not tracker_assert@2) (and (not tracker_assert_1@2) (not tracker_assert_2@2)))))
(check-sat)
(pop 1)
(define-fun dut_entries@3 () (Array (_ BitVec 2) (_ BitVec 32)) (ite (and dut_entries.MPORT.en@2 dut_entries.MPORT.mask@2) (store dut_entries@2 dut_entries.MPORT.addr@2 dut_entries.MPORT.data@2) dut_entries@2))
(define-fun dut_deqIndex_value@3 () (_ BitVec 2) (ite dut_reset@2 (_ bv0 2) dut__GEN_2@2))
(define-fun dut_enqIndex_value@3 () (_ BitVec 2) (ite dut_reset@2 (_ bv0 2) dut__GEN_9@2))
(define-fun dut_maybeFull@3 () Bool (ite dut_reset@2 false dut__GEN_0@2))
(define-fun tracker_elementCount@3 () (_ BitVec 2) (ite tracker_reset@2 (_ bv0 2) tracker_nextElementCount@2))
(define-fun tracker_isActive@3 () Bool (ite tracker_reset@2 false tracker__GEN_8@2))
(define-fun tracker_packetValue@3 () (_ BitVec 32) (ite tracker__T_2@2 tracker__GEN_1@2 tracker_packetValue@2))
(define-fun tracker_packetCount@3 () (_ BitVec 2) (ite tracker__T_9@2 tracker__packetCount_T_1@2 tracker__GEN_5@2))
(define-fun _resetCount@3 () Bool (ite _resetPhase@2 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _resetCount@2 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _resetCount@2))
(declare-fun reset@3 () Bool)
(declare-fun io_enq_valid@3 () Bool)
(declare-fun io_enq_bits@3 () (_ BitVec 32))
(declare-fun io_deq_ready@3 () Bool)
(declare-fun startTracking@3 () Bool)
(declare-fun dut_entries_io_deq_bits_MPORT_rand_data@3 () (_ BitVec 32))
(declare-fun dut__GEN_4_invalid@3 () (_ BitVec 2))
(declare-fun dut__GEN_7_invalid@3 () Bool)
(declare-fun dut__GEN_8_invalid@3 () (_ BitVec 32))
(define-fun dut_entries.io_deq_bits_MPORT.addr@3 () (_ BitVec 2) dut_deqIndex_value@3)
(define-fun dut_entries.io_deq_bits_MPORT.data@3 () (_ BitVec 32) (select dut_entries@3 dut_entries.io_deq_bits_MPORT.addr@3))
(define-fun dut_entries_io_deq_bits_MPORT_addr@3 () (_ BitVec 2) dut_deqIndex_value@3)
(define-fun dut_entries_io_deq_bits_MPORT_oob@3 () Bool (not (bvugt (_ bv3 2) dut_entries_io_deq_bits_MPORT_addr@3)))
(define-fun dut_entries_io_deq_bits_MPORT_rand_data.en@3 () Bool dut_entries_io_deq_bits_MPORT_oob@3)
(define-fun dut_indicesEqual@3 () Bool (= dut_enqIndex_value@3 dut_deqIndex_value@3))
(define-fun dut__empty_T@3 () Bool (not dut_maybeFull@3))
(define-fun dut_empty@3 () Bool (and dut_indicesEqual@3 dut__empty_T@3))
(define-fun dut_full@3 () Bool (and dut_indicesEqual@3 dut_maybeFull@3))
(define-fun dut__io_enq_ready_T@3 () Bool (not dut_full@3))
(define-fun dut_io_deq_ready@3 () Bool io_deq_ready@3)
(define-fun dut_io_deq_valid@3 () Bool (not dut_empty@3))
(define-fun dut__T@3 () Bool (and dut_io_deq_ready@3 dut_io_deq_valid@3))
(define-fun dut_io_enq_ready@3 () Bool (or dut__io_enq_ready_T@3 dut_io_deq_ready@3))
(define-fun dut_io_enq_valid@3 () Bool io_enq_valid@3)
(define-fun dut__T_1@3 () Bool (and dut_io_enq_ready@3 dut_io_enq_valid@3))
(define-fun dut__T_2@3 () Bool (distinct dut__T@3 dut__T_1@3))
(define-fun dut__T_3@3 () Bool (and dut_indicesEqual@3 dut__T_2@3))
(define-fun dut__GEN_0@3 () Bool (ite dut__T_3@3 dut__empty_T@3 dut_maybeFull@3))
(define-fun dut_wrap@3 () Bool (= dut_deqIndex_value@3 (_ bv2 2)))
(define-fun dut__value_T@3 () (_ BitVec 3) (bvadd ((_ zero_extend 1) dut_deqIndex_value@3) (_ bv1 3)))
(define-fun dut__value_T_1@3 () (_ BitVec 2) ((_ extract 1 0) dut__value_T@3))
(define-fun dut__GEN_1@3 () (_ BitVec 2) (ite dut_wrap@3 (_ bv0 2) dut__value_T_1@3))
(define-fun dut__GEN_2@3 () (_ BitVec 2) (ite dut__T@3 dut__GEN_1@3 dut_deqIndex_value@3))
(define-fun dut_wrap_1@3 () Bool (= dut_enqIndex_value@3 (_ bv2 2)))
(define-fun dut__value_T_2@3 () (_ BitVec 3) (bvadd ((_ zero_extend 1) dut_enqIndex_value@3) (_ bv1 3)))
(define-fun dut__value_T_3@3 () (_ BitVec 2) ((_ extract 1 0) dut__value_T_2@3))
(define-fun dut__GEN_3@3 () (_ BitVec 2) (ite dut_wrap_1@3 (_ bv0 2) dut__value_T_3@3))
(define-fun dut__GEN_4_invalid.en@3 () Bool (not dut__T_1@3))
(define-fun dut__GEN_7_invalid.en@3 () Bool (not dut__T_1@3))
(define-fun dut__GEN_8_invalid.en@3 () Bool (not dut__T_1@3))
(define-fun dut__GEN_9@3 () (_ BitVec 2) (ite dut__T_1@3 dut__GEN_3@3 dut_enqIndex_value@3))
(define-fun dut_io_deq_bits@3 () (_ BitVec 32) (ite dut_entries_io_deq_bits_MPORT_oob@3 dut_entries_io_deq_bits_MPORT_rand_data@3 dut_entries.io_deq_bits_MPORT.data@3))
(define-fun dut_entries.io_deq_bits_MPORT.en@3 () Bool true)
(define-fun dut_entries.MPORT.en@3 () Bool (and dut_io_enq_ready@3 dut_io_enq_valid@3))
(define-fun dut_entries.MPORT.addr@3 () (_ BitVec 2) (ite (not dut__T_1@3) dut__GEN_4_invalid@3 dut_enqIndex_value@3))
(define-fun dut_entries.MPORT.mask@3 () Bool (ite (not dut__T_1@3) dut__GEN_7_invalid@3 true))
(define-fun dut_io_enq_bits@3 () (_ BitVec 32) io_enq_bits@3)
(define-fun dut_entries.MPORT.data@3 () (_ BitVec 32) (ite (not dut__T_1@3) dut__GEN_8_invalid@3 dut_io_enq_bits@3))
(define-fun tracker_deq_valid@3 () Bool (and dut_io_deq_ready@3 dut_io_deq_valid@3))
(define-fun tracker__nextElementCount_T@3 () Bool (not tracker_deq_valid@3))
(define-fun tracker_enq_valid@3 () Bool (and dut_io_enq_ready@3 dut_io_enq_valid@3))
(define-fun tracker__nextElementCount_T_1@3 () Bool (and tracker_enq_valid@3 tracker__nextElementCount_T@3))
(define-fun tracker__nextElementCount_T_2@3 () (_ BitVec 3) (bvadd ((_ zero_extend 1) tracker_elementCount@3) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_3@3 () (_ BitVec 2) ((_ extract 1 0) tracker__nextElementCount_T_2@3))
(define-fun tracker__nextElementCount_T_4@3 () Bool (not tracker_enq_valid@3))
(define-fun tracker__nextElementCount_T_5@3 () Bool (and tracker__nextElementCount_T_4@3 tracker_deq_valid@3))
(define-fun tracker__nextElementCount_T_6@3 () (_ BitVec 3) (bvsub ((_ zero_extend 1) tracker_elementCount@3) (_ bv1 3)))
(define-fun tracker__nextElementCount_T_7@3 () (_ BitVec 2) ((_ extract 1 0) tracker__nextElementCount_T_6@3))
(define-fun tracker__nextElementCount_T_8@3 () (_ BitVec 2) (ite tracker__nextElementCount_T_5@3 tracker__nextElementCount_T_7@3 tracker_elementCount@3))
(define-fun tracker_nextElementCount@3 () (_ BitVec 2) (ite tracker__nextElementCount_T_1@3 tracker__nextElementCount_T_3@3 tracker__nextElementCount_T_8@3))
(define-fun tracker__T@3 () Bool (not tracker_isActive@3))
(define-fun tracker__T_1@3 () Bool (and tracker__T@3 tracker_enq_valid@3))
(define-fun tracker_startTracking@3 () Bool startTracking@3)
(define-fun tracker__T_2@3 () Bool (and tracker__T_1@3 tracker_startTracking@3))
(define-fun tracker__T_3@3 () Bool (= tracker_elementCount@3 (_ bv0 2)))
(define-fun tracker__T_4@3 () Bool (and tracker_deq_valid@3 tracker__T_3@3))
(define-fun tracker_enq_bits@3 () (_ BitVec 32) dut_io_enq_bits@3)
(define-fun tracker_deq_bits@3 () (_ BitVec 32) dut_io_deq_bits@3)
(define-fun tracker__T_5@3 () Bool (= tracker_enq_bits@3 tracker_deq_bits@3))
(define-fun tracker_reset@3 () Bool reset@3)
(define-fun tracker__T_7@3 () Bool (not tracker_reset@3))
(define-fun tracker__T_8@3 () Bool (not tracker__T_5@3))
(define-fun tracker__GEN_0@3 () Bool (ite tracker__T_4@3 tracker_isActive@3 true))
(define-fun tracker__GEN_1@3 () (_ BitVec 32) (ite tracker__T_4@3 tracker_packetValue@3 tracker_enq_bits@3))
(define-fun tracker__GEN_2@3 () (_ BitVec 2) (ite tracker__T_4@3 tracker_packetCount@3 tracker_nextElementCount@3))
(define-fun tracker__GEN_3@3 () Bool (ite tracker__T_2@3 tracker__GEN_0@3 tracker_isActive@3))
(define-fun tracker__GEN_5@3 () (_ BitVec 2) (ite tracker__T_2@3 tracker__GEN_2@3 tracker_packetCount@3))
(define-fun tracker__T_9@3 () Bool (and tracker_isActive@3 tracker_deq_valid@3))
(define-fun tracker__packetCount_T@3 () (_ BitVec 3) (bvsub ((_ zero_extend 1) tracker_packetCount@3) (_ bv1 3)))
(define-fun tracker__packetCount_T_1@3 () (_ BitVec 2) ((_ extract 1 0) tracker__packetCount_T@3))
(define-fun tracker__T_10@3 () Bool (= tracker_packetCount@3 (_ bv1 2)))
(define-fun tracker__T_11@3 () Bool (= tracker_packetValue@3 tracker_deq_bits@3))
(define-fun tracker__T_14@3 () Bool (not tracker__T_11@3))
(define-fun tracker__GEN_6@3 () Bool (ite tracker__T_10@3 false tracker__GEN_3@3))
(define-fun tracker__GEN_8@3 () Bool (ite tracker__T_9@3 tracker__GEN_6@3 tracker__GEN_3@3))
(define-fun tracker__T_15@3 () Bool (= tracker_elementCount@3 (_ bv3 2)))
(define-fun tracker__T_16@3 () Bool (not tracker__nextElementCount_T_1@3))
(define-fun tracker__T_19@3 () Bool (not tracker__T_16@3))
(define-fun tracker_assert@3 () Bool (not (=> (and (and tracker__T_2@3 tracker__T_4@3) tracker__T_7@3) tracker__T_5@3)))
(define-fun tracker_assert_1@3 () Bool (not (=> (and (and tracker__T_9@3 tracker__T_10@3) tracker__T_7@3) tracker__T_11@3)))
(define-fun tracker_assert_2@3 () Bool (not (=> (and tracker__T_15@3 tracker__T_7@3) tracker__T_16@3)))
(define-fun _resetPhase@3 () Bool (not (bvuge (ite _resetCount@3 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun io_enq_ready@3 () Bool dut_io_enq_ready@3)
(define-fun io_deq_valid@3 () Bool dut_io_deq_valid@3)
(define-fun io_deq_bits@3 () (_ BitVec 32) dut_io_deq_bits@3)
(define-fun dut_reset@3 () Bool reset@3)
(define-fun _resetActive@3 () Bool (=> _resetPhase@3 reset@3))
(assert _resetActive@3)
(push 1)
(assert (not (and (not tracker_assert@3) (and (not tracker_assert_1@3) (not tracker_assert_2@3)))))
(check-sat)
(get-value (dut_entries@0))

Issues when building on Windows

Hi! I'm trying to build Bitwuzla on Windows. I setup my environment as detailed in the documentation. The environment seems fine, however, I'm having an issue when the build script tries to setup cadical. Apparently, there's an error when it applies the patch:

checking file src/mobical.cpp
Hunk #1 succeeded at 752 (offset 59 lines).
Hunk #2 succeeded at 1492 (offset 74 lines).
Hunk #3 succeeded at 1517 (offset 74 lines).
Hunk #4 succeeded at 1536 (offset 74 lines).
Hunk #5 succeeded at 1549 (offset 74 lines).
Hunk #6 succeeded at 1567 (offset 74 lines).
Hunk #7 succeeded at 2603 (offset 105 lines).
Hunk #8 succeeded at 2629 (offset 105 lines).
Hunk #9 succeeded at 2663 (offset 105 lines).
checking file src/resources.cpp
Hunk #1 succeeded at 20 with fuzz 2 (offset 13 lines).
Hunk #2 FAILED at 34.
Hunk #3 FAILED at 51.
Hunk #4 FAILED at 64.
Hunk #5 succeeded at 138 with fuzz 1 (offset 66 lines).
3 out of 5 hunks FAILED
checking file src/signal.cpp
Hunk #1 FAILED at 25.
Hunk #2 succeeded at 49 (offset 7 lines).
Hunk #3 FAILED at 67.
Hunk #4 FAILED at 78.
Hunk #5 FAILED at 85.
Hunk #6 succeeded at 121 with fuzz 1 (offset 18 lines).
Hunk #7 succeeded at 129 with fuzz 1 (offset 18 lines).
4 out of 7 hunks FAILED
checking file test/makefile
Hunk #1 FAILED at 1.
1 out of 1 hunk FAILED

In principle, it seems the patch is out of sync with the code that ./contrib/setup-cadical.sh downloads. Could this be the case? I tried with the main branch as well as the tagged version (smtcomp-2021) and I ran into the same issue in both. Some similar happens with btor2tools (picosat and lingeling were setup successfully).

Loading SMT2 from files in Python binding

Bitwuzla can parse files via bitwuzla_parse and bitwuzla_parse_format, but it appears that those functions are not used in the Python binding (or rather commented out).

Are there plans to bring this functionality to the python bindings?

Issues about invalid model

Hi, for this instance, bitwuzla f834fc4 (debug build) gives an invalid model.

$ bitwuzla delta.smt2
[bzlachkmodel] bzla_check_model: invalid model
$ cat delta.smt2
(define-sort FPN () Float64)
(declare-fun e () FPN)
(assert (exists ((E FPN)) (not (= (fp.fma roundTowardNegative e e e) (fp.fma roundTowardNegative e e (fp.fma roundTowardNegative e e e))))))
(check-sat)

OS: Ubuntu 20.04

hello, excuse me, has wallace tree been used in the previous multiplication optimization

hello, excuse me, has wallace tree been used in the previous multiplication optimization

Build with assertions doesn't work

Trying ./configure.py --assertions gives a Python exception:

Traceback (most recent call last):
  File "./configure.py", line 136, in <module>
    main()
  File "./configure.py", line 115, in main
    build_opts.append(f'-Db_ndebug={_bool(args.assertions)}')
  File "./configure.py", line 47, in _bool
    assert val is bool
AssertionError

Removing the assert at line 47 in configure.py fixes this, but there's a missing negation:

> ./configure.py --assertions
-- meson configure build -Db_ndebug=true
-- compile Bitwuzla with: cd build && meson compile

This disables assertions rather than enables them. The setting should be -Dd_ndebug=false,

crash on get-value for array

Hi, thanks for all the fixes. We are down to a single failing test in the chiseltest test suite.

On the following query, bitwuzla crashes with the following output:

sat
((m@0 (store (store[bitwuzla>main] CAUGHT SIGNAL 11
unknown
fish: Job 1, 'bitwuzla bitwuzla_get_array_cra…' terminated by signal SIGSEGV (Address boundary error)

Query:

(set-option :produce-models true)
(set-logic QF_ABV)
(define-fun m@0 () (Array (_ BitVec 2) (_ BitVec 8)) (store (store ((as const (Array (_ BitVec 2) (_ BitVec 8))) (_ bv2 8)) (_ bv0 2) (_ bv1 8)) (_ bv3 2) (_ bv3 8)))
(check-sat)
(get-value (m@0))

z3 output:

sat
((m@0 (store (store ((as const (Array (_ BitVec 2) (_ BitVec 8))) #x02) #b00 #x01)
       #b11
       #x03)))

cvc4 output:

sat
((m@0 (store (store ((as const (Array (_ BitVec 2) (_ BitVec 8))) #b00000010) #b00 #b00000001) #b11 #b00000011)))

beta_reduce segfault w/ reduced 'update' node

Getting a segfault in bzla_sort_fun_get_codomain when beta_reduce calls bzla_node_create_apply:

bitwuzla/src/bzlabeta.c

Lines 443 to 452 in 2bb1fe6

	switch (real_cur->kind)
	{
	case BZLA_APPLY_NODE:
	if (bzla_node_is_fun(e[1]))
	{
	assert(bzla_node_is_args(e[0]));
	/* NOTE: do not use bzla_exp_apply here since
	* beta reduction is used in bzla_rewrite_apply_exp. */
	result = bzla_node_create_apply(bzla, e[1], e[0]);
	}

Backtrace:
(sorry, no symbols, debug build runs too slow & i'm hitting this really deep in a incremental solve so I don't have an easy reproducer).

#0  0x00007ffff68eb3b1 in bzla_sort_fun_get_codomain () from /usr/local/lib/libbitwuzla.so
#1  0x00007ffff689e118 in new_node () from /usr/local/lib/libbitwuzla.so
#2  0x00007ffff68a1c45 in create_exp.constprop () from /usr/local/lib/libbitwuzla.so
#3  0x00007ffff68a3560 in bzla_node_create_apply () from /usr/local/lib/libbitwuzla.so
#4  0x00007ffff687462d in beta_reduce () from /usr/local/lib/libbitwuzla.so
#5  0x00007ffff6973cbb in bzla_eliminate_applies () from /usr/local/lib/libbitwuzla.so
#6  0x00007ffff697fa91 in bzla_simplify () from /usr/local/lib/libbitwuzla.so
#7  0x00007ffff688cf12 in bzla_check_sat () from /usr/local/lib/libbitwuzla.so
#8  0x00007ffff6945b0b in bitwuzla_check_sat () from /usr/local/lib/libbitwuzla.so
...

Relevant snippet from new_node:

bitwuzla/src/bzlanode.c

Lines 2734 to 2737 in 2bb1fe6

	case BZLA_APPLY_NODE:
	sort = bzla_sort_copy(
	bzla, bzla_sort_fun_get_codomain(bzla, bzla_node_get_sort_id(e[0])));
	break;

This requires e[0] to have a function sort, but in the crashing case, it doesn't. Thus, it segfaults when trying to access sort->fun.codomain->id.

In the case of the crash, the function being applied is actually a BZLA_UPDATE_NODE, which seems like a totally legal type to apply. However, the update node's array (e[0]) is somehow actually a BZLA_BV_CONST_NODE, which means (of course) the sort does not have a codomain. I know only very little about this code, but this seems pretty suspicious. I'm only using the public C API, which seems to have thorough checks on the types, so I don't think I'm feeding in garbage here. My array is just 16-bit bv => 8-bit bv.

This reproduced repeatedly with the same backtrace, so it doesn't seem like any sort of one-off memory corruption. My best guess is for some sequence of array operations, it's possible for a BZLA_UPDATE_NODE to have its array (function) to be reduced entirely to a constant (though, this seems suspicious). I noticed some other code that avoids eliminating lambdas when the parent requires them, and I added a check against bzla_node_is_update, and this fixes it. However I have no idea if this is the right fix, or if there is something deeper going on here. I will post a reproducer if I can make one.

diff --git a/src/bzlabeta.c b/src/bzlabeta.c
index f338a52..8f54991 100644
--- a/src/bzlabeta.c
+++ b/src/bzlabeta.c
@@ -379,7 +379,8 @@ beta_reduce(Bzla *bzla,
        * generation for extensionality */
       else if (bzla_node_is_lambda(real_cur) && cur_parent
                && (bzla_node_is_fun_eq(cur_parent)
-                   || bzla_node_is_fun_cond(cur_parent)))
+                   || bzla_node_is_fun_cond(cur_parent)
+                   || bzla_node_is_update(cur_parent) ))
       {
         assert(!bzla_node_param_get_assigned_exp(real_cur->e[0]));
         cur_lambda_depth--;
@@ -464,6 +465,7 @@ beta_reduce(Bzla *bzla,
              * as argument */
             if (cur_parent
                 && (bzla_node_is_fun_eq(cur_parent)
+                    || bzla_node_is_update(cur_parent)
                     || (bzla_node_is_fun_cond(cur_parent)
                         && !bzla_node_param_get_assigned_exp(real_cur->e[0]))))
             {

src/CMakeLists.txt does not include SymFPU_INCLUDE_DIR

Even if SymFPU is found, if it has not been installed from the contrib/* script, the compilation fails because of the missing -I flag in the generated Makefile.

Here is a quick fix:

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 203433e..616bbec 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -111,6 +111,10 @@ target_include_directories(bitwuzla
 target_include_directories(bitwuzla PRIVATE ${Btor2Tools_INCLUDE_DIR})
 target_link_libraries(bitwuzla ${Btor2Tools_LIBRARIES})
 
+if (SymFPU_FOUND)
+  target_include_directories(bitwuzla PRIVATE ${SymFPU_INCLUDE_DIR})
+endif()
+
 if(GMP_FOUND)
   target_include_directories(bitwuzla PRIVATE ${GMP_INCLUDE_DIR})
   target_link_libraries(bitwuzla ${GMP_LIBRARIES})