From 98bfbc2d624d8fc7126268363d1fb1c5d072b062 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Dec 2019 13:59:45 -0800
Subject: [PATCH] tidy

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_pdd.cpp           |  4 ++--
 src/math/grobner/pdd_grobner.cpp | 13 ++++---------
 2 files changed, 6 insertions(+), 11 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 6359302d5..9b38424a4 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -441,7 +441,7 @@ namespace dd {
     pdd_manager::PDD pdd_manager::make_node(unsigned lvl, PDD l, PDD h) {
         m_is_new_node = false;
         if (is_zero(h)) return l;
-        SASSERT(is_val(l) || level(l) <= lvl);
+        SASSERT(is_val(l) || level(l) < lvl);
         SASSERT(is_val(h) || level(h) <= lvl);
         pdd_node n(lvl, l, h, tree_size(l) + tree_size(h) + 1);
         return insert_node(n);
@@ -706,7 +706,7 @@ namespace dd {
             PDD lo = n.m_lo;
             PDD hi = n.m_hi;
             if (hi == 0) continue; // it is a value
-            ok &= is_val(lo) || level(lo) <= lvl;
+            ok &= is_val(lo) || level(lo) < lvl;
             ok &= is_val(hi) || level(hi) <= lvl;
             ok &= is_val(lo) || !m_nodes[lo].is_internal();
             ok &= is_val(hi) || !m_nodes[hi].is_internal();
diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index 52521998c..a92c186df 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -72,16 +72,12 @@ namespace dd {
     
     grobner::equation* grobner::pick_next() {
         equation* eq = nullptr;
-        ptr_buffer<equation> to_delete;
         for (auto* curr : m_to_simplify) {
-            if (!eq|| is_simpler(*curr, *eq)) {
+            if (!eq || is_simpler(*curr, *eq)) {
                 eq = curr;
             }
         }
-        for (auto* e : to_delete)
-            del_equation(e);
-        if (eq) 
-            m_to_simplify.erase(eq);
+        if (eq) m_to_simplify.erase(eq);
         return eq;
     }
 
@@ -174,10 +170,9 @@ namespace dd {
         if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return;
         m_stats.m_superposed++;
         if (r.is_zero()) return;
-        unsigned idx = m_equations.size();
-        equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), idx);
+        equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), m_equations.size());
         update_stats_max_degree_and_size(*eq);
-        if (r.is_val()) set_conflict();
+        check_conflict(*eq);
         m_to_simplify.insert(eq);
     }