debug

src/math/lp/bound_analyzer_on_row.h

@@ -319,6 +319,7 @@ public :
         }
     }   
     static u_dependency* explain_bound_on_var_on_coeff(B* bp, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) {
+        TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";);
         auto& lar = bp->lp();
         int bound_sign = (is_lower_bound ? 1 : -1);
         int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign;

src/math/lp/implied_bound.h

@@ -36,7 +36,7 @@ class implied_bound {
     std::function<u_dependency*(int *)> m_explain_bound = nullptr;
     public:
     // s is expected to be the pointer to lp_bound_propagator.
-    u_dependency* explain(int * s) const { return m_explain_bound(s); }
+    u_dependency* explain_implied(int * s) const { return m_explain_bound(s); }
     void set_explain(std::function<u_dependency*(int *)> f) { m_explain_bound = f; }
     lconstraint_kind kind() const {
         lconstraint_kind k = m_is_lower_bound? GE : LE;

src/math/lp/lar_solver.h

@@ -311,9 +311,9 @@ class lar_solver : public column_namer {
 
     template <typename T>
     void explain_implied_bound(const implied_bound& ib, lp_bound_propagator<T>& bp) {
-        u_dependency* dep = ib.explain((int*)&bp);
+        u_dependency* dep = ib.explain_implied((int*)&bp);
         for (auto ci : flatten(dep))
-            bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients
+            bp.consume(mpq(1), ci); // TODO: flatten should provide the coefficients
         /*
         if (ib.m_is_monic) {
             NOT_IMPLEMENTED_YET();

src/math/lp/lp_bound_propagator.h

@@ -137,14 +137,18 @@ class lp_bound_propagator {
         return n_of_non_fixed <= 1;
     }
 
-
     void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) {
-        add_lower_bound_monic(monic_var, mpq(0), false, [zero_var](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);});
-        add_upper_bound_monic(monic_var, mpq(0), false, [zero_var](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);});
+        auto lambda = [zero_var](int* s) {
+            return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);
+        };
+        TRACE("add_bound", lp().print_column_info(zero_var, tout) << std::endl;);      
+        add_lower_bound_monic(monic_var, mpq(0), false, lambda);
+        add_upper_bound_monic(monic_var, mpq(0), false, lambda);
     }
 
     void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function<u_dependency* (int*)> explain_dep) {
        unsigned k;
+       TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;);
        j = lp().column_to_reported_index(j);
        if (!try_get_value(m_improved_lower_bounds, j, k)) {
             m_improved_lower_bounds[j] = m_ibounds.size();

src/sat/smt/arith_solver.cpp

@@ -253,7 +253,7 @@ namespace arith {
                 first = false;
                 reset_evidence();
                 m_explanation.clear();
-                be.explain((int*)&m_bp);                
+                be.explain_implied((int*)&m_bp);                
             }
             CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
             updt_unassigned_bounds(v, -1);