Underscore as the last character of a logic function has the potential to cause Why3 errors

[sarsko]

#[predicate]
pub fn ex() -> bool { true }

#[predicate]
pub fn ex_() -> bool { true }

#[logic]
fn lemma() {
    ex();
}

causes the error File "../ex.mlcfg", line 52, characters 12-18: unbound function or predicate symbol 'Ex0.ex'

The same applies no matter how many _s one appends to the second predicate.

Note that ex_() is perfectly usable, and the following:

#[predicate]
pub fn ex() -> bool { true }

#[logic]
fn lemma() {
    ex();
}

#[predicate]
pub fn ex_() -> bool { true }

and

#[logic]
fn lemma() {
    ex();
}

#[predicate]
pub fn ex() -> bool { true }

#[predicate]
pub fn ex_() -> bool { true }

are allowed.

[xldenis]

This sucks, clearly somewhere along the way I drop the trailing _.

[xldenis]

Fixed.