[SATLUG] Prover9 problem

Bruce Dubbs bruce.dubbs at gmail.com
Fri May 11 13:48:45 CDT 2012

Maurice Fox wrote:
> 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.

Does the link line have -lm in it?

$ nm -a /usr/lib/libm.so |grep ceil
000089a0 t __ceil
00010480 t __ceilf
00017dd0 t __ceill
000089a0 W ceil
00010480 W ceilf
00017dd0 W ceill

$ nm -a /usr/lib/libm.so |grep round
0000d4d0 t __llround
000148c0 t __llroundf
0001c820 t __llroundl
0000d3f0 t __lround
00014810 t __lroundf
0001c760 t __lroundl
0000b250 t __round
00012a10 t __roundf
0001a4a0 t __roundl
00005a00 T fegetround
00005a20 T fesetround
0000d4d0 W llround
000148c0 W llroundf
0001c820 W llroundl
0000d3f0 W lround
00014810 W lroundf
0001c760 W lroundl
0000b250 W round
00012a10 W roundf
0001a4a0 W roundl

   -- Bruce

More information about the SATLUG mailing list