From d4fa990b6e5c433dc5205dfb1f012385fb7425da Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 25 Apr 2023 13:47:02 -0700
Subject: [PATCH] return diagnostics

---
 src/math/lp/bound_analyzer_on_row.h | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index 6084145c2..0008a0ee9 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -54,32 +54,40 @@ public :
     {}
 
     
-    static void analyze_row(const C & row,
+    static unsigned analyze_row(const C & row,
                             unsigned bj, // basis column for the row
                             const numeric_pair<mpq>& rs,
                             unsigned row_or_term_index,
                             B & bp) {
         bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
-        a.analyze();
+        return a.analyze();
     }
 
 private:
 
-    void analyze() {
+    unsigned analyze() {
+        unsigned num_prop = 0;
         for (const auto & c : m_row) {
             if ((m_column_of_l == -2) && (m_column_of_u == -2))
-                return;
+                return 0;
             analyze_bound_on_var_on_coeff(c.var(), c.coeff());
         }
+        ++num_prop;
         if (m_column_of_u >= 0)
             limit_monoid_u_from_below();
         else if (m_column_of_u == -1)
             limit_all_monoids_from_below();
+        else
+            --num_prop;
 
+        ++num_prop;
         if (m_column_of_l >= 0)
             limit_monoid_l_from_above();
         else if (m_column_of_l == -1)
             limit_all_monoids_from_above();
+        else
+            --num_prop;
+        return num_prop;
     }
 
     bool bound_is_available(unsigned j, bool lower_bound) {