At the moment, duplicate properties are skipped silently. We should inform the user that a given property is being skipped. This could be especially useful in the case the user doesn't know 2 properties are equivalent (for example, in the case that we rewrite a property underwater). I encountered this when writing some very basic properties for bug hunting, and to my surprise not all properties showed up on the output. **Model:** ``` property p_1 = Pmin(<> true); property p_2 = Pmin(<> true); property p_3 = Pmin(<> false); process RandomWalk() { int i; tau palt { :6: {= i = (i + 1) % 5 =}; RandomWalk() :4: {= =}; RandomWalk() } } RandomWalk() ``` **Output:** ``` [...] + State space exploration State size: 1 bytes States: 1 Transitions: 1 Branches: 2 Rate: 15 states/s Time: 0.1 s + Property p_1 Probability: 1 Bounds: [1, 1] Time: 0.0 s + Value iteration Final error: 0 Iterations: 1 Time: 0.0 s + Property p_3 Probability: 0 Bounds: [0, 0] Time: 0.0 s + Value iteration Final error: 0 Iterations: 1 Time: 0.0 s ```