Skip to content

Bitwuzla fixed for quantified BV logics. - #293

Merged
martinjonas merged 2 commits into
SMT-COMP:masterfrom
mpreiner:bitwuzla-fixed-quant-bv
Jul 20, 2026
Merged

martinjonas merged 2 commits into
SMT-COMP:masterfrom
mpreiner:bitwuzla-fixed-quant-bv

Conversation

@mpreiner

Copy link
Copy Markdown
Contributor

Fixes a rare corner case in quantifier instantiation for BV logics.

@github-actions

Copy link
Copy Markdown
Summary of modified submissions

Bitwuzla-fixed

  • 2 authors
  • website: https://bitwuzla.github.io/
  • Participations
    • UnsatCore
      • Bitvec
        • all
      • Equality+MachineArith
        • ABV
        • ABVFP
        • ABVFPLRA
        • AUFBV
        • AUFBVFP
        • UFBV
        • UFBVFP
      • FPArith
        • BVFP
        • BVFPLRA
    • SingleQuery
      • Bitvec
        • all
      • Equality+MachineArith
        • ABV
        • ABVFP
        • ABVFPLRA
        • AUFBV
        • AUFBVFP
        • UFBV
        • UFBVFP
      • FPArith
        • BVFP
        • BVFPLRA
    • ModelValidation
    • Incremental
      • Bitvec
        • all
      • Equality+MachineArith
        • all
      • FPArith
        • all

@martinjonas
martinjonas merged commit 1c4787b into SMT-COMP:master Jul 20, 2026
2 of 4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants