Escape string attributes in session files
When a goal contains characters such as &
or <
, the session file becomes corrupted and cannot be opened any more. For example here:
Module Test
use int.Int
let function (&) (n: int): int
ensures { result = n + 1 }
= n + 1
end
The corruption is due to unescaped characters in the expl
attribute of the goal:
<goal name="VC infix &" expl="VC for infix &" proved="true">
This patch escapes string attributes including expl
.