nuXmv how does it know in initial state that (AF p) & (AF w) is false

Question

I have a question concerning nuXmv solution. I have a simple graph where the initial state is s1 and there are two arcs from s1, one leads to s2, the other to s3. From s2 and s3 there is one arc leading to s1. This is the program in nuXmv which describes the situaiton.

MODULE main
VAR
    s : {s1, s2, s3};  
    p : boolean;
    q : boolean;
    w : boolean;
ASSIGN 
    init(s) := {s1};
    next(s) := case 
        s = s1 : {s2, s3}; 
        s = s2 : s1;
        s = s3 : s1;
    esac;
    p := case 
        s = s2 : TRUE;
        TRUE : FALSE; 
    esac;
    q := case
        s = s1 : TRUE;  
        TRUE : FALSE; 
    esac;
    w := case
       s = s3 : TRUE;
        TRUE : FALSE;
    esac;
CTLSPEC (AF p) & (AF w);
CTLSPEC AG (AF p) & AG (AF w);

I do not understand how nuXmv already in the initial state s1 knows that the formula is false. It does not give a counterexample based on the loop, just immediately in s1 it says that the formula is wrong based on s1. My idea of explanation is that without justice assumptions nuXmv immediately assumes that one of the paths can be never executed. But should it not give a loop as an example? If I only left "CTLSPEC AF p;" nuXmv returns a loop as a counterexample. So why for "AF p & AF w" it only shows state s1 as counterexample?

-- specification (AF p & AF w)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    s = s1
    p = FALSE
    q = TRUE
    w = FALSE