safe state machines

I continue this interesting post with an example I don't understand.

I simulated the following FSM

 
module FSMexampleSafe2 (clk,reset,read_write, ready, oe);
input clk,reset,read_write, ready;
output oe;
wire clk,reset,read_write, ready;
reg oe;
reg  ac_state /* synthesis syn_encoding="user,safe" */;
parameter     // One-hot coding
idle =6'b000001,      decision=6'b000010,       read  =6'b000100,
write=6'b001000,      dummy1  =6'b010000,   dummy2=6'b100000;
always @(posedge clk)  // state register and logic for next state
begin
if (reset)
 ac_state <= idle;
else
 case (ac_state)
 idle:    ac_state <= (ready)      ? decision : idle;
 decision:   ac_state <= (read_write) ? read : write;
 read:    ac_state <= (ready)      ? idle : read;
 write:    ac_state <= (ready)      ? idle : write;
   dummy1:    ac_state <= dummy2;
   dummy2:    ac_state <= dummy1;
// default: ac_state <= idle;
 endcase
end
always @(ac_state)  // Moore logic for output
begin
case (ac_state)
 idle, decision, write:    oe<=1'b0; 
 read:   oe<=1'b1;
 default:  oe<=1'b0;
endcase
end
endmodule

and run the Modelsim RTL simulation with the following testbench

--- Quote Start ---

`timescale 1ns/1ps

module FSMexampleSafe2_tb();

parameter period=30;

reg clk,reset,read_write, ready;

wire oe;

FSMexampleSafe2 UUT(.clk(clk),.reset(reset),.read_write(read_write),

.ready(ready),.oe(oe));

always

begin

clk=0;# (period/2.0);

clk=1;# (period/2.0);

end

initial

begin

reset=1;{read_write, ready}=2'b00;# period;

reset=0;{read_write, ready}=2'b00;# (1*period);

{read_write, ready}=2'b01;# period;

{read_write, ready}=2'b10;# period;

{read_write, ready}=2'b01;# (2*period);

{read_write, ready}=2'b00;# period;

force UUT.ac_state = 6'b010000;# period;

release UUT.ac_state;# (4*period)

force UUT.ac_state = 6'b000000;# period;

release UUT.ac_state;# (3*period)

$stop;

end

endmodule

--- Quote End ---

The FSM is recognized by the synthesizer and the state machine viewer shows a FSM with 5 states.

The message windows confirms that the FSM is being implemented as 'safe'.

Following what is written in this post the synthesizer should:

1) remove dummy1 and dummy2 states that are not reachable.

2) gracefully recover from illegal states.

The RTL simulation shows, instead:

1) when forced in dummy1 state, the FSM hangs in the dummy1-dummy2 infinite cycle hence dummy1 and dummy2 have not been removed.

2) when froced in the illegal '000000' state, the FSM hangs there forever.

Can someone explain where's my error?

Please note that the default instruction in the next state block is commented.