id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
62	infinite loop when verifying simpleMPSpec	ywei	Stephen Siegel	"command:
tass verify -verbose simpleMPSpec.mmp -np 2
The infinite loop will occur when the verifier checks all the states and want to return from program.

...
Step 19: State 18 -- simpleMPSpec.mmp line 22 proc 1 [main@10->main@11] ""t = m;"" -> State 19

begin State 19
  onStack = true;
  seen = true;
  pathCondition : true
  begin model state
    begin shared variables
      s = 0;
      t = 5;
    end shared variables;
    begin process 0
    end process 0;
    begin process 1
      begin stack frame 0
        function : main;
        location : 11;
        i = 5;
        j = 7;
        k = 0;
        m = 5;
      end stack frame 0;
    end process 1;
  end model state
end State 19

Step 20: State 19 -- simpleMPSpec.mmp proc 1 [main@11->main@12] ""[implicit return]""
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid

It seems the transition system keeps adding the implicit return as a new transition. But the DfsSearcher thinks it has seen the state before. So the program loops forever.
"	defect	closed	major		search	1.0	fixed