Sign me up Login

Details about package bitwuzla

Name:	bitwuzla
Uploader:	Gábor Németh <homar@riseup.net> (Debian QA page)
Description:	bitwuzla - SMT solver for bit vectors and arrays libbitwuzla0 - SMT solver for bit vectors and arrays (runtime libraries) bitwuzla-dev - SMT solver for bit vectors and arrays (development files) python3-bitwuzla - SMT solver for bit vectors and arrays (Python bindings) bitwuzla-doc - Documentation for Bitwuzla

Package uploads

Upload #1

Information

Version:	0.8.2-1
Uploaded:	2025-12-04 10:58
Source package:	bitwuzla_0.8.2-1.dsc
Distribution:	unstable
Section:	science
Priority:	optional
Homepage:	https://github.com/bitwuzla/bitwuzla
Vcs-Browser:	https://salsa.debian.org/homar/bitwuzla
Vcs-Git:	https://salsa.debian.org/homar/bitwuzla.git
Closes bugs:	#1121763

Changelog

 bitwuzla (0.8.2-1) unstable; urgency=medium
 .
   * Initial release. (Closes: #1121763)

QA information

–
Package uses debhelper-compat

Debhelper compatibility level 13

–

A watch file is present but doesn't work

Warnings:

debian/watch is an obsolete version 1 watch file;
please upgrade to a higher version
(see uscan(1) for details).
debian/watch is an obsolete version 1 watch file;
please upgrade to a higher version
(see uscan(1) for details).
debian/watch is an obsolete version 1 watch file;
please upgrade to a higher version
(see uscan(1) for details).
debian/watch is an obsolete version 1 watch file;
please upgrade to a higher version
(see uscan(1) for details).
there appears to be a version 2 format line in
the version 1 watch file debian/watch;
Have you forgotten a 'version=2' line at the start, perhaps?
Skipping the line: Version: 5

there appears to be a version 2 format line in
the version 1 watch file debian/watch;
Have you forgotten a 'version=2' line at the start, perhaps?
Skipping the line: Template: Github

there appears to be a version 2 format line in
the version 1 watch file debian/watch;
Have you forgotten a 'version=2' line at the start, perhaps?
Skipping the line: Owner: bitwuzla

there appears to be a version 2 format line in
the version 1 watch file debian/watch;
Have you forgotten a 'version=2' line at the start, perhaps?
Skipping the line: Project: bitwuzla

–
Package is not native

Format: 3.0 (quilt)
–
"Maintainer" email is the same as the uploader
–
Package has lintian warnings
bitwuzla source
- W missing-debian-watch-file-standard
  - [debian/watch]
- P silent-on-rules-requiring-root
  - [debian/control]
- X upstream-metadata-file-is-missing
- X very-long-line-length-in-source-file
  - 1021 > 512 [test/regress/solver/bv/regrdomabst6.smt2:7]
  - 10492335 > 512 [test/regress/rewrite/array/rw17.btor.smt2:31]
  - 1066 > 512 [test/regress/solver/bv/hd11.btor.smt2:5]
  - 1069 > 512 [test/regress/solver/array/wchains002se.smt2:11]
  - 1083403 > 512 [test/regress/solver/array/random3.btor.smt2:32]
  - 1165456 > 512 [test/regress/rewrite/bv/eq_special_const_bvor.smt2:14762]
  - 1194526 > 512 [test/regress/rewrite/bv/eq_special_const_bvand.smt2:14762]
  - 1207 > 512 [test/regress/solver/array/wchains002ue.smt2:11]
  - 1216 > 512 [test/regress/solver/array/dubreva002ue.smt2:17]
  - 1243 > 512 [test/regress/solver/array/headline14.btor.smt2:9]
  - 1249 > 512 [test/regress/solver/array/write4.btor.smt2:12]
  - 14132 > 512 [test/regress/rewrite/array/regr3vl4.btor.smt2:34]
  - 1567 > 512 [test/regress/rewrite/array/rwr1.btor.smt2:7]
  - 17301 > 512 [test/regress/solver/array/fifo32in04k05.smt2:108]
  - 17823 > 512 [test/regress/solver/array/fifo32bc04k05.smt2:106]
  - 2038 > 512 [test/regress/solver/array/swapmem002se.smt2:17]
  - 2093 > 512 [test/regress/preprocess/array/nondestr_subst18.smt2:2027]
  - 21367 > 512 [test/regress/solver/array/fifo32ia04k05.smt2:109]
  - 2169 > 512 [test/regress/rewrite/bv/rw48.btor.smt2:8]
  - 2169 > 512 [test/regress/rewrite/bv/rw50.btor.smt2:8]
  - 2449 > 512 [test/regress/preprocess/array/nondestr_subst7.smt2:668]
  - 2516 > 512 [test/regress/solver/array/swapmem002ue.smt2:17]
  - 2800 > 512 [test/regress/solver/bv/modelgen26.btor.smt2:14]
  - 2904680 > 512 [test/regress/rewrite/array/rw16.btor.smt2:30]
  - 3021 > 512 [test/regress/solver/bv/sc12fuzzcheck2.smt2:7]
  - 3207 > 512 [test/regress/preprocess/array/nondestr_subst1.smt2:4043]
  - 3331 > 512 [test/regress/rewrite/bv/rw212.smt2:6]
  - 3737946 > 512 [test/regress/solver/bv/countbits016.smt2:12]
  - 38074 > 512 [test/regress/solver/array/headline13.smt2:15]
  - 513 > 512 [test/regress/solver/abstract/red-bench-8002.smt2:7]
  - 530 > 512 [test/regress/rewrite/bv/rw28.btor.smt2:5]
  - 530 > 512 [test/regress/rewrite/bv/rw29.btor.smt2:5]
  - 5328 > 512 [test/regress/solver/array/lazywritememleak1.btor.smt2:61]
  - 545 > 512 [test/regress/rewrite/array/rw213.smt2:6]
  - 5523 > 512 [test/regress/solver/array/binarysearch32s016.smt2:13]
  - 558 > 512 [test/regress/solver/bv/hd14.btor.smt2:5]
  - 559 > 512 [test/regress/solver/bv/modelgen9.btor.smt2:4]
  - 560 > 512 [test/regress/solver/bv/smtaxiombvsmod1.smt2:5]
  - 560 > 512 [test/regress/solver/bv/smtaxiombvsmod2.smt2:5]
  - 560 > 512 [test/regress/solver/bv/smtaxiombvsmod3.smt2:5]
  - 560 > 512 [test/regress/solver/bv/smtaxiombvsmod4.smt2:5]
  - 560 > 512 [test/regress/solver/bv/smtaxiombvsmod5.smt2:5]
  - 560 > 512 [test/regress/solver/bv/smtaxiombvsmod6.smt2:5]
  - 560 > 512 [test/regress/solver/bv/smtaxiombvsmod7.smt2:5]
  - 560 > 512 [test/regress/solver/bv/smtaxiombvsmod8.smt2:5]
  - 573 > 512 [test/regress/rewrite/array/rw178.btor.smt2:8]
  - 575 > 512 [test/regress/solver/bv/smtaxiombvsmod16.smt2:5]
  - 575 > 512 [test/regress/solver/bv/smtaxiombvsmod32.smt2:5]
  - 575 > 512 [test/regress/solver/bv/smtaxiombvsmod64.smt2:5]
  - 577 > 512 [test/regress/solver/bv/hd9.btor.smt2:4]
  - 597 > 512 [test/regress/solver/array/arraycond5.btor.smt2:10]
  - 597 > 512 [test/regress/solver/array/arraycond6.btor.smt2:10]
  - 597 > 512 [test/regress/solver/array/arraycond7.btor.smt2:10]
  - 597 > 512 [test/regress/solver/array/arraycond8.btor.smt2:10]
  - 598 > 512 [test/regress/solver/bv/calprob14sat5ksimp.btor.smt2:5]
  - 612 > 512 [test/regress/solver/array/memcpy02.smt2:15]
  - 617 > 512 [test/regress/solver/bv/hd16.btor.smt2:5]
  - 639 > 512 [test/regress/solver/array/read16.btor.smt2:9]
  - 662 > 512 [test/regress/solver/bv/hd12.btor.smt2:5]
  - 685 > 512 [test/regress/solver/array/write15.btor.smt2:14]
  - 687 > 512 [test/regress/solver/bv/headline16.btor.smt2:13]
  - 704 > 512 [test/regress/preprocess/array/nondestr_subst2.smt2:149]
  - 705 > 512 [test/regress/solver/array/arraycond12.btor.smt2:14]
  - 7168 > 512 [test/regress/solver/bv/regrdomabst5.smt2:8]
  - 729 > 512 [test/regress/solver/array/write17.btor.smt2:14]
  - 768 > 512 [test/regress/solver/array/selsort002un.smt2:13]
  - 769 > 512 [test/regress/solver/array/write16.btor.smt2:14]
  - 777 > 512 [test/regress/solver/bv/modelgen21.btor.smt2:11]
  - 780683 > 512 [test/regress/rewrite/array/rw18.btor.smt2:32]
  - 786 > 512 [test/regress/solver/array/bubsort002un.smt2:13]
  - 7997 > 512 [test/regress/solver/bv/nextpoweroftwo016.smt2:21]
  - 825 > 512 [test/regress/preprocess/normalize14.smt2:4]
  - 857245 > 512 [test/regress/solver/array/regrbetacache1.btor.smt2:12]
  - 871 > 512 [test/regress/rewrite/bv/rw157.btor.smt2:13]
  - 871 > 512 [test/regress/solver/bv/headline15.btor.smt2:13]
  - 8951 > 512 [test/regress/solver/fp/checkmodelfp1.smt2:8]
–
Package closes ITP bug
- bitwuzla:
  - #1121763 (Wishlist, ITP): ITP: bitwuzla -- SMT solver for bit vectors and arrays
–
Package is not in Debian
–
d/copyright is in DEP5 format

Upstream Contact: Aina Niemetz <niemetz@cs.stanford.edu>

Licenses: Expat

Comments

No comments

Upstream Contact:	Aina Niemetz <niemetz@cs.stanford.edu>
Licenses:	Expat