From 9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 Sep 2023 00:52:26 -0700
Subject: [PATCH] debug output with the variable that is fixed and its value

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_nl.h | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index ae0af89ec..0a2b6e938 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -765,10 +765,8 @@ typename theory_arith<Ext>::numeral theory_arith<Ext>::get_monomial_fixed_var_pr
 template<typename Ext>
 expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
     SASSERT(is_pure_monomial(m));
-    for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
-        expr * arg = to_app(m)->get_arg(i);
-        theory_var _var = expr2var(arg);
-        if (!is_fixed(_var))
+    for (expr* arg : *to_app(m)) {
+        if (!is_fixed(expr2var(arg)))
             return arg;
     }
     return nullptr;
@@ -780,7 +778,7 @@ expr * theory_arith<Ext>::get_monomial_non_fixed_var(expr * m) const {
 */
 template<typename Ext>
 bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
-    TRACE("non_linear", tout << "checking whether v" << v << " became linear...\n";);
+    TRACE("non_linear_verbose", tout << "checking whether v" << v << " became linear...\n";);
     if (m_data[v].m_nl_propagated)
         return false; // already propagated this monomial.
     expr * m = var2expr(v);
@@ -819,6 +817,11 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
             ctx.mark_as_relevant(rhs);
         }
         TRACE("non_linear_bug", tout << "enode: " << ctx.get_enode(rhs) << " enode_id: " << ctx.get_enode(rhs)->get_owner_id() << "\n";);
+        IF_VERBOSE(3,
+                   for (auto* arg : *to_app(m)) 
+                       if (is_fixed(expr2var(arg)))
+                           verbose_stream() << mk_pp(arg, get_manager()) << " = " << -k << "\n");
+            
         theory_var new_v = expr2var(rhs);
         SASSERT(new_v != null_theory_var);
         new_lower    = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER);
@@ -906,7 +909,7 @@ bool theory_arith<Ext>::propagate_linear_monomials() {
         return false;
     if (!reflection_enabled())
         return false;
-    TRACE("non_linear", tout << "propagating linear monomials...\n";);
+    TRACE("non_linear_verbose", tout << "propagating linear monomials...\n";);
     bool p = false;
     // CMW: m_nl_monomials can grow during this loop, so
     // don't use iterators.