When you apply a full_case synthesis attribute to a case statement header, it instructs tools to interpret unspecified states as “don’t care” values. The Quartus® II software infers additional logic to represent the "don't care" states. This additional logic can be different from the logic inferred by the formal verification tool, resulting in formal verification mismatches.
To overcome the mismatches, define all the states in the state machine.
Refer to the Recommended HDL Coding Styles (PDF) chapter in volume 1 of the Quartus II handbook for more information on state machine coding guidelines.