Alpha-conversion bug in alt-ergo 0.94
Bug #1134259 reported by
Malte Skoruppa
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| alt-ergo (Ubuntu) |
Fix Released
|
Undecided
|
Unassigned | ||
Bug Description
There is a rather serious alpha-conversion bug in alt-ergo 0.94 (available in Ubuntu 12.10). Try this:
goal absurd: (forall b:bool. b = true) or (forall b:bool. b = false)
Observed behavior: alt-ergo says this is valid.
Expected behavior: alt-ergo should not be able to prove this.
Note that this is fixed in alt-ergo 0.95, however this version is not available in the Ubuntu repos.
Best,
Malte
Revision history for this message
| Gianfranco Costamagna (costamagnagianfranco) wrote | #1 |
| Changed in alt-ergo (Ubuntu): | |
| status: | New → Incomplete |
| status: | Incomplete → Fix Released |
To post a comment you must log in.
this is fixed since a long time...