From da1f0e9e8479741487a59ad68198262c3730081e Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 21 Oct 2011 04:25:19 +0000
Subject: [PATCH] add gcc version information to Configuration, and warn when
 building with v4.5.1 which has a buggy optimizer (resolves bug #266)

---
 README                           | 17 ++++++++++++++++-
 config/gcc_version.m4            |  7 +++++++
 configure.ac                     |  9 +++++++++
 src/util/configuration.cpp       | 15 +++++++++++++++
 src/util/configuration.h         |  2 ++
 src/util/configuration_private.h |  3 ++-
 6 files changed, 51 insertions(+), 2 deletions(-)
 create mode 100644 config/gcc_version.m4

diff --git a/README b/README
index 562ae3938..4188c9d9b 100644
--- a/README
+++ b/README
@@ -10,7 +10,15 @@ installed (see below). Execute,
     make
 
 You can then "make install" to install in the prefix you gave to
-the configure script (/usr/local by default).
+the configure script (/usr/local by default).  ** You should run
+"make check" ** before installation to ensure that CVC4 has been
+built correctly.  In particular, GCC version 4.5.1 seems to have a
+bug in the optimizer that results in incorrect behavior (and wrong
+results) in many builds.  This is a known problem for Minisat, and
+since Minisat is at the core of CVC4, a problem for CVC4.  "make check"
+easily detects this problem (by showing a number of FAILed test cases).
+It is ok if the unit tests aren't run as part of "make check", but all
+system tests and regression tests should pass without incident.
 
 To build a source release, use "make dist"; this will include the
 configure script and all the bits of automake/autoconf/libtool that
@@ -27,12 +35,19 @@ given are minimum versions; more recent versions should be compatible.
 
 GNU C and C++ (gcc and g++), reasonably recent versions
 GNU Make
+GNU Bash
 GMP v4.2 (GNU Multi-Precision arithmetic library)
 libantlr3c v3.2 (ANTLR parser generator)
 Optional: CLN v1.3 (Class Library for Numbers)
 Optional: CUDD v2.4.2 (Colorado University Decision Diagram package)
 Optional: GNU Readline library (for an improved interactive experience)
 
+If "make" is non-GNU on your system, make sure to invoke "gmake" (or
+whatever GNU Make is installed as).  If your usual shell is not
+Bash, the configure script should auto-correct this.  If it does not,
+you'll see strange shell syntax errors, and you may need to explicitly
+set SHELL or CONFIG_SHELL to the location of bash on your system.
+
 CUDD, if desired, must be installed delicately.  The CVC4 configure
 script attempts to auto-detect the locations and names of CUDD headers
 and libraries the way that the Fedora RPMs install them, the way that
diff --git a/config/gcc_version.m4 b/config/gcc_version.m4
new file mode 100644
index 000000000..acd051042
--- /dev/null
+++ b/config/gcc_version.m4
@@ -0,0 +1,7 @@
+# GCC version 4.5.1 builds Minisat incorrectly with -O2
+# and that gives incorrect answers!  Warn the user!
+AC_DEFUN([CVC4_GCC_VERSION], [
+  if expr "$($CC -dumpversion)" : '4\.5\.1' &>/dev/null; then
+    CVC4_INTEGRITY_WARNING="GCC 4.5.1's optimizer is known to make errors building Minisat (and by extension CVC4)"
+  fi
+])# CVC4_GCC_VERSION
diff --git a/configure.ac b/configure.ac
index 9d28d21fa..cabb50706 100644
--- a/configure.ac
+++ b/configure.ac
@@ -208,6 +208,8 @@ AC_PROG_CC
 AC_PROG_CXX
 AC_PROG_INSTALL
 
+CVC4_GCC_VERSION
+
 # [chris 8/24/2010] The user *must* specify --with-cln to get CLN
 # (and, thus, opt in to the GPL dependency).
 
@@ -1062,3 +1064,10 @@ Install into : $prefix
 ${licensewarn}Now just type make, followed by make check or make install, as you like.
 
 EOF
+
+if test -n "$CVC4_INTEGRITY_WARNING"; then
+  AC_MSG_WARN([])
+  AC_MSG_WARN($CVC4_INTEGRITY_WARNING)
+  AC_MSG_WARN([Please run "make check" after building to ensure integrity of the binary and library])
+  AC_MSG_WARN([])
+fi
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 7225b8108..3164b75a5 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -186,4 +186,19 @@ string Configuration::getSubversionId() {
   return ss.str();
 }
 
+string Configuration::getCompiler() {
+  stringstream ss;
+#ifdef __GNUC__
+  ss << "GCC";
+#else /* __GNUC__ */
+  ss << "unknown compiler";
+#endif /* __GNUC__ */
+#ifdef __VERSION__
+  ss << " version " << __VERSION__;
+#else /* __VERSION__ */
+  ss << ", unknown version";
+#endif /* __VERSION__ */
+  return ss.str();
+}
+
 }/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index b4caf842c..c3040f3fb 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -99,6 +99,8 @@ public:
   static bool hasSubversionModifications();
   static std::string getSubversionId();
 
+  static std::string getCompiler();
+
 };/* class Configuration */
 
 }/* CVC4 namespace */
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 13347d970..abff15b3b 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -114,7 +114,8 @@ This is CVC4 version " CVC4_RELEASE_STRING ) + \
     ( ::CVC4::Configuration::isSubversionBuild() \
         ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \
         : ::std::string("") \
-    ) + "\n\n\
+    ) + "\n\
+compiled with " + ::CVC4::Configuration::getCompiler() + "\n\n\
 Copyright (C) 2009, 2010, 2011\n\
   The ACSys Group\n\
   Courant Institute of Mathematical Sciences\n\
-- 
2.30.2