GitLab

Since the same name cannot be reused for several theories in a single
file, the line-number suffix can be scrapped. This makes it easier to
reference a given theory from a human-written documentation.

The final underscore is kept to avoid ambiguities.

RFC 3986 states that the allowed characters are:

   fragment      = *( pchar / "/" / "?" )
   pchar         = unreserved / pct-encoded / sub-delims / ":" / "@"
   pct-encoded   = "%" HEXDIG HEXDIG
   unreserved    = ALPHA / DIGIT / "-" / "." / "_" / "~"
   sub-delims    = "!" / "$" / "&" / "'" / "(" / ")"
                 / "*" / "+" / "," / ";" / "="

Use coercions on the argument of an application even when the callee is not a symbol (partly fixes #72).

Translate BV*.of_int to int2bv for CVC4, since the bv1234 syntax rejects constants that are too large.

Note: while int2bv could be used as a "syntax function", this breaks too
many examples because of timeouts (or unexpected successes).

This is important for the "loose" fields: mutable components of
a private type which can be modified without a direct write into
the containing object. These subcomponents can be modified by
abstract functions, and these modifications are actually visible,
since a refinement of a private type can make ghost fields non-ghost.

Example:

bin/why3 ide --batch "type next;view source;type alt-ergo;wait 5;snap foo.png" examples/logic/hello_proof.why