From ad9300c75f567eb52e4b3932a726283d19efaee6 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 13 Jul 2026 03:07:15 +0000
Subject: [PATCH] Fix api_datalog test: use fresh contexts for each
 Z3_eval_smtlib2_string call

---
 src/test/api_datalog.cpp | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/test/api_datalog.cpp b/src/test/api_datalog.cpp
index 3b0011a4b3..f57e0c0419 100644
--- a/src/test/api_datalog.cpp
+++ b/src/test/api_datalog.cpp
@@ -66,6 +66,10 @@ void tst_api_datalog() {
 
     // Regression test for Spacer model construction on ADT CHCs
     {
+        Z3_config cfg2 = Z3_mk_config();
+        Z3_context ctx2 = Z3_mk_context(cfg2);
+        Z3_del_config(cfg2);
+
         char const* chc =
             "(set-logic HORN)\n"
             "(set-option :fp.engine spacer)\n"
@@ -85,13 +89,18 @@ void tst_api_datalog() {
             "      false)))\n"
             "(check-sat)\n";
 
-        Z3_string response = Z3_eval_smtlib2_string(ctx, chc);
+        Z3_string response = Z3_eval_smtlib2_string(ctx2, chc);
         ENSURE(response != nullptr);
-        ENSURE(Z3_get_error_code(ctx) == Z3_OK);
+        ENSURE(Z3_get_error_code(ctx2) == Z3_OK);
+        Z3_del_context(ctx2);
     }
 
     // Regression test for assertion violation in Spacer QE projection (#3845)
     {
+        Z3_config cfg3 = Z3_mk_config();
+        Z3_context ctx3 = Z3_mk_context(cfg3);
+        Z3_del_config(cfg3);
+
         char const* chc = R"(
 (set-logic HORN)
 (set-option :fp.xform.inline_eager false)
@@ -224,9 +233,10 @@ void tst_api_datalog() {
 (check-sat)
 )";
 
-        Z3_string response = Z3_eval_smtlib2_string(ctx, chc);
+        Z3_string response = Z3_eval_smtlib2_string(ctx3, chc);
         ENSURE(response != nullptr);
-        ENSURE(Z3_get_error_code(ctx) == Z3_OK);
+        ENSURE(Z3_get_error_code(ctx3) == Z3_OK);
+        Z3_del_context(ctx3);
     }
 
     Z3_del_context(ctx);