From c0e49d6979f8f91a9cb309ef483db6c8154b8992 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 9 Jul 2026 16:18:50 +0000 Subject: [PATCH] Fix Z3 infinite loop: change bv_sort_ac default from false to true 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. --- src/params/bv_rewriter_params.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/params/bv_rewriter_params.pyg b/src/params/bv_rewriter_params.pyg index 04c5824852..aa4af90bc9 100644 --- a/src/params/bv_rewriter_params.pyg +++ b/src/params/bv_rewriter_params.pyg @@ -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"),