search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Unable to build the code, undefined reference to symbol '__tls_get_addr@@GLIBC_2.3' error #73

Closed bkIITBHILAI closed 4 years ago

bkIITBHILAI commented 4 years ago

While running "make" command, I'm getting the following error. Please help me to build boolector in my system. I'm using Ubuntu 19.10. It has gcc and g++ both of version 9. 

[ 53%] Linking CXX executable ../bin/btormc
/usr/bin/ld: /usr/lib/gcc/x86_64-linux-gnu/9/libstdc++.a(eh_globals.o): undefined reference to symbol '__tls_get_addr@@GLIBC_2.3'
/usr/bin/ld: /lib/x86_64-linux-gnu/ld-linux-x86-64.so.2: error adding symbols: DSO missing from command line
collect2: error: ld returned 1 exit status
mpreiner commented 4 years ago

What's the output of ./configure.sh and what configure options are you using?

bkIITBHILAI commented 4 years ago

I'm not using any particular configure option. I just used ./configure.sh and I got the following message with no error. It was successfully completed.

myName@myName:~/boolector$ ./configure.sh
-- The C compiler identification is GNU 9.2.1
-- The CXX compiler identification is GNU 9.2.1
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- LIB directory is '/home/myName/boolector/build/lib'
-- BIN directory is '/home/myName/boolector/build/bin'
-- Performing Test HAVE_FLAG_std_gnu99
-- Performing Test HAVE_FLAG_std_gnu99 - Success
-- Configuring with C flag '-std=gnu99'
-- Configuring with CXX flag '-std=gnu++11'
-- Performing Test HAVE_FLAG_W
-- Performing Test HAVE_FLAG_W - Success
-- Configuring with C flag '-W'
-- Configuring with CXX flag '-W'
-- Performing Test HAVE_FLAG_Wall
-- Performing Test HAVE_FLAG_Wall - Success
-- Configuring with C flag '-Wall'
-- Configuring with CXX flag '-Wall'
-- Performing Test HAVE_FLAG_Wextra
-- Performing Test HAVE_FLAG_Wextra - Success
-- Configuring with C flag '-Wextra'
-- Configuring with CXX flag '-Wextra'
-- Performing Test HAVE_FLAG_Wredundant_decls
-- Performing Test HAVE_FLAG_Wredundant_decls - Success
-- Configuring with C flag '-Wredundant-decls'
-- Configuring with CXX flag '-Wredundant-decls'
-- No build type set, options are: Debug;Release
-- Building Release build
-- Performing Test HAVE_FLAG_O3
-- Performing Test HAVE_FLAG_O3 - Success
-- Configuring with C flag '-O3'
-- Configuring with CXX flag '-O3'
-- Performing Test HAVE_SIGNALS
-- Performing Test HAVE_SIGNALS - Success
-- Performing Test HAVE_TIME_UTILS
-- Performing Test HAVE_TIME_UTILS - Success
-- Performing Test HAVE_NO_EXPORT_DYNAMIC
-- Performing Test HAVE_NO_EXPORT_DYNAMIC - Success
-- Found Btor2Tools: /home/myName/boolector/deps/install/include  
-- Found Btor2Tools library: /home/myName/boolector/deps/install/lib/libbtor2parser.a
-- Looking for pthread.h
-- Looking for pthread.h - found
-- Looking for pthread_create
-- Looking for pthread_create - not found
-- Check if compiler accepts -pthread
-- Check if compiler accepts -pthread - yes
-- Found Threads: TRUE  
-- Could NOT find Lingeling (missing: Lingeling_INCLUDE_DIR Lingeling_LIBRARIES) 
-- Found CaDiCaL: /home/myName/boolector/deps/install/include  
-- Found CaDiCaL library: /home/myName/boolector/deps/install/lib/libcadical.a
-- Found CryptoMiniSat: /usr/local/include  
-- Found CryptoMiniSat library: /usr/local/lib/libcryptominisat5.so
-- Found PicoSAT: /home/myName/boolector/deps/install/include  
-- Found PicoSAT library: /home/myName/boolector/deps/install/lib/libpicosat.a
-- Found MiniSat: /usr/include  
-- Found MiniSat library: /usr/lib/libminisat.a
-- Found Git: /usr/bin/git (found version "2.20.1") 
-- Configuring done
-- Generating done
-- Build files have been written to: /home/myName/boolector/build/googletest
[ 11%] Performing update step for 'googletest'
[ 22%] No configure step for 'googletest'
[ 33%] No build step for 'googletest'
[ 44%] No install step for 'googletest'
[ 55%] No test step for 'googletest'
[ 66%] Completed 'googletest'
[100%] Built target googletest
-- Found PythonInterp: /usr/bin/python (found version "2.7.17") 
-- Configuring done
-- Generating done
-- Build files have been written to: /home/myName/boolector/build
mpreiner commented 4 years ago

Try to delete build and configure again you should get more output then.

bkIITBHILAI commented 4 years ago

I just deleted the build folder and rerun the ./configure.sh and got the following output again with no error.

myName@myName:~/boolector$ ./configure.sh 
-- The C compiler identification is GNU 9.2.1
-- The CXX compiler identification is GNU 9.2.1
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- LIB directory is '/home/myName/boolector/build/lib'
-- BIN directory is '/home/myName/boolector/build/bin'
-- Performing Test HAVE_FLAG_std_gnu99
-- Performing Test HAVE_FLAG_std_gnu99 - Success
-- Configuring with C flag '-std=gnu99'
-- Configuring with CXX flag '-std=gnu++11'
-- Performing Test HAVE_FLAG_W
-- Performing Test HAVE_FLAG_W - Success
-- Configuring with C flag '-W'
-- Configuring with CXX flag '-W'
-- Performing Test HAVE_FLAG_Wall
-- Performing Test HAVE_FLAG_Wall - Success
-- Configuring with C flag '-Wall'
-- Configuring with CXX flag '-Wall'
-- Performing Test HAVE_FLAG_Wextra
-- Performing Test HAVE_FLAG_Wextra - Success
-- Configuring with C flag '-Wextra'
-- Configuring with CXX flag '-Wextra'
-- Performing Test HAVE_FLAG_Wredundant_decls
-- Performing Test HAVE_FLAG_Wredundant_decls - Success
-- Configuring with C flag '-Wredundant-decls'
-- Configuring with CXX flag '-Wredundant-decls'
-- No build type set, options are: Debug;Release
-- Building Release build
-- Performing Test HAVE_FLAG_O3
-- Performing Test HAVE_FLAG_O3 - Success
-- Configuring with C flag '-O3'
-- Configuring with CXX flag '-O3'
-- Performing Test HAVE_SIGNALS
-- Performing Test HAVE_SIGNALS - Success
-- Performing Test HAVE_TIME_UTILS
-- Performing Test HAVE_TIME_UTILS - Success
-- Performing Test HAVE_NO_EXPORT_DYNAMIC
-- Performing Test HAVE_NO_EXPORT_DYNAMIC - Success
-- Found Btor2Tools: /home/myName/boolector/deps/install/include  
-- Found Btor2Tools library: /home/myName/boolector/deps/install/lib/libbtor2parser.a
-- Looking for pthread.h
-- Looking for pthread.h - found
-- Looking for pthread_create
-- Looking for pthread_create - not found
-- Check if compiler accepts -pthread
-- Check if compiler accepts -pthread - yes
-- Found Threads: TRUE  
-- Could NOT find Lingeling (missing: Lingeling_INCLUDE_DIR Lingeling_LIBRARIES) 
-- Found CaDiCaL: /home/myName/boolector/deps/install/include  
-- Found CaDiCaL library: /home/myName/boolector/deps/install/lib/libcadical.a
-- Found CryptoMiniSat: /usr/local/include  
-- Found CryptoMiniSat library: /usr/local/lib/libcryptominisat5.so
-- Found PicoSAT: /home/myName/boolector/deps/install/include  
-- Found PicoSAT library: /home/myName/boolector/deps/install/lib/libpicosat.a
-- Found MiniSat: /usr/include  
-- Found MiniSat library: /usr/lib/libminisat.a
-- Found Git: /usr/bin/git (found version "2.20.1") 
-- Configuring done
-- Generating done
-- Build files have been written to: /home/myName/boolector/build/googletest
Scanning dependencies of target googletest
[ 11%] Creating directories for 'googletest'
[ 22%] Performing download step (git clone) for 'googletest'
Cloning into 'googletest-src'...
Note: checking out 'release-1.10.0'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by performing another checkout.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -b with the checkout command again. Example:

  git checkout -b <new-branch-name>

HEAD is now at 703bd9ca Googletest export
[ 33%] No patch step for 'googletest'
[ 44%] Performing update step for 'googletest'
[ 55%] No configure step for 'googletest'
[ 66%] No build step for 'googletest'
[ 77%] No install step for 'googletest'
[ 88%] No test step for 'googletest'
[100%] Completed 'googletest'
[100%] Built target googletest
-- Found PythonInterp: /usr/bin/python (found version "2.7.17") 
-- Configuring done
-- Generating done
-- Build files have been written to: /home/myName/boolector/build
bkIITBHILAI commented 4 years ago

The following is the output of make command:

myName@myName:~/boolector/build$ make
Scanning dependencies of target gtest
[  0%] Building CXX object googletest/googletest-build/googletest/CMakeFiles/gtest.dir/src/gtest-all.cc.o
[  0%] Linking CXX static library ../../../lib/libgtest.a
[  0%] Built target gtest
Scanning dependencies of target gmock
[  0%] Building CXX object googletest/googletest-build/googlemock/CMakeFiles/gmock.dir/src/gmock-all.cc.o
[  1%] Linking CXX static library ../../../lib/libgmock.a
[  1%] Built target gmock
Scanning dependencies of target gmock_main
[  1%] Building CXX object googletest/googletest-build/googlemock/CMakeFiles/gmock_main.dir/src/gmock_main.cc.o
[  2%] Linking CXX static library ../../../lib/libgmock_main.a
[  2%] Built target gmock_main
Scanning dependencies of target gtest_main
[  4%] Building CXX object googletest/googletest-build/googletest/CMakeFiles/gtest_main.dir/src/gtest_main.cc.o
[  4%] Linking CXX static library ../../../lib/libgtest_main.a
[  4%] Built target gtest_main
Scanning dependencies of target boolector
[  4%] Building C object src/CMakeFiles/boolector.dir/aigprop.c.o
[  5%] Building C object src/CMakeFiles/boolector.dir/boolector.c.o
[  5%] Building C object src/CMakeFiles/boolector.dir/boolectormc.c.o
[  7%] Building C object src/CMakeFiles/boolector.dir/btorabort.c.o
[  7%] Building C object src/CMakeFiles/boolector.dir/btoraig.c.o
[  8%] Building C object src/CMakeFiles/boolector.dir/btoraigvec.c.o
[  8%] Building C object src/CMakeFiles/boolector.dir/btorass.c.o
[  8%] Building C object src/CMakeFiles/boolector.dir/btorbeta.c.o
[  9%] Building C object src/CMakeFiles/boolector.dir/btorbv.c.o
[  9%] Building C object src/CMakeFiles/boolector.dir/btorchkclone.c.o
[ 11%] Building C object src/CMakeFiles/boolector.dir/btorchkmodel.c.o
[ 11%] Building C object src/CMakeFiles/boolector.dir/btorchkfailed.c.o
[ 12%] Building C object src/CMakeFiles/boolector.dir/btorclone.c.o
[ 12%] Building C object src/CMakeFiles/boolector.dir/btorcore.c.o
[ 12%] Building C object src/CMakeFiles/boolector.dir/btordbg.c.o
[ 14%] Building C object src/CMakeFiles/boolector.dir/btordcr.c.o
[ 14%] Building C object src/CMakeFiles/boolector.dir/btorexp.c.o
[ 15%] Building C object src/CMakeFiles/boolector.dir/btorlsutils.c.o
[ 15%] Building C object src/CMakeFiles/boolector.dir/btormc.c.o
[ 16%] Building C object src/CMakeFiles/boolector.dir/btormodel.c.o
[ 16%] Building C object src/CMakeFiles/boolector.dir/btormsg.c.o
[ 16%] Building C object src/CMakeFiles/boolector.dir/btornode.c.o
[ 18%] Building C object src/CMakeFiles/boolector.dir/btoropt.c.o
[ 18%] Building C object src/CMakeFiles/boolector.dir/btorparse.c.o
[ 19%] Building C object src/CMakeFiles/boolector.dir/btorprintmodel.c.o
[ 19%] Building C object src/CMakeFiles/boolector.dir/btorproputils.c.o
[ 21%] Building C object src/CMakeFiles/boolector.dir/btorrewrite.c.o
[ 21%] Building C object src/CMakeFiles/boolector.dir/btorrwcache.c.o
[ 21%] Building C object src/CMakeFiles/boolector.dir/btorsat.c.o
[ 22%] Building C object src/CMakeFiles/boolector.dir/btorslsutils.c.o
[ 22%] Building C object src/CMakeFiles/boolector.dir/btorslvaigprop.c.o
[ 23%] Building C object src/CMakeFiles/boolector.dir/btorslvfun.c.o
[ 23%] Building C object src/CMakeFiles/boolector.dir/btorslvprop.c.o
[ 25%] Building C object src/CMakeFiles/boolector.dir/btorslvquant.c.o
[ 25%] Building C object src/CMakeFiles/boolector.dir/btorslvsls.c.o
[ 25%] Building C object src/CMakeFiles/boolector.dir/btorsort.c.o
[ 26%] Building C object src/CMakeFiles/boolector.dir/btorsubst.c.o
[ 26%] Building C object src/CMakeFiles/boolector.dir/btorsynth.c.o
[ 28%] Building C object src/CMakeFiles/boolector.dir/btortrapi.c.o
[ 28%] Building C object src/CMakeFiles/boolector.dir/dumper/btordumpaig.c.o
[ 29%] Building C object src/CMakeFiles/boolector.dir/dumper/btordumpbtor.c.o
[ 29%] Building C object src/CMakeFiles/boolector.dir/dumper/btordumpsmt.c.o
[ 29%] Building C object src/CMakeFiles/boolector.dir/parser/btorbtor.c.o
[ 30%] Building C object src/CMakeFiles/boolector.dir/parser/btorbtor2.c.o
[ 30%] Building C object src/CMakeFiles/boolector.dir/parser/btorsmt.c.o
[ 32%] Building C object src/CMakeFiles/boolector.dir/parser/btorsmt2.c.o
[ 32%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorpputils.c.o
[ 33%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorack.c.o
[ 33%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorder.c.o
[ 35%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorelimapplies.c.o
[ 35%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorelimslices.c.o
[ 35%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorembed.c.o
[ 36%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorextract.c.o
[ 36%] Building C object src/CMakeFiles/boolector.dir/preprocess/btormerge.c.o
[ 38%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorminiscope.c.o
[ 38%] Building C object src/CMakeFiles/boolector.dir/preprocess/btornormadd.c.o
[ 39%] Building C object src/CMakeFiles/boolector.dir/preprocess/btornormquant.c.o
[ 39%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorpreprocess.c.o
[ 39%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorskel.c.o
[ 40%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorskolemize.c.o
[ 40%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorunconstrained.c.o
[ 42%] Building C object src/CMakeFiles/boolector.dir/preprocess/btorvarsubst.c.o
[ 42%] Building C object src/CMakeFiles/boolector.dir/sat/btorcadical.c.o
[ 43%] Building CXX object src/CMakeFiles/boolector.dir/sat/btorcms.cc.o
/home/myName/boolector/src/sat/btorcms.cc: In member function ‘int32_t BtorCMS::deref(int32_t)’:
/home/myName/boolector/src/sat/btorcms.cc:145:14: warning: unused variable ‘v’ [-Wunused-variable]
  145 |     uint32_t v                      = l.var ();
      |              ^
[ 43%] Building C object src/CMakeFiles/boolector.dir/sat/btorlgl.c.o
[ 43%] Building CXX object src/CMakeFiles/boolector.dir/sat/btorminisat.cc.o
[ 45%] Building C object src/CMakeFiles/boolector.dir/sat/btorpicosat.c.o
[ 45%] Building C object src/CMakeFiles/boolector.dir/utils/boolectornodemap.c.o
[ 46%] Building C object src/CMakeFiles/boolector.dir/utils/btoraigmap.c.o
[ 46%] Building C object src/CMakeFiles/boolector.dir/utils/btorhashint.c.o
[ 47%] Building C object src/CMakeFiles/boolector.dir/utils/btorhashptr.c.o
[ 47%] Building C object src/CMakeFiles/boolector.dir/utils/btormem.c.o
[ 47%] Building C object src/CMakeFiles/boolector.dir/utils/btornodeiter.c.o
[ 49%] Building C object src/CMakeFiles/boolector.dir/utils/btornodemap.c.o
[ 49%] Building C object src/CMakeFiles/boolector.dir/utils/btoroptparse.c.o
[ 50%] Building C object src/CMakeFiles/boolector.dir/utils/btorpartgen.c.o
[ 50%] Building C object src/CMakeFiles/boolector.dir/utils/btorrng.c.o
[ 52%] Building C object src/CMakeFiles/boolector.dir/utils/btorunionfind.c.o
[ 52%] Building C object src/CMakeFiles/boolector.dir/utils/btorutil.c.o
[ 52%] Linking CXX static library ../lib/libboolector.a
[ 52%] Built target boolector
Scanning dependencies of target btormc
[ 52%] Building C object src/CMakeFiles/btormc.dir/btormcmain.c.o
[ 53%] Linking CXX executable ../bin/btormc
/usr/bin/ld: /usr/lib/gcc/x86_64-linux-gnu/9/libstdc++.a(eh_globals.o): undefined reference to symbol '__tls_get_addr@@GLIBC_2.3'
/usr/bin/ld: /lib/x86_64-linux-gnu/ld-linux-x86-64.so.2: error adding symbols: DSO missing from command line
collect2: error: ld returned 1 exit status
make[2]: *** [src/CMakeFiles/btormc.dir/build.make:90: bin/btormc] Error 1
make[1]: *** [CMakeFiles/Makefile2:342: src/CMakeFiles/btormc.dir/all] Error 2
make: *** [Makefile:141: all] Error 2
mpreiner commented 4 years ago

Seems like this happens while linking btormc. Boolector builds fine and the binary should be in build/bin. I'll try to reproduce the error. In the meantime you should be able to use Boolector without any problems.

bkIITBHILAI commented 4 years ago

No. Boolector has not been stored in build/bin. It might be the case that only after build is done successfully, all binaries get stored in build/bin. Temporarily they might be in some cache. It's just a guess.

mpreiner commented 4 years ago

Can you try compiling without MiniSat? ./configure.sh --no-minisat

bkIITBHILAI commented 4 years ago

Yes, I tried.. Again got the same error while running make

bkIITBHILAI commented 4 years ago

Ok.. Finally I solved it. I had to add the "\usr\lib64\ld-linux-x86-64.so.2" - this library manually to each linker.txt file. Thank you for your quick responses.

mpreiner commented 4 years ago

The problem is I can't reproduce it on Ubuntu 19.10 (docker container). It looks like you have minisat and cryptominisat installed on the system. Can you try configuring without them? --no-minisat --no-cms

bkIITBHILAI commented 4 years ago

Ok.. Finally I solved it. I had to add the "\usr\lib64\ld-linux-x86-64.so.2" - this library manually to each linker.txt file. Thank you for your quick responses.

The problem is solved now.