mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-09 23:42:21 +00:00
Code Activity

Fix crossed-bound dependency assertion and add regression for #10436

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-08-07 06:28:59 +00:00 • committed by GitHub
parent 287e78b7bb
commit 6b07277cf0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 18 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/lar_solver.cpp
View file

@ -2865,12 +2865,12 @@ namespace lp {
void lar_solver::set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep) {
if (m_imp->m_crossed_bounds_column != null_lpvar) return; // already set
SASSERT(m_imp->m_crossed_bounds_deps == nullptr);
set_status(lp_status::INFEASIBLE);
m_imp->m_crossed_bounds_column = j;
const auto& ul = m_imp->m_columns[j];
u_dependency* bdep = lower_bound? ul.lower_bound_witness() : ul.upper_bound_witness();
SASSERT(bdep != nullptr);
m_imp->m_crossed_bounds_deps = dep_manager().mk_join(bdep, dep);
SASSERT(m_imp->m_crossed_bounds_deps != nullptr);
set_status(lp_status::INFEASIBLE);
TRACE(dio, tout << "crossed_bound_deps:\n"; print_explanation(tout, flatten(m_imp->m_crossed_bounds_deps)) << "\n";);
}
const indexed_uint_set & lar_solver::touched_rows() const { return m_imp->m_touched_rows; }
@ -3098,4 +3098,3 @@ namespace lp {
out << "(exit)\n";
}
} // namespace lp

16
src/test/smt2print_parse.cpp
View file

@ -405,4 +405,20 @@ void tst_smt2print_parse() {
ENSURE(resp.find("unknown") == std::string::npos);
}
// Regression test for GitHub issue #10436:
// Do not crash with crossed bounds where one side has no bound witness.
{
char const* spec =
"(assert (or (forall ((x Int)) (and (= 1 x) (= 0 (+ 1 (* x x)))))))\n"
"(check-sat)\n";
Z3_context ctx = Z3_mk_context(nullptr);
Z3_set_error_handler(ctx, setError);
is_error = false;
std::string resp = Z3_eval_smtlib2_string(ctx, spec);
Z3_del_context(ctx);
std::cout << "Issue #10436 response: " << resp << "\n";
ENSURE(!is_error);
ENSURE(resp.find("unsat") != std::string::npos);
}
}