From f212ba97de1f0829449d09c8f7b9bfc273bacf2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Dec 2019 17:33:54 -0800 Subject: [PATCH] non-termination fix (#106) * fixes to use list bookkeeping Signed-off-by: Nikolaj Bjorner * fix reset logic Signed-off-by: Nikolaj Bjorner * fix non-termination bug in simplifier Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index a5212ad73..294cc3380 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -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"); } }