Octagonal_Shape::affine_image seems a bit too imprecise when treating assignments of the form Y = -Y + c.<br><br>Here's the code involved:<br><br>          // Here `w_coeff == -denominator'.<br>          // Remove the binary constraints on `var'.<br>
          forget_binary_octagonal_constraints(var_id);<br>          const Row_Iterator m_begin = matrix.row_begin();<br>          Row_Iterator m_iter = m_begin + n_var;<br>          N& m_v_cv = (*m_iter)[n_var+1];<br>
          ++m_iter;<br>          N& m_cv_v = (*m_iter)[n_var];<br>          // Swap the unary constraints on `var'.<br>          std::swap(m_v_cv, m_cv_v);<br>          // Strong closure is not preserved.<br>          reset_strongly_closed();<br>
          if (b != 0) {<br>            // Translate the unary constraints on `var',<br>            // adding or subtracting the value `b/denominator'.<br>            PPL_DIRTY_TEMP(N, d);<br>            div_round_up(d, b, denominator);<br>
            mul_2exp_assign_r(d, d, 1, ROUND_UP);<br>            add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP);<br>            PPL_DIRTY_TEMP(N, minus_d);<br>            div_round_up(minus_d, b, minus_den);<br>            mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP);<br>
            add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP);<br>          }<br>          incremental_strong_closure_assign(var);<br>         }<br><br>This approach that discards all old binary constraints on the assigned variable looks a little too naive to me. Consider for instance this assigment sequence:<br>
<br>X = Y;<br>Y = -Y;<br><br>The octagonal domain will not be able to deduce X + Y = 0 as I would expect. A similar problem probably exists for BD Shapes.<br>