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

non-termination fix (#106)

Browse source 
* fixes to use list bookkeeping

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix reset logic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix non-termination bug in simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-28 17:33:54 -08:00 committed by Lev Nachmanson
parent 014e5158c0
commit f212ba97de
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1445,6 +1445,10 @@ void core::check_pdd_eq(const dd::grobner::equation* e) {
};
if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
m_pdd_grobner.get_stats().m_conflicts++;
IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
}
else {
IF_VERBOSE(2, verbose_stream() << "grobner miss\n");
}
}