mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #4225

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-06 10:35:16 -07:00
parent bbaedbcccc
commit 93004a9d49
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/nlsat/nlsat_solver.cpp
View file

@ -947,10 +947,13 @@ namespace nlsat {
} }
void mk_clause(unsigned num_lits, literal const * lits, assumption a) { void mk_clause(unsigned num_lits, literal const * lits, assumption a) {
SASSERT(num_lits > 0);
_assumption_set as = nullptr; _assumption_set as = nullptr;
if (a != nullptr) if (a != nullptr)
as = m_asm.mk_leaf(a); as = m_asm.mk_leaf(a);
if (num_lits == 0) {
num_lits = 1;
lits = &false_literal;
}
mk_clause(num_lits, lits, false, as); mk_clause(num_lits, lits, false, as);
} }