hi Alexandre, Seems like the function formula::is_literal() should be marked const: /// \brief Whether the formula is an atomic proposition or its /// negation. bool is_literal() { return (is(op::ap) || // If f is in nenoform, Not can only occur in front of // an atomic proposition. So this way we do not have // to check the type of the child. (is(op::Not) && is_boolean() && is_in_nenoform())); } kind wishes, Ayrat