mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Fix Z3 infinite loop: change bv_sort_ac default from false to true

Browse source 
The bv_sort_ac parameter sorts arguments of AC bit-vector operators
(bvor, bvand, bvxor) to create canonical forms, preventing infinite
expansion loops during rewriting.

The old SMT path (asserted_formulas.cpp) always explicitly set
bv_sort_ac=true, but the newer solver preprocessing path used the
default value of false.

Changing the default to true ensures all solver paths benefit from AC
argument sorting. This fixes the issue reported in Z3Prover/z3#7700
where Z3 4.15.1 loops forever on a formula that Z3 4.8.14 resolved
as unsat in ~3 seconds.

Suggested by NikolajBjorner: rewriter.bv_sort_ac=true fixes the issue.
This commit is contained in:
copilot-swe-agent[bot] 2026-07-09 16:18:50 +00:00 • committed by GitHub
parent d63140b749
commit c0e49d6979
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/params/bv_rewriter_params.pyg
View file

@ -7,7 +7,7 @@ def_module_params(module_name='rewriter',
("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),
("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"),
("bv_sort_ac", BOOL, True, "sort the arguments of all AC operators"),
("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"),
("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"),
("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"),