[SATLUG] Prover9 problem

Maurice Fox mauricejfox at gmail.com
Fri May 11 13:39:12 CDT 2012

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?


More information about the SATLUG mailing list