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

Fix sat.smt invalid BV comparator model by disabling elim_unconstrained in sat.smt preprocess

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:52:00 +00:00 • committed by GitHub
parent 92094ed10f
commit ad9cc8e293
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 35 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/solver/solver_preprocess.cpp
View file

@ -42,6 +42,7 @@ Notes:
#include "ast/simplifiers/bound_simplifier.h"
#include "ast/simplifiers/cnf_nnf.h"
#include "params/smt_params.h"
#include "params/sat_params.hpp"
#include "solver/solver_preprocess.h"
#include "qe/lite/qe_lite_tactic.h"
@ -59,10 +60,11 @@ void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, de
return r;
};
smt_params smtp(p);
sat_params satp(p);
s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st));
if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st));
if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st));
if (smtp.m_elim_unconstrained && !satp.smt()) s.add_simplifier(alloc(elim_unconstrained, m, st));
if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st));
if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifier(m, p, st));
@ -88,4 +90,3 @@ void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, de
//
}

35
src/test/api_bug.cpp
View file

@ -6,6 +6,35 @@ Copyright (c) 2015 Microsoft Corporation
#include<stdio.h>
#include "api/z3.h"
#include "util/debug.h"
static void test_sat_smt_bv_model_reconstruction() {
Z3_global_param_set("sat.smt", "true");
Z3_context ctx = Z3_mk_context(nullptr);
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_sort bv4 = Z3_mk_bv_sort(ctx, 4);
Z3_ast k = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "k"), bv4);
Z3_ast one = Z3_mk_unsigned_int64(ctx, 1, bv4);
Z3_ast three = Z3_mk_unsigned_int64(ctx, 3, bv4);
Z3_ast cmp[2] = { Z3_mk_bvuge(ctx, k, one), Z3_mk_bvult(ctx, k, three) };
Z3_ast fml = Z3_mk_and(ctx, 2, cmp);
Z3_solver_assert(ctx, s, fml);
ENSURE(Z3_solver_check(ctx, s) == Z3_L_TRUE);
Z3_model mdl = Z3_solver_get_model(ctx, s);
Z3_model_inc_ref(ctx, mdl);
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_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() {
unsigned vmajor, vminor, vbuild, vrevision;
@ -46,7 +75,7 @@ void tst_api_bug() {
printf("model : %s\n", ms);
Z3_solver_dec_ref(ctx, s);
Z3_del_config(cfg);
Z3_del_context(ctx);
Z3_del_context(ctx);
test_sat_smt_bv_model_reconstruction();
}