Received: from antares.mcs.anl.gov (mcs.anl.gov [140.221.9.6]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id AAA17488 for <jharriso@ra.abo.fi>; Wed, 13 Dec 1995 00:02:16 +0200
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
	id PAA12365 for qed-out; Tue, 12 Dec 1995 15:47:29 -0600
Received: from lutra (lutra.mcs.anl.gov [140.221.5.137]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
	id PAA12360 for <qed@mcs.anl.gov>; Tue, 12 Dec 1995 15:47:19 -0600
From: William McCune <mccune@mcs.anl.gov>
Date: Tue, 12 Dec 1995 15:47:17 -0600
Message-Id: <199512122147.PAA01693@lutra>
To: qed@mcs.anl.gov
Subject: proof double checking and verified compilers
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


A funny QED-motivating thing happened to me yesterday:
(1) Compile Otter unoptimized, it seems to run correctly
and gets a correct proof.  (2) Compile Otter optimized,
run it on the same input and get an unsound proof---no core
dump, no error, proof "looks" ok, but has a bad
inference.  (Compiler is gcc 2.5.8.)

    Bill McCune