mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

bugfixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-07 15:12:15 -07:00
parent f41769cdcf
commit 5340b23d1b
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_solver.cpp
View file

@ -2796,6 +2796,8 @@ namespace nlsat {
unsigned sz = m_clauses.size(); unsigned sz = m_clauses.size();
while (true) { while (true) {
IF_VERBOSE(3, display(verbose_stream() << "subsuming\n"));
subsumption_simplify(); subsumption_simplify();
while (elim_uncnstr()) while (elim_uncnstr())
@ -2919,7 +2921,7 @@ namespace nlsat {
lits[1] = qgt; lits[1] = qgt;
mk_clause(2, lits, false, asum); mk_clause(2, lits, false, asum);
lits[0] = qlt; lits[0] = qlt;
lits[1] = plt; lits[1] = pgt;
mk_clause(2, lits, false, asum); mk_clause(2, lits, false, asum);
} }
break; break;
@ -3371,6 +3373,8 @@ namespace nlsat {
for (auto lit2 : c) for (auto lit2 : c)
if (lit2 != lit) if (lit2 != lit)
lits.push_back(lit2); lits.push_back(lit2);
if (lits.empty())
return false;
auto cls = mk_clause(lits.size(), lits.data(), false, a); auto cls = mk_clause(lits.size(), lits.data(), false, a);
if (cls) if (cls)
compute_occurs(*cls); compute_occurs(*cls);