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