From 00277ba3cf9d41bc6376d6d214d754765c4bff53 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 15 Mar 2025 18:17:27 -0700
Subject: [PATCH] nits

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/dioph_eq.cpp | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index e3a14ae22..48d50ac81 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -1397,7 +1397,7 @@ namespace lp {
             std_vector<unsigned> sorted_changed_terms;
             std_vector<unsigned> processed_terms;
             m_tightened_columns.reset();
-            for (unsigned j: m_terms_to_tighten) {
+            for (unsigned j: m_terms_to_tighten) {                
                 if (j >= lra.column_count() ||
                     !lra.column_has_term(j) ||
                     lra.column_is_free(j) ||
@@ -1423,14 +1423,19 @@ namespace lp {
             );
             for (unsigned j : sorted_changed_terms) {
                 m_terms_to_tighten.remove(j);
-                r = tighten_bounds_for_term_column(j);
-                if (r != lia_move::undef) {
+                auto r0 = tighten_bounds_for_term_column(j);
+                if (r0 == lia_move::conflict) {
+                    r = r0;
                     break;
-                }                
+                }
+                else if (r0 == lia_move::continue_with_check)
+                    r = r0;
+                else if (r0 == lia_move::branch && r == lia_move::undef)
+                    r = r0;
             }
-            for (unsigned j :processed_terms) {
+            for (unsigned j : processed_terms) 
                 m_terms_to_tighten.remove(j);
-            }
+            TRACE("dio", tout << r << "\n");
             return r;
         }
 
@@ -1802,10 +1807,10 @@ namespace lp {
             lia_move ret = process_f(f_vector);
             if (ret != lia_move::undef)
                 return ret;
-            TRACE("dio", print_S(tout););
             ret = tighten_terms_with_S();
             if (ret == lia_move::conflict) 
                 lra.stats().m_dio_tighten_conflicts++;
+            TRACE("dio", print_S(tout););
             return ret;
         }