team-worthwhile/worthwhile — Issue #33: cannot save because of incompatible encodings
Author: danielbruns
Created: 2012-02-14 10:31:46+00:00
State: open

I tried to save the following text in a worthwhile file, but then an error message popped up: Some characters cannot be mapped using "ANSI_X3.4-1968" character encoding. I used the binary version on Linux x86_64.

Integer[] a
Integer x
Integer length
_assume length > 0
//_assume ∀ Integer j (length ≤ j) : a[j] == 0
x := a[0]
Integer i := 1
while (i < length) {
if (x < a[i]) {
x := a[i]
}
i := i + 1
}
_ensures ∀ Integer i (0 ≤ i ∧ i < length(a)) : x ≥ a[i]
_ensures ∃ Integer i (0 ≤ i ∧ i < length(a)) : x == a[i]