From e9816ba2944302a3219bf0844eca4e12d6b41b3c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 19 May 2026 08:05:47 +0000
Subject: [PATCH] Do not use `as const` with Z3 due to soundness issue

Disable `as const` for Z3 as it produces wrong results per
https://github.com/Z3Prover/z3/issues/9550.
---
 src/solvers/smt2/smt2_conv.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 70624dab03c..c79b07e7235 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -118,7 +118,7 @@ smt2_convt::smt2_convt(
 
   case solvert::Z3:
     use_array_of_bool = true;
-    use_as_const = true;
+    use_as_const = false;
     use_check_sat_assuming = true;
     use_lambda_for_array = true;
     emit_set_logic = false;