mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

update add_lemmas to use check-feasible

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-21 19:58:07 -07:00
parent c9d298e57f
commit 4e21e126a8
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/arith_solver.cpp
View file

@ -1484,6 +1484,13 @@ namespace arith {
} }
void solver::add_lemmas() { void solver::add_lemmas() {
if (m_nla->check_feasible()) {
auto is_sat = make_feasible();
if (l_false == is_sat) {
get_infeasibility_explanation_and_set_conflict();
return;
}
}
for (auto const& ineq : m_nla->literals()) { for (auto const& ineq : m_nla->literals()) {
auto lit = mk_ineq_literal(ineq); auto lit = mk_ineq_literal(ineq);
ctx.mark_relevant(lit); ctx.mark_relevant(lit);