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 api_datalog test: reuse of Z3_context across set-logic calls (#10101)

Browse source 
The `api_datalog` unit test was failing in CI with `"the logic has
already been set"`. Two consecutive regression tests shared a single
`Z3_context`, but both called `Z3_eval_smtlib2_string` with `(set-logic
HORN)` — the second call always fails because context logic state is
permanent.

## Changes

- **`src/test/api_datalog.cpp`**: Give each
`Z3_eval_smtlib2_string`-based regression test its own
`Z3_config`/`Z3_context`, destroyed immediately after the test block.
The outer context is retained only for the two tests that don't invoke
the SMT-LIB evaluator.

```cpp
// Before: both blocks shared `ctx`, second (set-logic HORN) always errored
Z3_string response = Z3_eval_smtlib2_string(ctx, chc1);  // sets HORN logic
Z3_string response = Z3_eval_smtlib2_string(ctx, chc2);  // ERROR: logic already set

// After: each block owns its context
Z3_config cfg2 = Z3_mk_config();
Z3_context ctx2 = Z3_mk_context(cfg2);
Z3_del_config(cfg2);
Z3_string response = Z3_eval_smtlib2_string(ctx2, chc2);
Z3_del_context(ctx2);
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-12 20:32:02 -07:00 • committed by GitHub
parent 136a653ade
commit 087eeaf33c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/test/api_datalog.cpp
View file

@ -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);