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