Output of KIND2

[kumori123]

Hi，I noticed that In recent version of KIND2，the output rename the property into auto-generated string like InvProp[l84c3] instead of property itself. Is there any option that can change the property name back to property itself?
Thank you!

[daniel-larraz]

No, there isn't. Since the introduction of dedicated syntax for checking reachability properties in version 1.9.0, the boolean expression alone no longer uniquely identifies the property being checked. For instance, both check P and check reachable P use the same boolean expression, but they represent different proof obligations. However, you can name a property so that you can quickly recognize which property is. For example: check "I1" P and check reachable "R1" P