SPIN verification breaks when narrowing implementation contract

[TPolzer]

The following verifies fine with -m native:

model[NuSMV] client("impl.smv","client") {
  input bool proceed;
  output enum { nc, cs } st; 
  init st 'nc;
  // Basic behaviour
  automaton {
    init final state nc {
      st = 'nc;
      transition[proceed] cs; 
      transition nc; 
    }   
    final state cs {
      st = 'cs;
      transition nc; 
      transition cs; 
    }   
  };  
  // Constrained behaviour
  always (st = 'cs => (st = 'cs until[4cy] st = 'nc));
}

model[NuSMV] server("impl.smv","server") {
  input enum { nc, cs }^2 procstates;
  output bool^2 procouts;
  init procouts [false,false];
  always (procstates[1] != 'cs and procouts = [true,false])
         or (procouts = [false,false]);
}

instance client c0; 
instance client c1; 

instance server s;

connect c0.st s.procstates[0];
connect c1.st s.procstates[1];

connect s.procouts[0] c0.proceed;
connect s.procouts[1] c1.proceed;

verify {
  //liveness
  always (c0.st = 'cs => finally c0.st = 'nc);
}

while this fails:

model[NuSMV] client("impl.smv","client") {
  input bool proceed;
  output enum { nc, cs } st; 
  init st 'nc;
  // Basic behaviour
  automaton {
    init final state nc {
      st = 'nc;
      transition[proceed] cs; 
      transition nc; 
    }   
    final state cs {
      st = 'cs;
      transition nc; 
      transition cs; 
    }   
  };  
  // Constrained behaviour
  always (st = 'cs => (st = 'cs until[4cy] st = 'nc));
  always (st = 'nc) => ((next st = 'cs) => next next st = 'cs);
}

model[NuSMV] server("impl.smv","server") {
  input enum { nc, cs }^2 procstates;
  output bool^2 procouts;
  init procouts [false,false];
  always (procstates[1] != 'cs and procouts = [true,false])
         or (procouts = [false,false]);
}

instance client c0; 
instance client c1; 

instance server s;

connect c0.st s.procstates[0];
connect c1.st s.procstates[1];

connect s.procouts[0] c0.proceed;
connect s.procouts[1] c1.proceed;

verify {
  //liveness
  always (c0.st = 'cs => finally c0.st = 'nc);
}

Where the only difference is this line in the client contract:

always (st = 'nc) => ((next st = 'cs) => next next st = 'cs);

Since this only narrows down the number of valid traces for the client it cannot possibly invalidate the global goal.

[hgoes]

Thanks for the report. The SMT-BMC target does indeed find nothing wrong with the new contract, so it must be an implementation bug in the SPIN target. Unfortunately I don't have time to look into it right now, so I have to leave it open for at least a few days :(