A model with Safety annex were verified true in AGREE for all top level properties without turning on "Perform Safety Analysis during AGREE Verification". After turning on the safety analysis, some of the top level properties failed, and the counterexample show the effects caused by fault injection. However, the fault node(s) do not show activated in the counterexample.
E.g., https://www-users.cs.umn.edu/svn_amase/examples/Byzantine_Test (SVN revision 86)
A model with Safety annex were verified true in AGREE for all top level properties without turning on "Perform Safety Analysis during AGREE Verification". After turning on the safety analysis, some of the top level properties failed, and the counterexample show the effects caused by fault injection. However, the fault node(s) do not show activated in the counterexample. E.g., https://www-users.cs.umn.edu/svn_amase/examples/Byzantine_Test (SVN revision 86)