From: trevor_hansen Date: Sun, 28 Nov 2010 02:53:02 +0000 (+0000) Subject: No longer default to -m32, causes too many problems X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=cf73ac1f21d2250769deaae76d8aea8185ba4a37;p=francis%2Fstp.git No longer default to -m32, causes too many problems git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1029 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 955bbae..71292bf 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -16,7 +16,15 @@ #OPTIMIZE = -O3 -march=native -fomit-frame-pointer # Maximum optimization #OPTIMIZE = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE OPTIMIZE = -O3 -g # Maximum optimization -CFLAGS_M32 = -m32 + + +#When solving array problems STP creates lots of objects during the conversion to CNF. If STP is compiled +#as a 32-bit executable, then these objects are about half the size than they are if STP is compiled as a 64-bit +#program. That's because lots of the data in the objects are pointers to other objects. So, if you meet the +#following criteria you may want to enable -m32 on your 64-bit machine: +#1) You are solving array problems. Problems without arrays use another CNF conversion scheme. +#2) You need STP to use about half the memory. +#CFLAGS_M32 = -m32 #-fno-inline CFLAGS_BASE = $(OPTIMIZE)