mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 19:36:20 +00:00
Code Activity

Gate elim_unconstrained in sat.smt preprocess and add regression api_bug test

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/adbdc74f-5aab-4b0e-86a1-4ae2bdb4636e

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-08 17:54:41 +00:00 • committed by GitHub
parent ad9cc8e293
commit 2bebd7ba7a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/test/api_bug.cpp
View file

@ -9,7 +9,14 @@ Copyright (c) 2015 Microsoft Corporation
#include "util/debug.h"
static void test_sat_smt_bv_model_reconstruction() {
Z3_global_param_set("sat.smt", "true");
// Regression: with sat.smt=true, model reconstruction should preserve
// conjunctions of BV comparator predicates.
struct sat_smt_guard {
sat_smt_guard() { Z3_global_param_set("sat.smt", "true"); }
~sat_smt_guard() { Z3_global_param_set("sat.smt", "false"); }
} guard;
(void)guard;
Z3_context ctx = Z3_mk_context(nullptr);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
@ -28,12 +35,13 @@ static void test_sat_smt_bv_model_reconstruction() {
Z3_ast val = nullptr;
ENSURE(Z3_model_eval(ctx, mdl, fml, true, &val));
ENSURE(Z3_get_ast_kind(ctx, val) == Z3_APP_AST);
ENSURE(Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, val))) == Z3_OP_TRUE);
Z3_app val_app = Z3_to_app(ctx, val);
Z3_func_decl val_decl = Z3_get_app_decl(ctx, val_app);
ENSURE(Z3_get_decl_kind(ctx, val_decl) == Z3_OP_TRUE);
Z3_model_dec_ref(ctx, mdl);
Z3_solver_dec_ref(ctx, s);
Z3_del_context(ctx);
Z3_global_param_set("sat.smt", "false");
}
void tst_api_bug() {