ocaml-maint team mailing list archive

[Malte Skoruppa <einheitlix@xxxxxxxxxxxxxx>]

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