Skip to content

gWhy tries to use Alt-Ergo even if not installed

ID0000037: This issue was created automatically from Mantis Issue 37. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000037 Frama-C Plug-in > jessie public 2009-04-07 2009-12-03
Reporter virgile Assigned To cmarche Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Lithium-20081201 Target Version - Fixed in Version -

Description :

[bug 7532 from old bts, reported by Boris Hollas] gWhy correctly identifies that

  • Simplify is installed
  • Alt-Ergo is not installed on my system.

Although Simplify is pre-selected in the menu "Proof", gWhy tries to run Alt-Ergo when I invoke "Prove all obligations".

Environment: Windows XP, cygwin with bash

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information