Skip to content

Add SMT2 regression for minimize + define-fun-rec “canceled” failure#10041

Draft
NikolajBjorner with Copilot wants to merge 3 commits into
masterfrom
copilot/fix-canceled-error-on-minimize
Draft

Add SMT2 regression for minimize + define-fun-rec “canceled” failure#10041
NikolajBjorner with Copilot wants to merge 3 commits into
masterfrom
copilot/fix-canceled-error-on-minimize

Conversation

Copilot AI commented Jul 4, 2026

Copy link
Copy Markdown
Contributor

A reported SMT2 optimization input using define-fun-rec and (minimize ...) was returning (error "...: canceled"), while an inlined equivalent did not. This change adds focused coverage for that exact shape so the behavior remains stable.

  • Regression coverage

    • Added a new test case in src/test/smt2print_parse.cpp that evaluates the reported script through Z3_eval_smtlib2_string.
    • The test ensures this input is handled as a normal solver response (no parser/command error), matching current expected behavior.
  • Test suite integration

    • Wired the new regression into tst_smt2print_parse() so it runs with existing SMT2 parse/eval regression coverage.
char const* spec =
    "(declare-const bound Int)\n"
    "(declare-const a Int)\n"
    "(declare-const b Int)\n"
    "(define-fun-rec f ((x Int) (y Int)) Bool ...)\n"
    "(assert ...)\n"
    "(minimize bound)\n"
    "(check-sat)\n";

test_eval(ctx, spec, false); // expect no error path

Copilot AI changed the title [WIP] Fix 'canceled' error on minimize request in z3 Add SMT2 regression for minimize + define-fun-rec “canceled” failure Jul 4, 2026
Copilot AI requested a review from NikolajBjorner July 4, 2026 20:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

"Canceled" Error on minimize request

2 participants