#5223

Z3Prover · May 2, 2021 · 0810720 · 0810720
1 parent 323e0e6
commit 0810720
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h
@@ -66,7 +66,7 @@ namespace lp_api {
         lp::constraint_index get_constraint(bool b) const { return m_constraints[b]; }
 
         inf_rational get_value(bool is_true) const {
-            if (is_true) 
+            if (is_true == !get_lit().sign()) 
                 return inf_rational(m_value);                         // v >= value or v <= value
             if (m_is_int) {
                 SASSERT(m_value.is_int());

diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
@@ -382,7 +382,7 @@ namespace arith {
         updt_unassigned_bounds(v, +1);
         m_bounds_trail.push_back(v);
         m_bool_var2bound.insert(bv, b);
-        TRACE("arith_verbose", tout << "Internalized " << bv << ": " << mk_pp(atom, m) << "\n";);
+        TRACE("arith_verbose", tout << "Internalized " << lit << ": " << mk_pp(atom, m) << " " << *b << "\n";);
         m_new_bounds.push_back(b);
         //add_use_lists(b);
         return true;
@@ -583,11 +583,10 @@ namespace arith {
         if (e->is_attached_to(get_id()))
             return e->get_th_var(get_id());
         theory_var v = mk_var(e);
-        TRACE("arith", tout << "fresh var: v" << v << " " << mk_pp(n, m) << "\n";);
+        TRACE("arith_verbose", tout << "v" << v << " " << mk_pp(n, m) << "\n";);
         SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty());
         reserve_bounds(v);
         ctx.attach_th_var(e, this, v);
-        TRACE("arith", tout << mk_pp(n, m) << " " << v << "\n";);
         SASSERT(euf::null_theory_var != v);
         return v;
     }

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
@@ -145,7 +145,7 @@ namespace arith {
         bool v_is_int = b.is_int();
         literal lit2 = sat::null_literal;
         bool find_glb = (is_true == (k == lp_api::lower_t));
-        TRACE("arith", tout << "v" << v << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
+        TRACE("arith", tout << lit1 << " v" << v << " val " << val << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
         if (find_glb) {
             rational glb;
             api_bound* lb = nullptr;
@@ -187,6 +187,7 @@ namespace arith {
         m_params.push_back(parameter(m_farkas));
         m_params.push_back(parameter(rational(1)));
         m_params.push_back(parameter(rational(1)));
+        TRACE("arith", tout << lit2 << " <- " << m_core << "\n";);
         assign(lit2, m_core, m_eqs, m_params);
         ++m_stats.m_bounds_propagations;
     }