[SATLUG] Re: Prover9 problem

Maurice Fox mauricejfox at gmail.com
Sun May 13 14:04:30 CDT 2012

Solved it.

After some fiddling around with gcc, nm, and whatnot, here's the solution, strange though it may be.

On ubuntu, if test is a program calling for round and ceil, in C and C++ versions

g++ -o test -lm test.cpp

works OK.

gcc -o test -lm test.c


But if I move the -lm parameter like this

gcc -o test test.c -lm

it works OK.  (It also works OK on t he g++ line to move -lm to the end.)

So the problem was in the Makefile.  I edited the Makefile to move -lm after the source/object lists, and everything built OK.  For some reason gcc version 4.6.3 as distributed with the most recent ubuntu this way.  The inconsistency between gcc and g++ is a little strange.  Seems that both invoke ld, but what do I know?


On May 12, 2012, at 12:00 PM, satlug-request at satlug.org wrote:

> Message: 2
> Date: Fri, 11 May 2012 13:39:12 -0500
> From: Maurice Fox <mauricejfox at gmail.com>
> Subject: [SATLUG] Prover9 problem
> To: satlug at satlug.org
> Message-ID: <AF0A3278-FC80-4E20-9FD4-4A433BF006D7 at gmail.com>
> Content-Type: text/plain; charset=us-ascii
> I downloaded the automated theorem prover called Prover9 from its home page and tried to build it under the most recent Ubuntu distro.  It failed on two unresolved symbols in ld:  ceil and round.  
> I moved the tar.gz file over to Mac OS X LION, extracted the source files, and built it just fine.  Ran the tests under make test, completely successful.
> Anybody have any idea why the Linux distro would not resolve those two calls?  They should be part of libm.a, and indeed running ar on libm.a reveals that t here is related content.  For ceil, I get s_ceil.a, s_ceill.a, and s_ceilf.a.  Similarly, for round, I get nine variously decorated .o files.
> Any ideas?
> Regards,
> Maurice

More information about the SATLUG mailing list