Public bug reported:
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
** Affects: alt-ergo (Ubuntu)
Importance: Undecided
Status: New
--
You received this bug notification because you are a member of Debian
OCaml Maintainers, which is subscribed to alt-ergo in Ubuntu.
https://bugs.launchpad.net/bugs/1134259
Title:
Alpha-conversion bug in alt-ergo 0.94
Status in “alt-ergo” package in Ubuntu:
New
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
To manage notifications about this bug go to:
https://bugs.launchpad.net/ubuntu/+source/alt-ergo/+bug/1134259/+subscriptions
_______________________________________________
Mailing list: https://launchpad.net/~ocaml-maint
Post to : [email protected]
Unsubscribe : https://launchpad.net/~ocaml-maint
More help : https://help.launchpad.net/ListHelp
