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