mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Update nla_core.cpp

Browse source
This commit is contained in:
Lev Nachmanson 2020-02-14 17:37:26 -08:00
parent 697fd37d26
commit 0db112ef8f
1 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/nla_core.cpp
View file

@ -1230,11 +1230,7 @@ rational core::val(const factorization& f) const {
}
void core::add_empty_lemma() {
m_lemma_vec->push_back(lemma());
if (lp_settings().stats().m_nla_calls == 5 && m_lemma_vec->size() == 11) {
TRACE("nla_solver", tout << "bad lemma\n";);
}
m_lemma_vec->push_back(lemma());
}
void core::negate_relation(unsigned j, const rational& a) {