diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-21 04:25:19 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-21 04:25:19 +0000 |
| commit | da1f0e9e8479741487a59ad68198262c3730081e (patch) | |
| tree | 2f764fcd4574ddefd62ad0da44b1bec64df685dd /README | |
| parent | 19b3adf57987584096ca59dc9852fb9573ee1715 (diff) | |
add gcc version information to Configuration, and warn when building with v4.5.1 which has a buggy optimizer (resolves bug #266)
Diffstat (limited to 'README')
| -rw-r--r-- | README | 17 |
1 files changed, 16 insertions, 1 deletions
@@ -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 |