From d53326044521bc9a4e94d6d706406c5b49e47eea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Dec 2025 16:09:37 -0800
Subject: [PATCH] use new arithmetic solver for AUFLIA, fixes #8090

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_setup.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index c1affcf1a..98db1ab71 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -511,7 +511,7 @@ namespace smt {
         TRACE(setup, tout << "AUFLIA\n";);
         m_params.setup_AUFLIA(simple_array);
         TRACE(setup, tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
-        m_context.register_plugin(alloc(smt::theory_i_arith, m_context));
+        setup_i_arith();
         setup_arrays();
     }