* Package: sci-mathematics/vampire-4.6.1 * Repository: gentoo * Maintainer: sci-mathematics@gentoo.org * Upstream: https://github.com/vprover/vampire/issues/ * USE: abi_x86_64 amd64 elibc_glibc kernel_linux userland_GNU z3 * FEATURES: network-sandbox preserve-libs sandbox userpriv usersandbox >>> Unpacking source... >>> Unpacking vampire-4.6.1.tar.gz to /var/tmp/portage/sci-mathematics/vampire-4.6.1/work >>> Source unpacked in /var/tmp/portage/sci-mathematics/vampire-4.6.1/work >>> Preparing source in /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 ... * Source directory (CMAKE_USE_DIR): "/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1" * Build directory (BUILD_DIR): "/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build" * Hardcoded definition(s) removed in CMakeLists.txt: * set(CMAKE_BUILD_TYPE Release CACHE STRING "Choose the type of build." FORCE >>> Source prepared. >>> Configuring source in /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 ... * Source directory (CMAKE_USE_DIR): "/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1" * Build directory (BUILD_DIR): "/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build" cmake -C /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build/gentoo_common_config.cmake -G Ninja -DCMAKE_INSTALL_PREFIX=/usr -DZ3_DIR=/usr/lib64/cmake/z3/ -DCMAKE_BUILD_TYPE=Release -DCMAKE_TOOLCHAIN_FILE=/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build/gentoo_toolchain.cmake /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 loading initial cache file /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build/gentoo_common_config.cmake -- The C compiler identification is GNU 12.1.1 -- The CXX compiler identification is GNU 12.1.1 -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/bin/x86_64-pc-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/bin/x86_64-pc-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- IPO supported -- Found Z3 4.10.1.0 fatal: not a git repository (or any parent up to mount point /var/tmp) Stopping at filesystem boundary (GIT_DISCOVERY_ACROSS_FILESYSTEM not set). -- Setting binary name to 'vampire_z3_rel' -- <<< Gentoo configuration >>> Build type Release Install path /usr Compiler flags: C -pipe -march=native -fno-diagnostics-color -O2 C++ -pipe -march=native -fno-diagnostics-color -O2 Linker flags: Executable -Wl,-O1 -Wl,--as-needed -Wl,--defsym=__gentoo_check_ldflags__=0 Module -Wl,-O1 -Wl,--as-needed -Wl,--defsym=__gentoo_check_ldflags__=0 Shared -Wl,-O1 -Wl,--as-needed -Wl,--defsym=__gentoo_check_ldflags__=0 -- Configuring done -- Generating done -- Build files have been written to: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build >>> Source configured. >>> Compiling source in /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 ... * Source directory (CMAKE_USE_DIR): "/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1" * Build directory (BUILD_DIR): "/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build" ninja -v -j4 -l0 [1/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Debug/Assertion.cpp.o -MF CMakeFiles/obj.dir/Debug/Assertion.cpp.o.d -o CMakeFiles/obj.dir/Debug/Assertion.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Debug/Assertion.cpp [2/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Debug/Tracer.cpp.o -MF CMakeFiles/obj.dir/Debug/Tracer.cpp.o.d -o CMakeFiles/obj.dir/Debug/Tracer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Debug/Tracer.cpp [3/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Debug/RuntimeStatistics.cpp.o -MF CMakeFiles/obj.dir/Debug/RuntimeStatistics.cpp.o.d -o CMakeFiles/obj.dir/Debug/RuntimeStatistics.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Debug/RuntimeStatistics.cpp [4/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/DHMap.cpp.o -MF CMakeFiles/obj.dir/Lib/DHMap.cpp.o.d -o CMakeFiles/obj.dir/Lib/DHMap.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/DHMap.cpp [5/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Event.cpp.o -MF CMakeFiles/obj.dir/Lib/Event.cpp.o.d -o CMakeFiles/obj.dir/Lib/Event.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Event.cpp [6/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Allocator.cpp.o -MF CMakeFiles/obj.dir/Lib/Allocator.cpp.o.d -o CMakeFiles/obj.dir/Lib/Allocator.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Allocator.cpp [7/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Exception.cpp.o -MF CMakeFiles/obj.dir/Lib/Exception.cpp.o.d -o CMakeFiles/obj.dir/Lib/Exception.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Exception.cpp [8/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Int.cpp.o -MF CMakeFiles/obj.dir/Lib/Int.cpp.o.d -o CMakeFiles/obj.dir/Lib/Int.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Int.cpp [9/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/IntNameTable.cpp.o -MF CMakeFiles/obj.dir/Lib/IntNameTable.cpp.o.d -o CMakeFiles/obj.dir/Lib/IntNameTable.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/IntNameTable.cpp [10/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/MemoryLeak.cpp.o -MF CMakeFiles/obj.dir/Lib/MemoryLeak.cpp.o.d -o CMakeFiles/obj.dir/Lib/MemoryLeak.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/MemoryLeak.cpp [11/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Hash.cpp.o -MF CMakeFiles/obj.dir/Lib/Hash.cpp.o.d -o CMakeFiles/obj.dir/Lib/Hash.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Hash.cpp [12/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/MultiCounter.cpp.o -MF CMakeFiles/obj.dir/Lib/MultiCounter.cpp.o.d -o CMakeFiles/obj.dir/Lib/MultiCounter.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/MultiCounter.cpp [13/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/IntUnionFind.cpp.o -MF CMakeFiles/obj.dir/Lib/IntUnionFind.cpp.o.d -o CMakeFiles/obj.dir/Lib/IntUnionFind.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/IntUnionFind.cpp [14/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Random.cpp.o -MF CMakeFiles/obj.dir/Lib/Random.cpp.o.d -o CMakeFiles/obj.dir/Lib/Random.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Random.cpp [15/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/NameArray.cpp.o -MF CMakeFiles/obj.dir/Lib/NameArray.cpp.o.d -o CMakeFiles/obj.dir/Lib/NameArray.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/NameArray.cpp [16/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/StringUtils.cpp.o -MF CMakeFiles/obj.dir/Lib/StringUtils.cpp.o.d -o CMakeFiles/obj.dir/Lib/StringUtils.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/StringUtils.cpp [17/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/TimeCounter.cpp.o -MF CMakeFiles/obj.dir/Lib/TimeCounter.cpp.o.d -o CMakeFiles/obj.dir/Lib/TimeCounter.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/TimeCounter.cpp [18/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/System.cpp.o -MF CMakeFiles/obj.dir/Lib/System.cpp.o.d -o CMakeFiles/obj.dir/Lib/System.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/System.cpp [19/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Sys/Multiprocessing.cpp.o -MF CMakeFiles/obj.dir/Lib/Sys/Multiprocessing.cpp.o.d -o CMakeFiles/obj.dir/Lib/Sys/Multiprocessing.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Sys/Multiprocessing.cpp [20/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Timer.cpp.o -MF CMakeFiles/obj.dir/Lib/Timer.cpp.o.d -o CMakeFiles/obj.dir/Lib/Timer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Timer.cpp [21/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Sys/Semaphore.cpp.o -MF CMakeFiles/obj.dir/Lib/Sys/Semaphore.cpp.o.d -o CMakeFiles/obj.dir/Lib/Sys/Semaphore.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Sys/Semaphore.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Sys/Semaphore.cpp: In constructor ‘Lib::Sys::Semaphore::Semaphore(int)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Sys/Semaphore.cpp:67:11: warning: ignoring return value of ‘int system(const char*)’ declared with attribute ‘warn_unused_result’ [-Wunused-result] 67 | system("ipcs -s | grep 0x00000000 | cut -d' ' -f2|xargs -n 1 ipcrm -s"); | ~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [22/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/ClauseQueue.cpp.o -MF CMakeFiles/obj.dir/Kernel/ClauseQueue.cpp.o.d -o CMakeFiles/obj.dir/Kernel/ClauseQueue.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/ClauseQueue.cpp [23/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Sys/SyncPipe.cpp.o -MF CMakeFiles/obj.dir/Lib/Sys/SyncPipe.cpp.o.d -o CMakeFiles/obj.dir/Lib/Sys/SyncPipe.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Sys/SyncPipe.cpp [24/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/ELiteralSelector.cpp.o -MF CMakeFiles/obj.dir/Kernel/ELiteralSelector.cpp.o.d -o CMakeFiles/obj.dir/Kernel/ELiteralSelector.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/ELiteralSelector.cpp [25/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o -MF CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o.d -o CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/ColorHelper.cpp [26/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Clause.cpp.o -MF CMakeFiles/obj.dir/Kernel/Clause.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Clause.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Clause.cpp [27/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/EqHelper.cpp.o -MF CMakeFiles/obj.dir/Kernel/EqHelper.cpp.o.d -o CMakeFiles/obj.dir/Kernel/EqHelper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp: In static member function ‘static Kernel::TermIterator Kernel::EqHelper::getSubVarSupLHSIterator(Kernel::Literal*, const Kernel::Ordering&)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:359:11: warning: enumeration value ‘EQUAL’ not handled in switch [-Wswitch] 359 | switch(ord.getEqualityArgumentOrder(lit)) | ^ In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/OperatorType.hpp:30, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TermAlgebra.hpp:19, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Theory.hpp:25, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Property.hpp:27, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Options.hpp:57, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:17: In member function ‘Kernel::Term* Kernel::TermList::term()’, inlined from ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableSubtermIterator(Kernel::Literal*, const Kernel::Ordering&) [with SubtermIterator = Kernel::BooleanSubtermIt]’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:265:43: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.hpp:117:27: warning: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ may be used uninitialized [-Wmaybe-uninitialized] 117 | { ASS(isTerm()); return _term; } | ^~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp: In static member function ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableSubtermIterator(Kernel::Literal*, const Kernel::Ordering&) [with SubtermIterator = Kernel::BooleanSubtermIt]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:242:14: note: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ was declared here 242 | TermList sel; | ^~~ In member function ‘Kernel::Term* Kernel::TermList::term()’, inlined from ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableSubtermIterator(Kernel::Literal*, const Kernel::Ordering&) [with SubtermIterator = Kernel::NarrowableSubtermIt]’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:265:43: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.hpp:117:27: warning: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ may be used uninitialized [-Wmaybe-uninitialized] 117 | { ASS(isTerm()); return _term; } | ^~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp: In static member function ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableSubtermIterator(Kernel::Literal*, const Kernel::Ordering&) [with SubtermIterator = Kernel::NarrowableSubtermIt]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:242:14: note: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ was declared here 242 | TermList sel; | ^~~ In member function ‘Kernel::Term* Kernel::TermList::term()’, inlined from ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableSubtermIterator(Kernel::Literal*, const Kernel::Ordering&) [with SubtermIterator = Kernel::FirstOrderSubtermIt]’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:265:43: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.hpp:117:27: warning: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ may be used uninitialized [-Wmaybe-uninitialized] 117 | { ASS(isTerm()); return _term; } | ^~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp: In static member function ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableSubtermIterator(Kernel::Literal*, const Kernel::Ordering&) [with SubtermIterator = Kernel::FirstOrderSubtermIt]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:242:14: note: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ was declared here 242 | TermList sel; | ^~~ In member function ‘Kernel::Term* Kernel::TermList::term()’, inlined from ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableSubtermIterator(Kernel::Literal*, const Kernel::Ordering&) [with SubtermIterator = Kernel::NonVariableNonTypeIterator]’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:265:43: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.hpp:117:27: warning: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ may be used uninitialized [-Wmaybe-uninitialized] 117 | { ASS(isTerm()); return _term; } | ^~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp: In static member function ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableSubtermIterator(Kernel::Literal*, const Kernel::Ordering&) [with SubtermIterator = Kernel::NonVariableNonTypeIterator]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:242:14: note: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ was declared here 242 | TermList sel; | ^~~ In member function ‘Kernel::TermTag Kernel::TermList::tag() const’, inlined from ‘bool Kernel::TermList::isTerm() const’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.hpp:113:15, inlined from ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableVarsIterator(Lib::DHSet*, Kernel::Literal*, const Kernel::Ordering&)’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:225:18: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.hpp:87:39: warning: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ may be used uninitialized [-Wmaybe-uninitialized] 87 | inline TermTag tag() const { return (TermTag)(_content & 0x0003); } | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp: In static member function ‘static Kernel::TermIterator Kernel::EqHelper::getRewritableVarsIterator(Lib::DHSet*, Kernel::Literal*, const Kernel::Ordering&)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/EqHelper.cpp:205:12: note: ‘sel.Kernel::TermList::.Kernel::TermList::::_content’ was declared here 205 | TermList sel; | ^~~ [28/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/FlatTerm.cpp.o -MF CMakeFiles/obj.dir/Kernel/FlatTerm.cpp.o.d -o CMakeFiles/obj.dir/Kernel/FlatTerm.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/FlatTerm.cpp [29/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Formula.cpp.o -MF CMakeFiles/obj.dir/Kernel/Formula.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Formula.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Formula.cpp [30/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/FormulaUnit.cpp.o -MF CMakeFiles/obj.dir/Kernel/FormulaUnit.cpp.o.d -o CMakeFiles/obj.dir/Kernel/FormulaUnit.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/FormulaUnit.cpp [31/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/FormulaTransformer.cpp.o -MF CMakeFiles/obj.dir/Kernel/FormulaTransformer.cpp.o.d -o CMakeFiles/obj.dir/Kernel/FormulaTransformer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/FormulaTransformer.cpp [32/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Lib/Environment.cpp.o -MF CMakeFiles/obj.dir/Lib/Environment.cpp.o.d -o CMakeFiles/obj.dir/Lib/Environment.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Environment.cpp [33/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/FormulaVarIterator.cpp.o -MF CMakeFiles/obj.dir/Kernel/FormulaVarIterator.cpp.o.d -o CMakeFiles/obj.dir/Kernel/FormulaVarIterator.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/FormulaVarIterator.cpp [34/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Grounder.cpp.o -MF CMakeFiles/obj.dir/Kernel/Grounder.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Grounder.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Grounder.cpp [35/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Inference.cpp.o -MF CMakeFiles/obj.dir/Kernel/Inference.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Inference.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Inference.cpp [36/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Rebalancing.cpp.o -MF CMakeFiles/obj.dir/Kernel/Rebalancing.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Rebalancing.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Rebalancing.cpp [37/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/InterpretedLiteralEvaluator.cpp.o -MF CMakeFiles/obj.dir/Kernel/InterpretedLiteralEvaluator.cpp.o.d -o CMakeFiles/obj.dir/Kernel/InterpretedLiteralEvaluator.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/InterpretedLiteralEvaluator.cpp [38/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/KBOForEPR.cpp.o -MF CMakeFiles/obj.dir/Kernel/KBOForEPR.cpp.o.d -o CMakeFiles/obj.dir/Kernel/KBOForEPR.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/KBOForEPR.cpp [39/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/InferenceStore.cpp.o -MF CMakeFiles/obj.dir/Kernel/InferenceStore.cpp.o.d -o CMakeFiles/obj.dir/Kernel/InferenceStore.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/InferenceStore.cpp [40/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/KBO.cpp.o -MF CMakeFiles/obj.dir/Kernel/KBO.cpp.o.d -o CMakeFiles/obj.dir/Kernel/KBO.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/KBO.cpp [41/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/LookaheadLiteralSelector.cpp.o -MF CMakeFiles/obj.dir/Kernel/LookaheadLiteralSelector.cpp.o.d -o CMakeFiles/obj.dir/Kernel/LookaheadLiteralSelector.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/LookaheadLiteralSelector.cpp [42/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/LiteralSelector.cpp.o -MF CMakeFiles/obj.dir/Kernel/LiteralSelector.cpp.o.d -o CMakeFiles/obj.dir/Kernel/LiteralSelector.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/LiteralSelector.cpp [43/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/MainLoop.cpp.o -MF CMakeFiles/obj.dir/Kernel/MainLoop.cpp.o.d -o CMakeFiles/obj.dir/Kernel/MainLoop.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/MainLoop.cpp [44/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/MaximalLiteralSelector.cpp.o -MF CMakeFiles/obj.dir/Kernel/MaximalLiteralSelector.cpp.o.d -o CMakeFiles/obj.dir/Kernel/MaximalLiteralSelector.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/MaximalLiteralSelector.cpp [45/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o -MF CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o.d -o CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/MLMatcher.cpp [46/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/MLVariant.cpp.o -MF CMakeFiles/obj.dir/Kernel/MLVariant.cpp.o.d -o CMakeFiles/obj.dir/Kernel/MLVariant.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/MLVariant.cpp [47/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/MLMatcherSD.cpp.o -MF CMakeFiles/obj.dir/Kernel/MLMatcherSD.cpp.o.d -o CMakeFiles/obj.dir/Kernel/MLMatcherSD.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/MLMatcherSD.cpp [48/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Matcher.cpp.o -MF CMakeFiles/obj.dir/Kernel/Matcher.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Matcher.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Matcher.cpp [49/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Ordering_Equality.cpp.o -MF CMakeFiles/obj.dir/Kernel/Ordering_Equality.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Ordering_Equality.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Ordering_Equality.cpp [50/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Problem.cpp.o -MF CMakeFiles/obj.dir/Kernel/Problem.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Problem.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Problem.cpp [51/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Renaming.cpp.o -MF CMakeFiles/obj.dir/Kernel/Renaming.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Renaming.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Renaming.cpp [52/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Ordering.cpp.o -MF CMakeFiles/obj.dir/Kernel/Ordering.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Ordering.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Ordering.cpp [53/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/MismatchHandler.cpp.o -MF CMakeFiles/obj.dir/Kernel/MismatchHandler.cpp.o.d -o CMakeFiles/obj.dir/Kernel/MismatchHandler.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/MismatchHandler.cpp [54/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/RobSubstitution.cpp.o -MF CMakeFiles/obj.dir/Kernel/RobSubstitution.cpp.o.d -o CMakeFiles/obj.dir/Kernel/RobSubstitution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/RobSubstitution.cpp [55/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/SpassLiteralSelector.cpp.o -MF CMakeFiles/obj.dir/Kernel/SpassLiteralSelector.cpp.o.d -o CMakeFiles/obj.dir/Kernel/SpassLiteralSelector.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/SpassLiteralSelector.cpp [56/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/OperatorType.cpp.o -MF CMakeFiles/obj.dir/Kernel/OperatorType.cpp.o.d -o CMakeFiles/obj.dir/Kernel/OperatorType.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/OperatorType.cpp [57/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/SortHelper.cpp.o -MF CMakeFiles/obj.dir/Kernel/SortHelper.cpp.o.d -o CMakeFiles/obj.dir/Kernel/SortHelper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/SortHelper.cpp In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/OperatorType.hpp:30, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TermAlgebra.hpp:19, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Signature.hpp:35, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/SortHelper.cpp:19: In member function ‘unsigned int Kernel::TermList::var() const’, inlined from ‘static Kernel::TermList Kernel::SortHelper::getResultSort(Kernel::TermList, Lib::DHMap&)’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/SortHelper.cpp:146:23: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.hpp:110:26: warning: ‘masterVar.Kernel::TermList::.Kernel::TermList::::_content’ may be used uninitialized [-Wmaybe-uninitialized] 110 | { ASS(isVar()); return _content / 4; } | ^~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/SortHelper.cpp: In static member function ‘static Kernel::TermList Kernel::SortHelper::getResultSort(Kernel::TermList, Lib::DHMap&)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/SortHelper.cpp:143:12: note: ‘masterVar’ declared here 143 | TermList masterVar; | ^~~~~~~~~ [58/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Substitution.cpp.o -MF CMakeFiles/obj.dir/Kernel/Substitution.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Substitution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Substitution.cpp [59/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/SubformulaIterator.cpp.o -MF CMakeFiles/obj.dir/Kernel/SubformulaIterator.cpp.o.d -o CMakeFiles/obj.dir/Kernel/SubformulaIterator.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/SubformulaIterator.cpp [60/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Signature.cpp.o -MF CMakeFiles/obj.dir/Kernel/Signature.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Signature.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Signature.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Signature.cpp: In constructor ‘Kernel::Signature::Signature()’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Signature.cpp:256:12: warning: variable ‘aux’ set but not used [-Wunused-but-set-variable] 256 | unsigned aux; | ^~~ [61/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/TermTransformer.cpp.o -MF CMakeFiles/obj.dir/Kernel/TermTransformer.cpp.o.d -o CMakeFiles/obj.dir/Kernel/TermTransformer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/TermTransformer.cpp [62/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/TermIterators.cpp.o -MF CMakeFiles/obj.dir/Kernel/TermIterators.cpp.o.d -o CMakeFiles/obj.dir/Kernel/TermIterators.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/TermIterators.cpp [63/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Unit.cpp.o -MF CMakeFiles/obj.dir/Kernel/Unit.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Unit.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Unit.cpp [64/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/LPO.cpp.o -MF CMakeFiles/obj.dir/Kernel/LPO.cpp.o.d -o CMakeFiles/obj.dir/Kernel/LPO.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/LPO.cpp [65/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Theory.cpp.o -MF CMakeFiles/obj.dir/Kernel/Theory.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Theory.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Theory.cpp [66/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Term.cpp.o -MF CMakeFiles/obj.dir/Kernel/Term.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Term.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.cpp [67/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/ApplicativeHelper.cpp.o -MF CMakeFiles/obj.dir/Kernel/ApplicativeHelper.cpp.o.d -o CMakeFiles/obj.dir/Kernel/ApplicativeHelper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/ApplicativeHelper.cpp [68/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/SKIKBO.cpp.o -MF CMakeFiles/obj.dir/Kernel/SKIKBO.cpp.o.d -o CMakeFiles/obj.dir/Kernel/SKIKBO.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/SKIKBO.cpp [69/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Polynomial.cpp.o -MF CMakeFiles/obj.dir/Kernel/Polynomial.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Polynomial.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Polynomial.cpp [70/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/PolynomialNormalizer.cpp.o -MF CMakeFiles/obj.dir/Kernel/PolynomialNormalizer.cpp.o.d -o CMakeFiles/obj.dir/Kernel/PolynomialNormalizer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.hpp:34, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp:11: In constructor ‘Kernel::Monom::Monom(Numeral, Lib::Perfect >) [with Number = Kernel::NumTraits]’, inlined from ‘Kernel::Monom Kernel::RenderMonom::operator()(Kernel::MonomFactors&&) const [with NumTraits = Kernel::NumTraits]’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp:54:44: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Polynomial.hpp:541:5: warning: ‘*(const Kernel::IntegerConstantType*)((char*)&fstNum + offsetof(Lib::Option,Lib::Option::.Lib::OptionBase::_elem.Lib::MaybeUninit::_elem)).Kernel::IntegerConstantType::_val’ may be used uninitialized [-Wmaybe-uninitialized] 541 | : numeral(numeral), factors(factors) | ^~~~~~~~~~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp: In function ‘Kernel::Monom Kernel::RenderMonom::operator()(Kernel::MonomFactors&&) const [with NumTraits = Kernel::NumTraits]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp:28:10: note: ‘*(const Kernel::IntegerConstantType*)((char*)&fstNum + offsetof(Lib::Option,Lib::Option::.Lib::OptionBase::_elem.Lib::MaybeUninit::_elem)).Kernel::IntegerConstantType::_val’ was declared here 28 | auto fstNum = Option(); | ^~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp: In function ‘Kernel::Monom Kernel::RenderMonom::operator()(Kernel::MonomFactors&&) const [with NumTraits = Kernel::NumTraits]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp:28:10: warning: ‘((Kernel::IntegerConstantType::InnerType*)((char*)&fstNum + offsetof(Lib::Option,Lib::Option::.Lib::OptionBase::_elem.Lib::MaybeUninit::_elem)))[1]’ may be used uninitialized [-Wmaybe-uninitialized] /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp:28:10: warning: ‘*(Kernel::IntegerConstantType::InnerType*)((char*)&fstNum + offsetof(Lib::Option,Lib::Option::.Lib::OptionBase::_elem.Lib::MaybeUninit::_elem))’ may be used uninitialized [-Wmaybe-uninitialized] /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp: In function ‘Kernel::Monom Kernel::RenderMonom::operator()(Kernel::MonomFactors&&) const [with NumTraits = Kernel::NumTraits]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp:28:10: warning: ‘((Kernel::IntegerConstantType::InnerType*)((char*)&fstNum + offsetof(Lib::Option,Lib::Option::.Lib::OptionBase::_elem.Lib::MaybeUninit::_elem)))[1]’ may be used uninitialized [-Wmaybe-uninitialized] /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/PolynomialNormalizer.cpp:28:10: warning: ‘*(Kernel::IntegerConstantType::InnerType*)((char*)&fstNum + offsetof(Lib::Option,Lib::Option::.Lib::OptionBase::_elem.Lib::MaybeUninit::_elem))’ may be used uninitialized [-Wmaybe-uninitialized] [71/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/CombinatorDemodISE.cpp.o -MF CMakeFiles/obj.dir/Inferences/CombinatorDemodISE.cpp.o.d -o CMakeFiles/obj.dir/Inferences/CombinatorDemodISE.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/CombinatorDemodISE.cpp [72/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/CNFOnTheFly.cpp.o -MF CMakeFiles/obj.dir/Inferences/CNFOnTheFly.cpp.o.d -o CMakeFiles/obj.dir/Inferences/CNFOnTheFly.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/CNFOnTheFly.cpp [73/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/TypeSubstitutionTree.cpp.o -MF CMakeFiles/obj.dir/Indexing/TypeSubstitutionTree.cpp.o.d -o CMakeFiles/obj.dir/Indexing/TypeSubstitutionTree.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/TypeSubstitutionTree.cpp [74/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/CombinatorNormalisationISE.cpp.o -MF CMakeFiles/obj.dir/Inferences/CombinatorNormalisationISE.cpp.o.d -o CMakeFiles/obj.dir/Inferences/CombinatorNormalisationISE.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/CombinatorNormalisationISE.cpp [75/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/ArgCong.cpp.o -MF CMakeFiles/obj.dir/Inferences/ArgCong.cpp.o.d -o CMakeFiles/obj.dir/Inferences/ArgCong.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/ArgCong.cpp [76/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/NegativeExt.cpp.o -MF CMakeFiles/obj.dir/Inferences/NegativeExt.cpp.o.d -o CMakeFiles/obj.dir/Inferences/NegativeExt.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/NegativeExt.cpp [77/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Narrow.cpp.o -MF CMakeFiles/obj.dir/Inferences/Narrow.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Narrow.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Narrow.cpp [78/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/BoolEqToDiseq.cpp.o -MF CMakeFiles/obj.dir/Inferences/BoolEqToDiseq.cpp.o.d -o CMakeFiles/obj.dir/Inferences/BoolEqToDiseq.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/BoolEqToDiseq.cpp [79/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/PrimitiveInstantiation.cpp.o -MF CMakeFiles/obj.dir/Inferences/PrimitiveInstantiation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/PrimitiveInstantiation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/PrimitiveInstantiation.cpp [80/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/SubVarSup.cpp.o -MF CMakeFiles/obj.dir/Inferences/SubVarSup.cpp.o.d -o CMakeFiles/obj.dir/Inferences/SubVarSup.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/SubVarSup.cpp [81/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/ElimLeibniz.cpp.o -MF CMakeFiles/obj.dir/Inferences/ElimLeibniz.cpp.o.d -o CMakeFiles/obj.dir/Inferences/ElimLeibniz.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/ElimLeibniz.cpp [82/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/BoolSimp.cpp.o -MF CMakeFiles/obj.dir/Inferences/BoolSimp.cpp.o.d -o CMakeFiles/obj.dir/Inferences/BoolSimp.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/BoolSimp.cpp [83/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Injectivity.cpp.o -MF CMakeFiles/obj.dir/Inferences/Injectivity.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Injectivity.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Injectivity.cpp [84/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Choice.cpp.o -MF CMakeFiles/obj.dir/Inferences/Choice.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Choice.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Choice.cpp [85/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/CasesSimp.cpp.o -MF CMakeFiles/obj.dir/Inferences/CasesSimp.cpp.o.d -o CMakeFiles/obj.dir/Inferences/CasesSimp.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/CasesSimp.cpp [86/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Cases.cpp.o -MF CMakeFiles/obj.dir/Inferences/Cases.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Cases.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Cases.cpp [87/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/LambdaElimination.cpp.o -MF CMakeFiles/obj.dir/Shell/LambdaElimination.cpp.o.d -o CMakeFiles/obj.dir/Shell/LambdaElimination.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/LambdaElimination.cpp [88/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/AcyclicityIndex.cpp.o -MF CMakeFiles/obj.dir/Indexing/AcyclicityIndex.cpp.o.d -o CMakeFiles/obj.dir/Indexing/AcyclicityIndex.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/AcyclicityIndex.cpp [89/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/ClauseCodeTree.cpp.o -MF CMakeFiles/obj.dir/Indexing/ClauseCodeTree.cpp.o.d -o CMakeFiles/obj.dir/Indexing/ClauseCodeTree.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/ClauseCodeTree.cpp [90/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/CodeTree.cpp.o -MF CMakeFiles/obj.dir/Indexing/CodeTree.cpp.o.d -o CMakeFiles/obj.dir/Indexing/CodeTree.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/CodeTree.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/CodeTree.cpp: In member function ‘bool Indexing::CodeTree::CodeOp::equalsForOpMatching(const Indexing::CodeTree::CodeOp&) const’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/CodeTree.cpp:385:1: warning: control reaches end of non-void function [-Wreturn-type] 385 | } | ^ [91/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/ClauseVariantIndex.cpp.o -MF CMakeFiles/obj.dir/Indexing/ClauseVariantIndex.cpp.o.d -o CMakeFiles/obj.dir/Indexing/ClauseVariantIndex.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/ClauseVariantIndex.cpp [92/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/CodeTreeInterfaces.cpp.o -MF CMakeFiles/obj.dir/Indexing/CodeTreeInterfaces.cpp.o.d -o CMakeFiles/obj.dir/Indexing/CodeTreeInterfaces.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/CodeTreeInterfaces.cpp [93/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/GroundingIndex.cpp.o -MF CMakeFiles/obj.dir/Indexing/GroundingIndex.cpp.o.d -o CMakeFiles/obj.dir/Indexing/GroundingIndex.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/GroundingIndex.cpp [94/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/Index.cpp.o -MF CMakeFiles/obj.dir/Indexing/Index.cpp.o.d -o CMakeFiles/obj.dir/Indexing/Index.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/Index.cpp [95/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/LiteralMiniIndex.cpp.o -MF CMakeFiles/obj.dir/Indexing/LiteralMiniIndex.cpp.o.d -o CMakeFiles/obj.dir/Indexing/LiteralMiniIndex.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/LiteralMiniIndex.cpp [96/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/LiteralIndex.cpp.o -MF CMakeFiles/obj.dir/Indexing/LiteralIndex.cpp.o.d -o CMakeFiles/obj.dir/Indexing/LiteralIndex.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/LiteralIndex.cpp [97/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/IndexManager.cpp.o -MF CMakeFiles/obj.dir/Indexing/IndexManager.cpp.o.d -o CMakeFiles/obj.dir/Indexing/IndexManager.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/IndexManager.cpp [98/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/ResultSubstitution.cpp.o -MF CMakeFiles/obj.dir/Indexing/ResultSubstitution.cpp.o.d -o CMakeFiles/obj.dir/Indexing/ResultSubstitution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/ResultSubstitution.cpp [99/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/LiteralSubstitutionTree.cpp.o -MF CMakeFiles/obj.dir/Indexing/LiteralSubstitutionTree.cpp.o.d -o CMakeFiles/obj.dir/Indexing/LiteralSubstitutionTree.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/LiteralSubstitutionTree.cpp [100/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/SubstitutionTree.cpp.o -MF CMakeFiles/obj.dir/Indexing/SubstitutionTree.cpp.o.d -o CMakeFiles/obj.dir/Indexing/SubstitutionTree.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree.cpp [101/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastGen.cpp.o -MF CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastGen.cpp.o.d -o CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastGen.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastGen.cpp In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree.hpp:30, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastGen.cpp:22: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/SkipList.hpp: In instantiation of ‘Lib::List* Lib::SkipList::toList() [with Value = Indexing::SubstitutionTree::Node*; ValueComparator = Indexing::SubstitutionTree::SListIntermediateNode::NodePtrComparator]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastGen.cpp:680:65: required from here /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/SkipList.hpp:521:56: warning: dereferencing type-punned pointer will break strict-aliasing rules [-Wstrict-aliasing] 521 | return reinterpret_cast*&>(_left->nodes[0]); | ~~~~~~~~~~~~^ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastGen.cpp: In member function ‘bool Indexing::SubstitutionTree::FastGeneralizationsIterator::findNextLeaf()’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastGen.cpp:570:26: warning: ‘currSpecVar’ may be used uninitialized [-Wmaybe-uninitialized] 570 | if(!_subst->matchNext(currSpecVar, curr->term, sibilingsRemain)) { //[1] | ~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastGen.cpp:500:14: note: ‘currSpecVar’ was declared here 500 | unsigned currSpecVar; | ^~~~~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastGen.cpp:556:7: warning: ‘sibilingsRemain’ may be used uninitialized [-Wmaybe-uninitialized] 556 | if(sibilingsRemain) { | ^~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastGen.cpp:480:8: note: ‘sibilingsRemain’ was declared here 480 | bool sibilingsRemain; | ^~~~~~~~~~~~~~~ [102/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/SubstitutionTree_Nodes.cpp.o -MF CMakeFiles/obj.dir/Indexing/SubstitutionTree_Nodes.cpp.o.d -o CMakeFiles/obj.dir/Indexing/SubstitutionTree_Nodes.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_Nodes.cpp [103/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/TermCodeTree.cpp.o -MF CMakeFiles/obj.dir/Indexing/TermCodeTree.cpp.o.d -o CMakeFiles/obj.dir/Indexing/TermCodeTree.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/TermCodeTree.cpp [104/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/TermIndex.cpp.o -MF CMakeFiles/obj.dir/Indexing/TermIndex.cpp.o.d -o CMakeFiles/obj.dir/Indexing/TermIndex.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/TermIndex.cpp [105/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastInst.cpp.o -MF CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastInst.cpp.o.d -o CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastInst.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastInst.cpp In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree.hpp:30, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastInst.cpp:23: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/SkipList.hpp: In instantiation of ‘Lib::List* Lib::SkipList::toList() [with Value = Indexing::SubstitutionTree::Node*; ValueComparator = Indexing::SubstitutionTree::SListIntermediateNode::NodePtrComparator]’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/SubstitutionTree_FastInst.cpp:887:65: required from here /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/SkipList.hpp:521:56: warning: dereferencing type-punned pointer will break strict-aliasing rules [-Wstrict-aliasing] 521 | return reinterpret_cast*&>(_left->nodes[0]); | ~~~~~~~~~~~~^ [106/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/TermSharing.cpp.o -MF CMakeFiles/obj.dir/Indexing/TermSharing.cpp.o.d -o CMakeFiles/obj.dir/Indexing/TermSharing.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/TermSharing.cpp [107/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/BackwardDemodulation.cpp.o -MF CMakeFiles/obj.dir/Inferences/BackwardDemodulation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/BackwardDemodulation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/BackwardDemodulation.cpp [108/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Indexing/TermSubstitutionTree.cpp.o -MF CMakeFiles/obj.dir/Indexing/TermSubstitutionTree.cpp.o.d -o CMakeFiles/obj.dir/Indexing/TermSubstitutionTree.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Indexing/TermSubstitutionTree.cpp [109/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/BackwardSubsumptionResolution.cpp.o -MF CMakeFiles/obj.dir/Inferences/BackwardSubsumptionResolution.cpp.o.d -o CMakeFiles/obj.dir/Inferences/BackwardSubsumptionResolution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/BackwardSubsumptionResolution.cpp [110/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/BackwardSubsumptionDemodulation.cpp.o -MF CMakeFiles/obj.dir/Inferences/BackwardSubsumptionDemodulation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/BackwardSubsumptionDemodulation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/BackwardSubsumptionDemodulation.cpp [111/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Condensation.cpp.o -MF CMakeFiles/obj.dir/Inferences/Condensation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Condensation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Condensation.cpp [112/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/DistinctEqualitySimplifier.cpp.o -MF CMakeFiles/obj.dir/Inferences/DistinctEqualitySimplifier.cpp.o.d -o CMakeFiles/obj.dir/Inferences/DistinctEqualitySimplifier.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/DistinctEqualitySimplifier.cpp [113/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/BinaryResolution.cpp.o -MF CMakeFiles/obj.dir/Inferences/BinaryResolution.cpp.o.d -o CMakeFiles/obj.dir/Inferences/BinaryResolution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/BinaryResolution.cpp [114/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/EqualityFactoring.cpp.o -MF CMakeFiles/obj.dir/Inferences/EqualityFactoring.cpp.o.d -o CMakeFiles/obj.dir/Inferences/EqualityFactoring.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/EqualityFactoring.cpp [115/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/EqualityResolution.cpp.o -MF CMakeFiles/obj.dir/Inferences/EqualityResolution.cpp.o.d -o CMakeFiles/obj.dir/Inferences/EqualityResolution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/EqualityResolution.cpp [116/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Factoring.cpp.o -MF CMakeFiles/obj.dir/Inferences/Factoring.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Factoring.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Factoring.cpp [117/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/FOOLParamodulation.cpp.o -MF CMakeFiles/obj.dir/Inferences/FOOLParamodulation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/FOOLParamodulation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/FOOLParamodulation.cpp [118/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/FastCondensation.cpp.o -MF CMakeFiles/obj.dir/Inferences/FastCondensation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/FastCondensation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/FastCondensation.cpp [119/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/ExtensionalityResolution.cpp.o -MF CMakeFiles/obj.dir/Inferences/ExtensionalityResolution.cpp.o.d -o CMakeFiles/obj.dir/Inferences/ExtensionalityResolution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/ExtensionalityResolution.cpp [120/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/ForwardDemodulation.cpp.o -MF CMakeFiles/obj.dir/Inferences/ForwardDemodulation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/ForwardDemodulation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/ForwardDemodulation.cpp [121/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/ForwardLiteralRewriting.cpp.o -MF CMakeFiles/obj.dir/Inferences/ForwardLiteralRewriting.cpp.o.d -o CMakeFiles/obj.dir/Inferences/ForwardLiteralRewriting.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/ForwardLiteralRewriting.cpp [122/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/ForwardSubsumptionAndResolution.cpp.o -MF CMakeFiles/obj.dir/Inferences/ForwardSubsumptionAndResolution.cpp.o.d -o CMakeFiles/obj.dir/Inferences/ForwardSubsumptionAndResolution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/ForwardSubsumptionAndResolution.cpp [123/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/ForwardSubsumptionDemodulation.cpp.o -MF CMakeFiles/obj.dir/Inferences/ForwardSubsumptionDemodulation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/ForwardSubsumptionDemodulation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/ForwardSubsumptionDemodulation.cpp [124/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/InnerRewriting.cpp.o -MF CMakeFiles/obj.dir/Inferences/InnerRewriting.cpp.o.d -o CMakeFiles/obj.dir/Inferences/InnerRewriting.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/InnerRewriting.cpp [125/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/HyperSuperposition.cpp.o -MF CMakeFiles/obj.dir/Inferences/HyperSuperposition.cpp.o.d -o CMakeFiles/obj.dir/Inferences/HyperSuperposition.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/HyperSuperposition.cpp [126/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/GlobalSubsumption.cpp.o -MF CMakeFiles/obj.dir/Inferences/GlobalSubsumption.cpp.o.d -o CMakeFiles/obj.dir/Inferences/GlobalSubsumption.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/GlobalSubsumption.cpp [127/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/EquationalTautologyRemoval.cpp.o -MF CMakeFiles/obj.dir/Inferences/EquationalTautologyRemoval.cpp.o.d -o CMakeFiles/obj.dir/Inferences/EquationalTautologyRemoval.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/EquationalTautologyRemoval.cpp [128/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/InductionHelper.cpp.o -MF CMakeFiles/obj.dir/Inferences/InductionHelper.cpp.o.d -o CMakeFiles/obj.dir/Inferences/InductionHelper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/InductionHelper.cpp [129/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/InterpretedEvaluation.cpp.o -MF CMakeFiles/obj.dir/Inferences/InterpretedEvaluation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/InterpretedEvaluation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/InterpretedEvaluation.cpp [130/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Instantiation.cpp.o -MF CMakeFiles/obj.dir/Inferences/Instantiation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Instantiation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Instantiation.cpp [131/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/InferenceEngine.cpp.o -MF CMakeFiles/obj.dir/Inferences/InferenceEngine.cpp.o.d -o CMakeFiles/obj.dir/Inferences/InferenceEngine.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/InferenceEngine.cpp [132/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/PushUnaryMinus.cpp.o -MF CMakeFiles/obj.dir/Inferences/PushUnaryMinus.cpp.o.d -o CMakeFiles/obj.dir/Inferences/PushUnaryMinus.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/PushUnaryMinus.cpp [133/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Induction.cpp.o -MF CMakeFiles/obj.dir/Inferences/Induction.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Induction.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Induction.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Induction.cpp: In member function ‘void Inferences::InductionClauseIterator::performStructInductionTwo(Kernel::Clause*, Kernel::Literal*, Kernel::Literal*, Kernel::Term*, Kernel::InferenceRule)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Induction.cpp:890:127: warning: ‘’ may be used uninitialized [-Wmaybe-uninitialized] 890 | Connective::AND,new FormulaList(new AtomicFormula(Ly),formulas))) | ^ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Induction.cpp:890:128: warning: ‘’ may be used uninitialized [-Wmaybe-uninitialized] 890 | Connective::AND,new FormulaList(new AtomicFormula(Ly),formulas))) | ^ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Induction.cpp:890:117: warning: ‘’ may be used uninitialized [-Wmaybe-uninitialized] 890 | Connective::AND,new FormulaList(new AtomicFormula(Ly),formulas))) | ^ [134/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/NumTraits.cpp.o -MF CMakeFiles/obj.dir/Kernel/NumTraits.cpp.o.d -o CMakeFiles/obj.dir/Kernel/NumTraits.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/NumTraits.cpp [135/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/GaussianVariableElimination.cpp.o -MF CMakeFiles/obj.dir/Inferences/GaussianVariableElimination.cpp.o.d -o CMakeFiles/obj.dir/Inferences/GaussianVariableElimination.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/GaussianVariableElimination.cpp [136/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/Rebalancing/Inverters.cpp.o -MF CMakeFiles/obj.dir/Kernel/Rebalancing/Inverters.cpp.o.d -o CMakeFiles/obj.dir/Kernel/Rebalancing/Inverters.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Rebalancing/Inverters.cpp [137/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Cancellation.cpp.o -MF CMakeFiles/obj.dir/Inferences/Cancellation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Cancellation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Cancellation.cpp [138/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/TautologyDeletionISE.cpp.o -MF CMakeFiles/obj.dir/Inferences/TautologyDeletionISE.cpp.o.d -o CMakeFiles/obj.dir/Inferences/TautologyDeletionISE.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/TautologyDeletionISE.cpp [139/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/SLQueryBackwardSubsumption.cpp.o -MF CMakeFiles/obj.dir/Inferences/SLQueryBackwardSubsumption.cpp.o.d -o CMakeFiles/obj.dir/Inferences/SLQueryBackwardSubsumption.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/SLQueryBackwardSubsumption.cpp [140/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/Superposition.cpp.o -MF CMakeFiles/obj.dir/Inferences/Superposition.cpp.o.d -o CMakeFiles/obj.dir/Inferences/Superposition.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/Superposition.cpp [141/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/TermAlgebraReasoning.cpp.o -MF CMakeFiles/obj.dir/Inferences/TermAlgebraReasoning.cpp.o.d -o CMakeFiles/obj.dir/Inferences/TermAlgebraReasoning.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/TermAlgebraReasoning.cpp [142/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/URResolution.cpp.o -MF CMakeFiles/obj.dir/Inferences/URResolution.cpp.o.d -o CMakeFiles/obj.dir/Inferences/URResolution.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/URResolution.cpp [143/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/ArithmeticSubtermGeneralization.cpp.o -MF CMakeFiles/obj.dir/Inferences/ArithmeticSubtermGeneralization.cpp.o.d -o CMakeFiles/obj.dir/Inferences/ArithmeticSubtermGeneralization.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/ArithmeticSubtermGeneralization.cpp [144/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/SubsumptionDemodulationHelper.cpp.o -MF CMakeFiles/obj.dir/Inferences/SubsumptionDemodulationHelper.cpp.o.d -o CMakeFiles/obj.dir/Inferences/SubsumptionDemodulationHelper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/SubsumptionDemodulationHelper.cpp [145/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/InstGen/ModelPrinter.cpp.o -MF CMakeFiles/obj.dir/InstGen/ModelPrinter.cpp.o.d -o CMakeFiles/obj.dir/InstGen/ModelPrinter.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/InstGen/ModelPrinter.cpp [146/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/TheoryInstAndSimp.cpp.o -MF CMakeFiles/obj.dir/Inferences/TheoryInstAndSimp.cpp.o.d -o CMakeFiles/obj.dir/Inferences/TheoryInstAndSimp.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/TheoryInstAndSimp.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/TheoryInstAndSimp.cpp: In lambda function: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/TheoryInstAndSimp.cpp:564:10: warning: unused variable ‘res’ [-Wunused-variable] 564 | auto res = _solver->solveUnderAssumptions(theoryLits, 0, false); | ^~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/TheoryInstAndSimp.cpp: In function ‘Kernel::Clause* Inferences::instantiate(Kernel::Clause*, Kernel::Substitution&, const Lib::Stack&, Saturation::Splitter*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/TheoryInstAndSimp.cpp:693:12: warning: variable ‘t’ set but not used [-Wunused-but-set-variable] 693 | auto t = iter.next(); | ^ [147/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Inferences/PolynomialEvaluation.cpp.o -MF CMakeFiles/obj.dir/Inferences/PolynomialEvaluation.cpp.o.d -o CMakeFiles/obj.dir/Inferences/PolynomialEvaluation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Inferences/PolynomialEvaluation.cpp [148/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/BufferedSolver.cpp.o -MF CMakeFiles/obj.dir/SAT/BufferedSolver.cpp.o.d -o CMakeFiles/obj.dir/SAT/BufferedSolver.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/BufferedSolver.cpp [149/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/FallbackSolverWrapper.cpp.o -MF CMakeFiles/obj.dir/SAT/FallbackSolverWrapper.cpp.o.d -o CMakeFiles/obj.dir/SAT/FallbackSolverWrapper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/FallbackSolverWrapper.cpp [150/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/DIMACS.cpp.o -MF CMakeFiles/obj.dir/SAT/DIMACS.cpp.o.d -o CMakeFiles/obj.dir/SAT/DIMACS.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/DIMACS.cpp [151/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/MinimizingSolver.cpp.o -MF CMakeFiles/obj.dir/SAT/MinimizingSolver.cpp.o.d -o CMakeFiles/obj.dir/SAT/MinimizingSolver.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/MinimizingSolver.cpp [152/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/Preprocess.cpp.o -MF CMakeFiles/obj.dir/SAT/Preprocess.cpp.o.d -o CMakeFiles/obj.dir/SAT/Preprocess.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/Preprocess.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/Preprocess.cpp: In static member function ‘static void SAT::Preprocess::propagateUnits(SAT::SATClauseIterator, SAT::SATClauseIterator&, SAT::SATClauseIterator&)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/Preprocess.cpp:217:10: warning: variable ‘kept_assigned’ set but not used [-Wunused-but-set-variable] 217 | bool kept_assigned = false; | ^~~~~~~~~~~~~ [153/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/SAT2FO.cpp.o -MF CMakeFiles/obj.dir/SAT/SAT2FO.cpp.o.d -o CMakeFiles/obj.dir/SAT/SAT2FO.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/SAT2FO.cpp [154/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/SATClause.cpp.o -MF CMakeFiles/obj.dir/SAT/SATClause.cpp.o.d -o CMakeFiles/obj.dir/SAT/SATClause.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/SATClause.cpp In file included from /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/include/g++-v12/ios:40, from /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/include/g++-v12/ostream:38, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/SATClause.cpp:16: In static member function ‘static std::char_traits::char_type* std::char_traits::copy(char_type*, const char_type*, std::size_t)’, inlined from ‘static void std::__cxx11::basic_string<_CharT, _Traits, _Alloc>::_S_copy(_CharT*, const _CharT*, size_type) [with _CharT = char; _Traits = std::char_traits; _Alloc = Lib::STLAllocator]’ at /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/include/g++-v12/bits/basic_string.h:422:21, inlined from ‘static void std::__cxx11::basic_string<_CharT, _Traits, _Alloc>::_S_copy(_CharT*, const _CharT*, size_type) [with _CharT = char; _Traits = std::char_traits; _Alloc = Lib::STLAllocator]’ at /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/include/g++-v12/bits/basic_string.h:417:7, inlined from ‘std::__cxx11::basic_string<_CharT, _Traits, _Alloc>& std::__cxx11::basic_string<_CharT, _Traits, _Alloc>::_M_replace(size_type, size_type, const _CharT*, size_type) [with _CharT = char; _Traits = std::char_traits; _Alloc = Lib::STLAllocator]’ at /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/include/g++-v12/bits/basic_string.tcc:532:22, inlined from ‘std::__cxx11::basic_string<_CharT, _Traits, _Alloc>& std::__cxx11::basic_string<_CharT, _Traits, _Alloc>::assign(const _CharT*) [with _CharT = char; _Traits = std::char_traits; _Alloc = Lib::STLAllocator]’ at /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/include/g++-v12/bits/basic_string.h:1646:19, inlined from ‘std::__cxx11::basic_string<_CharT, _Traits, _Alloc>& std::__cxx11::basic_string<_CharT, _Traits, _Alloc>::operator=(const _CharT*) [with _CharT = char; _Traits = std::char_traits; _Alloc = Lib::STLAllocator]’ at /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/include/g++-v12/bits/basic_string.h:814:28, inlined from ‘Lib::vstring SAT::SATClause::toString() const’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/SATClause.cpp:271:14: /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/include/g++-v12/bits/char_traits.h:431:56: warning: ‘void* __builtin_memcpy(void*, const void*, long unsigned int)’ accessing 9223372036854775810 or more bytes at offsets [2, 9223372036854775807] and 17 may overlap up to 9223372036854775813 bytes at offset -3 [-Wrestrict] 431 | return static_cast(__builtin_memcpy(__s1, __s2, __n)); | ~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~ [155/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/SATLiteral.cpp.o -MF CMakeFiles/obj.dir/SAT/SATLiteral.cpp.o.d -o CMakeFiles/obj.dir/SAT/SATLiteral.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/SATLiteral.cpp [156/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/SATInference.cpp.o -MF CMakeFiles/obj.dir/SAT/SATInference.cpp.o.d -o CMakeFiles/obj.dir/SAT/SATInference.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/SATInference.cpp [157/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/DP/ShortConflictMetaDP.cpp.o -MF CMakeFiles/obj.dir/DP/ShortConflictMetaDP.cpp.o.d -o CMakeFiles/obj.dir/DP/ShortConflictMetaDP.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/DP/ShortConflictMetaDP.cpp [158/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/AWPassiveClauseContainer.cpp.o -MF CMakeFiles/obj.dir/Saturation/AWPassiveClauseContainer.cpp.o.d -o CMakeFiles/obj.dir/Saturation/AWPassiveClauseContainer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/AWPassiveClauseContainer.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/AWPassiveClauseContainer.cpp: In member function ‘virtual void Saturation::AWPassiveClauseContainer::remove(Kernel::Clause*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/AWPassiveClauseContainer.cpp:227:3: warning: ‘wasRemoved’ may be used uninitialized [-Wmaybe-uninitialized] 227 | if (wasRemoved) { | ^~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/AWPassiveClauseContainer.cpp:219:8: note: ‘wasRemoved’ was declared here 219 | bool wasRemoved; // will be assigned, since at least one of the following checks succeeds | ^~~~~~~~~~ [159/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/DP/SimpleCongruenceClosure.cpp.o -MF CMakeFiles/obj.dir/DP/SimpleCongruenceClosure.cpp.o.d -o CMakeFiles/obj.dir/DP/SimpleCongruenceClosure.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/DP/SimpleCongruenceClosure.cpp [160/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/ManCSPassiveClauseContainer.cpp.o -MF CMakeFiles/obj.dir/Saturation/ManCSPassiveClauseContainer.cpp.o.d -o CMakeFiles/obj.dir/Saturation/ManCSPassiveClauseContainer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/ManCSPassiveClauseContainer.cpp [161/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/ClauseContainer.cpp.o -MF CMakeFiles/obj.dir/Saturation/ClauseContainer.cpp.o.d -o CMakeFiles/obj.dir/Saturation/ClauseContainer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/ClauseContainer.cpp [162/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/ConsequenceFinder.cpp.o -MF CMakeFiles/obj.dir/Saturation/ConsequenceFinder.cpp.o.d -o CMakeFiles/obj.dir/Saturation/ConsequenceFinder.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/ConsequenceFinder.cpp [163/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/Z3Interfacing.cpp.o -MF CMakeFiles/obj.dir/SAT/Z3Interfacing.cpp.o.d -o CMakeFiles/obj.dir/SAT/Z3Interfacing.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/Z3Interfacing.cpp [164/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/InstGen/IGAlgorithm.cpp.o -MF CMakeFiles/obj.dir/InstGen/IGAlgorithm.cpp.o.d -o CMakeFiles/obj.dir/InstGen/IGAlgorithm.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/InstGen/IGAlgorithm.cpp [165/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/Discount.cpp.o -MF CMakeFiles/obj.dir/Saturation/Discount.cpp.o.d -o CMakeFiles/obj.dir/Saturation/Discount.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Discount.cpp [166/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/ExtensionalityClauseContainer.cpp.o -MF CMakeFiles/obj.dir/Saturation/ExtensionalityClauseContainer.cpp.o.d -o CMakeFiles/obj.dir/Saturation/ExtensionalityClauseContainer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/ExtensionalityClauseContainer.cpp [167/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/LabelFinder.cpp.o -MF CMakeFiles/obj.dir/Saturation/LabelFinder.cpp.o.d -o CMakeFiles/obj.dir/Saturation/LabelFinder.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/LabelFinder.cpp [168/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/LRS.cpp.o -MF CMakeFiles/obj.dir/Saturation/LRS.cpp.o.d -o CMakeFiles/obj.dir/Saturation/LRS.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/LRS.cpp [169/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/Otter.cpp.o -MF CMakeFiles/obj.dir/Saturation/Otter.cpp.o.d -o CMakeFiles/obj.dir/Saturation/Otter.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Otter.cpp [170/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/ProvingHelper.cpp.o -MF CMakeFiles/obj.dir/Saturation/ProvingHelper.cpp.o.d -o CMakeFiles/obj.dir/Saturation/ProvingHelper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/ProvingHelper.cpp [171/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/SymElOutput.cpp.o -MF CMakeFiles/obj.dir/Saturation/SymElOutput.cpp.o.d -o CMakeFiles/obj.dir/Saturation/SymElOutput.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/SymElOutput.cpp [172/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/PredicateSplitPassiveClauseContainer.cpp.o -MF CMakeFiles/obj.dir/Saturation/PredicateSplitPassiveClauseContainer.cpp.o.d -o CMakeFiles/obj.dir/Saturation/PredicateSplitPassiveClauseContainer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/PredicateSplitPassiveClauseContainer.cpp [173/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/SaturationAlgorithm.cpp.o -MF CMakeFiles/obj.dir/Saturation/SaturationAlgorithm.cpp.o.d -o CMakeFiles/obj.dir/Saturation/SaturationAlgorithm.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/SaturationAlgorithm.cpp [174/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Saturation/Splitter.cpp.o -MF CMakeFiles/obj.dir/Saturation/Splitter.cpp.o.d -o CMakeFiles/obj.dir/Saturation/Splitter.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp: In member function ‘Kernel::Unit* Saturation::Splitter::getDefinitionFromName(Kernel::SplitLevel) const’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp:772:10: warning: ‘def’ may be used uninitialized [-Wmaybe-uninitialized] 772 | return def; | ^~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp:770:9: note: ‘def’ was declared here 770 | Unit* def; | ^~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp: In member function ‘bool Saturation::Splitter::handleNonSplittable(Kernel::Clause*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp:770:9: warning: ‘def’ may be used uninitialized [-Wmaybe-uninitialized] In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Backtrackable.hpp:18, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Stack.hpp:28, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.hpp:23, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp:15: In constructor ‘Lib::List::List(C, Lib::List*) [with C = Kernel::Unit*]’, inlined from ‘static Lib::List* Lib::List::cons(C, Lib::List*) [with C = Kernel::Unit*]’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/List.hpp:248:12, inlined from ‘static void Lib::List::push(C, Lib::List*&) [with C = Kernel::Unit*]’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/List.hpp:260:15, inlined from ‘bool Saturation::Splitter::handleNonSplittable(Kernel::Clause*)’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp:966:19: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/List.hpp:77:5: warning: ‘def’ may be used uninitialized [-Wmaybe-uninitialized] 77 | _head(head), | ^~~~~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp: In member function ‘bool Saturation::Splitter::handleNonSplittable(Kernel::Clause*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp:770:9: note: ‘def’ was declared here 770 | Unit* def; | ^~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp: In member function ‘bool Saturation::Splitter::doSplitting(Kernel::Clause*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp:770:9: warning: ‘def’ may be used uninitialized [-Wmaybe-uninitialized] /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Saturation/Splitter.cpp:770:9: warning: ‘def’ may be used uninitialized [-Wmaybe-uninitialized] [175/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/CNF.cpp.o -MF CMakeFiles/obj.dir/Shell/CNF.cpp.o.d -o CMakeFiles/obj.dir/Shell/CNF.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/CNF.cpp [176/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/CommandLine.cpp.o -MF CMakeFiles/obj.dir/Shell/CommandLine.cpp.o.d -o CMakeFiles/obj.dir/Shell/CommandLine.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/CommandLine.cpp [177/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/DistinctProcessor.cpp.o -MF CMakeFiles/obj.dir/Shell/DistinctProcessor.cpp.o.d -o CMakeFiles/obj.dir/Shell/DistinctProcessor.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/DistinctProcessor.cpp [178/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/DistinctGroupExpansion.cpp.o -MF CMakeFiles/obj.dir/Shell/DistinctGroupExpansion.cpp.o.d -o CMakeFiles/obj.dir/Shell/DistinctGroupExpansion.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/DistinctGroupExpansion.cpp [179/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/EqResWithDeletion.cpp.o -MF CMakeFiles/obj.dir/Shell/EqResWithDeletion.cpp.o.d -o CMakeFiles/obj.dir/Shell/EqResWithDeletion.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/EqResWithDeletion.cpp [180/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/EqualityProxy.cpp.o -MF CMakeFiles/obj.dir/Shell/EqualityProxy.cpp.o.d -o CMakeFiles/obj.dir/Shell/EqualityProxy.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/EqualityProxy.cpp [181/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/NewCNF.cpp.o -MF CMakeFiles/obj.dir/Shell/NewCNF.cpp.o.d -o CMakeFiles/obj.dir/Shell/NewCNF.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/NewCNF.cpp In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/DHSet.hpp:21, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Metaiterators.hpp:26, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Map.hpp:28, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/OperatorType.hpp:21, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/NewCNF.cpp:18: In member function ‘bool Lib::DHMap::insert(Key, const Val&) [with Key = unsigned int; Val = Kernel::TermList; Hash1 = Lib::IdentityHash; Hash2 = Lib::Hash]’, inlined from ‘void Shell::NewCNF::createFreshVariableRenaming(unsigned int, unsigned int)’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/NewCNF.cpp:429:24: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/DHMap.hpp:313:25: warning: ‘sort’ may be used uninitialized [-Wmaybe-uninitialized] 313 | return emplace(key, Val(val)); | ^~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/NewCNF.cpp: In member function ‘void Shell::NewCNF::createFreshVariableRenaming(unsigned int, unsigned int)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/NewCNF.cpp:427:12: note: ‘sort’ declared here 427 | TermList sort; | ^~~~ [182/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Flattening.cpp.o -MF CMakeFiles/obj.dir/Shell/Flattening.cpp.o.d -o CMakeFiles/obj.dir/Shell/Flattening.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Flattening.cpp [183/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/EqualityProxyMono.cpp.o -MF CMakeFiles/obj.dir/Shell/EqualityProxyMono.cpp.o.d -o CMakeFiles/obj.dir/Shell/EqualityProxyMono.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/EqualityProxyMono.cpp [184/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/FunctionDefinition.cpp.o -MF CMakeFiles/obj.dir/Shell/FunctionDefinition.cpp.o.d -o CMakeFiles/obj.dir/Shell/FunctionDefinition.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/FunctionDefinition.cpp In static member function ‘static void Shell::FunctionDefinition::reverse(Def*)’, inlined from ‘bool Shell::FunctionDefinition::removeAllDefinitions(Kernel::UnitList*&)’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/FunctionDefinition.cpp:286:16: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/FunctionDefinition.cpp:258:12: warning: ‘d2’ may be used uninitialized [-Wmaybe-uninitialized] 258 | def->lhs = def->rhs; | ~~~~~~~~~^~~~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/FunctionDefinition.cpp: In member function ‘bool Shell::FunctionDefinition::removeAllDefinitions(Kernel::UnitList*&)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/FunctionDefinition.cpp:284:14: note: ‘d2’ was declared here 284 | Def* d2; | ^~ [185/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/GeneralSplitting.cpp.o -MF CMakeFiles/obj.dir/Shell/GeneralSplitting.cpp.o.d -o CMakeFiles/obj.dir/Shell/GeneralSplitting.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/GeneralSplitting.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/GeneralSplitting.cpp: In member function ‘bool Shell::GeneralSplitting::apply(Kernel::Clause*&, Kernel::UnitList*&)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/GeneralSplitting.cpp:174:12: warning: ‘minDegVar’ may be used uninitialized [-Wmaybe-uninitialized] 174 | unsigned minDegVar; | ^~~~~~~~~ [186/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/GoalGuessing.cpp.o -MF CMakeFiles/obj.dir/Shell/GoalGuessing.cpp.o.d -o CMakeFiles/obj.dir/Shell/GoalGuessing.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/GoalGuessing.cpp [187/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/InequalitySplitting.cpp.o -MF CMakeFiles/obj.dir/Shell/InequalitySplitting.cpp.o.d -o CMakeFiles/obj.dir/Shell/InequalitySplitting.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/InequalitySplitting.cpp [188/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/AnswerExtractor.cpp.o -MF CMakeFiles/obj.dir/Shell/AnswerExtractor.cpp.o.d -o CMakeFiles/obj.dir/Shell/AnswerExtractor.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/AnswerExtractor.cpp [189/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Grounding.cpp.o -MF CMakeFiles/obj.dir/Shell/Grounding.cpp.o.d -o CMakeFiles/obj.dir/Shell/Grounding.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Grounding.cpp [190/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Interpolants.cpp.o -MF CMakeFiles/obj.dir/Shell/Interpolants.cpp.o.d -o CMakeFiles/obj.dir/Shell/Interpolants.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Interpolants.cpp [191/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/InterpolantMinimizer.cpp.o -MF CMakeFiles/obj.dir/Shell/InterpolantMinimizer.cpp.o.d -o CMakeFiles/obj.dir/Shell/InterpolantMinimizer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/InterpolantMinimizer.cpp [192/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/InterpolantsNew.cpp.o -MF CMakeFiles/obj.dir/Shell/InterpolantsNew.cpp.o.d -o CMakeFiles/obj.dir/Shell/InterpolantsNew.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/InterpolantsNew.cpp [193/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/InterpolantMinimizerNew.cpp.o -MF CMakeFiles/obj.dir/Shell/InterpolantMinimizerNew.cpp.o.d -o CMakeFiles/obj.dir/Shell/InterpolantMinimizerNew.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/InterpolantMinimizerNew.cpp [194/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Lexer.cpp.o -MF CMakeFiles/obj.dir/Shell/Lexer.cpp.o.d -o CMakeFiles/obj.dir/Shell/Lexer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Lexer.cpp [195/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/LispLexer.cpp.o -MF CMakeFiles/obj.dir/Shell/LispLexer.cpp.o.d -o CMakeFiles/obj.dir/Shell/LispLexer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/LispLexer.cpp [196/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/InterpretedNormalizer.cpp.o -MF CMakeFiles/obj.dir/Shell/InterpretedNormalizer.cpp.o.d -o CMakeFiles/obj.dir/Shell/InterpretedNormalizer.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/InterpretedNormalizer.cpp [197/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/LispParser.cpp.o -MF CMakeFiles/obj.dir/Shell/LispParser.cpp.o.d -o CMakeFiles/obj.dir/Shell/LispParser.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/LispParser.cpp [198/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/LaTeX.cpp.o -MF CMakeFiles/obj.dir/Shell/LaTeX.cpp.o.d -o CMakeFiles/obj.dir/Shell/LaTeX.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/LaTeX.cpp [199/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/NNF.cpp.o -MF CMakeFiles/obj.dir/Shell/NNF.cpp.o.d -o CMakeFiles/obj.dir/Shell/NNF.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/NNF.cpp [200/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Normalisation.cpp.o -MF CMakeFiles/obj.dir/Shell/Normalisation.cpp.o.d -o CMakeFiles/obj.dir/Shell/Normalisation.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Normalisation.cpp [201/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Naming.cpp.o -MF CMakeFiles/obj.dir/Shell/Naming.cpp.o.d -o CMakeFiles/obj.dir/Shell/Naming.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Naming.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Naming.cpp: In member function ‘Kernel::Formula* Shell::Naming::apply_iter(Kernel::Formula*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Naming.cpp:294:15: warning: ‘canBeDef’ may be used uninitialized [-Wmaybe-uninitialized] 294 | if (canBeDef) { | ^~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Naming.cpp:278:16: note: ‘canBeDef’ was declared here 278 | bool canBeDef; | ^~~~~~~~ [202/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/PredicateDefinition.cpp.o -MF CMakeFiles/obj.dir/Shell/PredicateDefinition.cpp.o.d -o CMakeFiles/obj.dir/Shell/PredicateDefinition.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/PredicateDefinition.cpp [203/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Preprocess.cpp.o -MF CMakeFiles/obj.dir/Shell/Preprocess.cpp.o.d -o CMakeFiles/obj.dir/Shell/Preprocess.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Preprocess.cpp [204/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Property.cpp.o -MF CMakeFiles/obj.dir/Shell/Property.cpp.o.d -o CMakeFiles/obj.dir/Shell/Property.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Property.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Property.cpp: In static member function ‘static Lib::vstring Shell::Property::categoryToString(Category)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Property.cpp:832:1: warning: control reaches end of non-void function [-Wreturn-type] 832 | } // categoryString | ^ [205/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/SimplifyFalseTrue.cpp.o -MF CMakeFiles/obj.dir/Shell/SimplifyFalseTrue.cpp.o.d -o CMakeFiles/obj.dir/Shell/SimplifyFalseTrue.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/SimplifyFalseTrue.cpp [206/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Rectify.cpp.o -MF CMakeFiles/obj.dir/Shell/Rectify.cpp.o.d -o CMakeFiles/obj.dir/Shell/Rectify.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Rectify.cpp [207/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Skolem.cpp.o -MF CMakeFiles/obj.dir/Shell/Skolem.cpp.o.d -o CMakeFiles/obj.dir/Shell/Skolem.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Skolem.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Skolem.cpp: In member function ‘void Shell::Skolem::preskolemise(Kernel::Formula*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Skolem.cpp:223:46: warning: ‘varOccInfo.Shell::Skolem::VarOccInfo::occurs_below’ may be used uninitialized [-Wmaybe-uninitialized] 223 | varOccInfo.occurs_below->headRef() = true; // ... occurs in this literal | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Skolem.cpp:219:20: note: ‘varOccInfo.Shell::Skolem::VarOccInfo::occurs_below’ was declared here 219 | VarOccInfo varOccInfo; | ^~~~~~~~~~ [208/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/SineUtils.cpp.o -MF CMakeFiles/obj.dir/Shell/SineUtils.cpp.o.d -o CMakeFiles/obj.dir/Shell/SineUtils.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/SineUtils.cpp [209/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/SMTFormula.cpp.o -MF CMakeFiles/obj.dir/Shell/SMTFormula.cpp.o.d -o CMakeFiles/obj.dir/Shell/SMTFormula.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/SMTFormula.cpp [210/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/FOOLElimination.cpp.o -MF CMakeFiles/obj.dir/Shell/FOOLElimination.cpp.o.d -o CMakeFiles/obj.dir/Shell/FOOLElimination.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/FOOLElimination.cpp [211/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/SymbolDefinitionInlining.cpp.o -MF CMakeFiles/obj.dir/Shell/SymbolDefinitionInlining.cpp.o.d -o CMakeFiles/obj.dir/Shell/SymbolDefinitionInlining.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/SymbolDefinitionInlining.cpp [212/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Statistics.cpp.o -MF CMakeFiles/obj.dir/Shell/Statistics.cpp.o.d -o CMakeFiles/obj.dir/Shell/Statistics.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Statistics.cpp [213/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/SymbolOccurrenceReplacement.cpp.o -MF CMakeFiles/obj.dir/Shell/SymbolOccurrenceReplacement.cpp.o.d -o CMakeFiles/obj.dir/Shell/SymbolOccurrenceReplacement.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/SymbolOccurrenceReplacement.cpp [214/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/SymCounter.cpp.o -MF CMakeFiles/obj.dir/Shell/SymCounter.cpp.o.d -o CMakeFiles/obj.dir/Shell/SymCounter.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/SymCounter.cpp [215/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/TermAlgebra.cpp.o -MF CMakeFiles/obj.dir/Shell/TermAlgebra.cpp.o.d -o CMakeFiles/obj.dir/Shell/TermAlgebra.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TermAlgebra.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TermAlgebra.cpp: In constructor ‘Shell::TermAlgebraConstructor::TermAlgebraConstructor(unsigned int, Lib::Array)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TermAlgebra.cpp:33:10: warning: unused variable ‘sym’ [-Wunused-variable] 33 | auto sym = _type->arg(i++) == AtomicSort::boolSort() ? env.signature->getPredicate(d) | ^~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TermAlgebra.cpp: In constructor ‘Shell::TermAlgebraConstructor::TermAlgebraConstructor(unsigned int, unsigned int, Lib::Array)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TermAlgebra.cpp:45:13: warning: unused variable ‘d’ [-Wunused-variable] 45 | for (auto d : destructors) { | ^ [216/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/TheoryFinder.cpp.o -MF CMakeFiles/obj.dir/Shell/TheoryFinder.cpp.o.d -o CMakeFiles/obj.dir/Shell/TheoryFinder.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryFinder.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryFinder.cpp: In static member function ‘static bool Shell::TheoryFinder::matchCode(const void*, const unsigned char*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryFinder.cpp:212:8: warning: variable ‘clength_assigned’ set but not used [-Wunused-but-set-variable] 212 | bool clength_assigned = false; | ^~~~~~~~~~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryFinder.cpp:441:5: warning: ‘clength’ may be used uninitialized [-Wmaybe-uninitialized] 441 | if (c == clength) { // no candidate found | ^~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryFinder.cpp:210:7: note: ‘clength’ was declared here 210 | int clength; | ^~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryFinder.cpp:696:26: warning: ‘clause’ may be used uninitialized [-Wmaybe-uninitialized] 696 | objects[objectPos++] = (*clause)[c]; /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryFinder.cpp:208:17: note: ‘clause’ was declared here 208 | const Clause* clause; | ^~~~~~ [217/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/TheoryAxioms.cpp.o -MF CMakeFiles/obj.dir/Shell/TheoryAxioms.cpp.o.d -o CMakeFiles/obj.dir/Shell/TheoryAxioms.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryAxioms.cpp [218/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/TheoryFlattening.cpp.o -MF CMakeFiles/obj.dir/Shell/TheoryFlattening.cpp.o.d -o CMakeFiles/obj.dir/Shell/TheoryFlattening.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TheoryFlattening.cpp [219/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Token.cpp.o -MF CMakeFiles/obj.dir/Shell/Token.cpp.o.d -o CMakeFiles/obj.dir/Shell/Token.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Token.cpp [220/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/BlockedClauseElimination.cpp.o -MF CMakeFiles/obj.dir/Shell/BlockedClauseElimination.cpp.o.d -o CMakeFiles/obj.dir/Shell/BlockedClauseElimination.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/BlockedClauseElimination.cpp [221/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/VarManager.cpp.o -MF CMakeFiles/obj.dir/Shell/VarManager.cpp.o.d -o CMakeFiles/obj.dir/Shell/VarManager.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/VarManager.cpp [222/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/UIHelper.cpp.o -MF CMakeFiles/obj.dir/Shell/UIHelper.cpp.o.d -o CMakeFiles/obj.dir/Shell/UIHelper.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/UIHelper.cpp [223/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/TPTPPrinter.cpp.o -MF CMakeFiles/obj.dir/Shell/TPTPPrinter.cpp.o.d -o CMakeFiles/obj.dir/Shell/TPTPPrinter.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TPTPPrinter.cpp [224/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/UnificationWithAbstractionConfig.cpp.o -MF CMakeFiles/obj.dir/Shell/UnificationWithAbstractionConfig.cpp.o.d -o CMakeFiles/obj.dir/Shell/UnificationWithAbstractionConfig.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/UnificationWithAbstractionConfig.cpp [225/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/SubexpressionIterator.cpp.o -MF CMakeFiles/obj.dir/Shell/SubexpressionIterator.cpp.o.d -o CMakeFiles/obj.dir/Shell/SubexpressionIterator.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/SubexpressionIterator.cpp [226/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/FMB/ClauseFlattening.cpp.o -MF CMakeFiles/obj.dir/FMB/ClauseFlattening.cpp.o.d -o CMakeFiles/obj.dir/FMB/ClauseFlattening.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/ClauseFlattening.cpp [227/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/FMB/FiniteModel.cpp.o -MF CMakeFiles/obj.dir/FMB/FiniteModel.cpp.o.d -o CMakeFiles/obj.dir/FMB/FiniteModel.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/FiniteModel.cpp [228/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Parse/SMTLIB2.cpp.o -MF CMakeFiles/obj.dir/Parse/SMTLIB2.cpp.o.d -o CMakeFiles/obj.dir/Parse/SMTLIB2.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/SMTLIB2.cpp In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/OperatorType.hpp:30, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/TermAlgebra.hpp:19, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Signature.hpp:35, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Formula.hpp:28, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/SMTLIB2.cpp:23: In member function ‘bool Kernel::TermList::isVar() const’, inlined from ‘void Parse::SMTLIB2::parseMatchEnd(Shell::LExpr*)’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/SMTLIB2.cpp:1761:27: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Term.hpp:101:61: warning: ‘varPattern.Kernel::TermList::.Kernel::TermList::::_content’ may be used uninitialized [-Wmaybe-uninitialized] 101 | inline bool isVar() const { return (_content & 0x0001) == 1; } | ^ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/SMTLIB2.cpp: In member function ‘void Parse::SMTLIB2::parseMatchEnd(Shell::LExpr*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/SMTLIB2.cpp:1704:12: note: ‘varPattern.Kernel::TermList::.Kernel::TermList::::_content’ was declared here 1704 | TermList varPattern; | ^~~~~~~~~~ [229/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Parse/TPTP.cpp.o -MF CMakeFiles/obj.dir/Parse/TPTP.cpp.o.d -o CMakeFiles/obj.dir/Parse/TPTP.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp: In member function ‘Kernel::OperatorType* Parse::TPTP::constructOperatorType(Type*, Kernel::VList*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp:3935:16: warning: enumeration value ‘TT_QUANTIFIED’ not handled in switch [-Wswitch] 3935 | switch (tp->tag()) { | ^ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp: In static member function ‘static Lib::vstring Parse::TPTP::toString(Tag)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp:425:1: warning: control reaches end of non-void function [-Wreturn-type] 425 | } // toString(Tag) | ^ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp: In member function ‘void Parse::TPTP::endFormula()’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp:3509:23: warning: ‘c’ may be used uninitialized [-Wmaybe-uninitialized] 3509 | if (higherPrecedence(con,c)) { | ~~~~~~~~~~~~~~~~^~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp:3426:14: note: ‘c’ was declared here 3426 | Connective c; | ^ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp:3492:7: warning: ‘conReverse’ may be used uninitialized [-Wmaybe-uninitialized] 3492 | if (conReverse) { | ^~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp:3389:8: note: ‘conReverse’ was declared here 3389 | bool conReverse; | ^~~~~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp: In member function ‘void Parse::TPTP::endHolFormula()’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp:1914:23: warning: ‘c’ may be used uninitialized [-Wmaybe-uninitialized] 1914 | if (higherPrecedence(con,c)) { | ~~~~~~~~~~~~~~~~^~~~~~~ /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Parse/TPTP.cpp:1811:7: note: ‘c’ was declared here 1811 | int c; | ^ [230/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/FMB/FiniteModelMultiSorted.cpp.o -MF CMakeFiles/obj.dir/FMB/FiniteModelMultiSorted.cpp.o.d -o CMakeFiles/obj.dir/FMB/FiniteModelMultiSorted.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/FiniteModelMultiSorted.cpp [231/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/FMB/Monotonicity.cpp.o -MF CMakeFiles/obj.dir/FMB/Monotonicity.cpp.o.d -o CMakeFiles/obj.dir/FMB/Monotonicity.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/Monotonicity.cpp [232/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/FMB/FiniteModelBuilder.cpp.o -MF CMakeFiles/obj.dir/FMB/FiniteModelBuilder.cpp.o.d -o CMakeFiles/obj.dir/FMB/FiniteModelBuilder.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/FiniteModelBuilder.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/FiniteModelBuilder.cpp: In member function ‘void FMB::FiniteModelBuilder::onModelFound()’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/FiniteModelBuilder.cpp:1893:10: warning: variable ‘found’ set but not used [-Wunused-but-set-variable] 1893 | bool found=false; | ^~~~~ In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Recycler.hpp:22, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Metaiterators.hpp:24, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Kernel/Clause.hpp:27, from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/FiniteModelBuilder.cpp:23: In member function ‘void Lib::Stack::push(C&&) [with C = Kernel::TermList]’, inlined from ‘Kernel::Term* FMB::DefinitionIntroduction::addGroundDefinition(Kernel::Term*, Kernel::Clause*)’ at /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/DefinitionIntroduction.hpp:143:24: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Lib/Stack.hpp:367:5: warning: ‘argT’ may be used uninitialized [-Wmaybe-uninitialized] 367 | ::new(_cursor) C(std::move(elem)); | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In file included from /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/FiniteModelBuilder.cpp:58: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/DefinitionIntroduction.hpp: In member function ‘Kernel::Term* FMB::DefinitionIntroduction::addGroundDefinition(Kernel::Term*, Kernel::Clause*)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/DefinitionIntroduction.hpp:141:21: note: ‘argT’ was declared here 141 | Term* argT; | ^~~~ [233/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/Z3MainLoop.cpp.o -MF CMakeFiles/obj.dir/SAT/Z3MainLoop.cpp.o.d -o CMakeFiles/obj.dir/SAT/Z3MainLoop.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/Z3MainLoop.cpp [234/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/FMB/SortInference.cpp.o -MF CMakeFiles/obj.dir/FMB/SortInference.cpp.o.d -o CMakeFiles/obj.dir/FMB/SortInference.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/SortInference.cpp [235/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Minisat/core/Solver.cc.o -MF CMakeFiles/obj.dir/Minisat/core/Solver.cc.o.d -o CMakeFiles/obj.dir/Minisat/core/Solver.cc.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Minisat/core/Solver.cc [236/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Minisat/utils/Options.cc.o -MF CMakeFiles/obj.dir/Minisat/utils/Options.cc.o.d -o CMakeFiles/obj.dir/Minisat/utils/Options.cc.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Minisat/utils/Options.cc [237/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Minisat/utils/System.cc.o -MF CMakeFiles/obj.dir/Minisat/utils/System.cc.o.d -o CMakeFiles/obj.dir/Minisat/utils/System.cc.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Minisat/utils/System.cc [238/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Minisat/simp/SimpSolver.cc.o -MF CMakeFiles/obj.dir/Minisat/simp/SimpSolver.cc.o.d -o CMakeFiles/obj.dir/Minisat/simp/SimpSolver.cc.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Minisat/simp/SimpSolver.cc [239/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/FMB/FunctionRelationshipInference.cpp.o -MF CMakeFiles/obj.dir/FMB/FunctionRelationshipInference.cpp.o.d -o CMakeFiles/obj.dir/FMB/FunctionRelationshipInference.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/FMB/FunctionRelationshipInference.cpp [240/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/MinisatInterfacing.cpp.o -MF CMakeFiles/obj.dir/SAT/MinisatInterfacing.cpp.o.d -o CMakeFiles/obj.dir/SAT/MinisatInterfacing.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/MinisatInterfacing.cpp [241/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/SAT/MinisatInterfacingNewSimp.cpp.o -MF CMakeFiles/obj.dir/SAT/MinisatInterfacingNewSimp.cpp.o.d -o CMakeFiles/obj.dir/SAT/MinisatInterfacingNewSimp.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/SAT/MinisatInterfacingNewSimp.cpp [242/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/CASC/ScheduleExecutor.cpp.o -MF CMakeFiles/obj.dir/CASC/ScheduleExecutor.cpp.o.d -o CMakeFiles/obj.dir/CASC/ScheduleExecutor.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/CASC/ScheduleExecutor.cpp [243/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/CASC/PortfolioMode.cpp.o -MF CMakeFiles/obj.dir/CASC/PortfolioMode.cpp.o.d -o CMakeFiles/obj.dir/CASC/PortfolioMode.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/CASC/PortfolioMode.cpp [244/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/Shell/Options.cpp.o -MF CMakeFiles/obj.dir/Shell/Options.cpp.o.d -o CMakeFiles/obj.dir/Shell/Options.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Options.cpp /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Options.cpp: In member function ‘virtual bool Shell::Options::TimeLimitOptionValue::setValue(const Lib::vstring&)’: /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/Shell/Options.cpp:2734:10: warning: ‘char* __builtin_strncpy(char*, const char*, long unsigned int)’ specified bound 128 equals destination size [-Wstringop-truncation] 2734 | strncpy(copy,value.c_str(),COPY_SIZE); | ^ [245/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/version.cpp.o -MF CMakeFiles/obj.dir/version.cpp.o.d -o CMakeFiles/obj.dir/version.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build/version.cpp [246/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/CASC/Schedules.cpp.o -MF CMakeFiles/obj.dir/CASC/Schedules.cpp.o.d -o CMakeFiles/obj.dir/CASC/Schedules.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/CASC/Schedules.cpp [247/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/vampire.dir/vampire.cpp.o -MF CMakeFiles/vampire.dir/vampire.cpp.o.d -o CMakeFiles/vampire.dir/vampire.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/vampire.cpp [248/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/CASC/CLTBMode.cpp.o -MF CMakeFiles/obj.dir/CASC/CLTBMode.cpp.o.d -o CMakeFiles/obj.dir/CASC/CLTBMode.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/CASC/CLTBMode.cpp [249/250] /usr/bin/x86_64-pc-linux-gnu-g++ -DCHECK_LEAKS=0 -DVDEBUG=0 -DVZ3=1 -I/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1 -pipe -march=native -fno-diagnostics-color -O2 -Wall -std=c++14 -MD -MT CMakeFiles/obj.dir/CASC/CLTBModeLearning.cpp.o -MF CMakeFiles/obj.dir/CASC/CLTBModeLearning.cpp.o.d -o CMakeFiles/obj.dir/CASC/CLTBModeLearning.cpp.o -c /var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1/CASC/CLTBModeLearning.cpp [250/250] : && /usr/bin/x86_64-pc-linux-gnu-g++ -pipe -march=native -fno-diagnostics-color -O2 -Wl,-O1 -Wl,--as-needed -Wl,--defsym=__gentoo_check_ldflags__=0 CMakeFiles/obj.dir/Debug/Assertion.cpp.o CMakeFiles/obj.dir/Debug/RuntimeStatistics.cpp.o CMakeFiles/obj.dir/Debug/Tracer.cpp.o CMakeFiles/obj.dir/Lib/Allocator.cpp.o CMakeFiles/obj.dir/Lib/DHMap.cpp.o CMakeFiles/obj.dir/Lib/Environment.cpp.o CMakeFiles/obj.dir/Lib/Event.cpp.o CMakeFiles/obj.dir/Lib/Exception.cpp.o CMakeFiles/obj.dir/Lib/Hash.cpp.o CMakeFiles/obj.dir/Lib/Int.cpp.o CMakeFiles/obj.dir/Lib/IntNameTable.cpp.o CMakeFiles/obj.dir/Lib/IntUnionFind.cpp.o CMakeFiles/obj.dir/Lib/MemoryLeak.cpp.o CMakeFiles/obj.dir/Lib/MultiCounter.cpp.o CMakeFiles/obj.dir/Lib/NameArray.cpp.o CMakeFiles/obj.dir/Lib/Random.cpp.o CMakeFiles/obj.dir/Lib/StringUtils.cpp.o CMakeFiles/obj.dir/Lib/System.cpp.o CMakeFiles/obj.dir/Lib/TimeCounter.cpp.o CMakeFiles/obj.dir/Lib/Timer.cpp.o CMakeFiles/obj.dir/Lib/Sys/Multiprocessing.cpp.o CMakeFiles/obj.dir/Lib/Sys/Semaphore.cpp.o CMakeFiles/obj.dir/Lib/Sys/SyncPipe.cpp.o CMakeFiles/obj.dir/Kernel/Clause.cpp.o CMakeFiles/obj.dir/Kernel/ClauseQueue.cpp.o CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o CMakeFiles/obj.dir/Kernel/ELiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/EqHelper.cpp.o CMakeFiles/obj.dir/Kernel/FlatTerm.cpp.o CMakeFiles/obj.dir/Kernel/Formula.cpp.o CMakeFiles/obj.dir/Kernel/FormulaTransformer.cpp.o CMakeFiles/obj.dir/Kernel/FormulaUnit.cpp.o CMakeFiles/obj.dir/Kernel/FormulaVarIterator.cpp.o CMakeFiles/obj.dir/Kernel/Grounder.cpp.o CMakeFiles/obj.dir/Kernel/Inference.cpp.o CMakeFiles/obj.dir/Kernel/InferenceStore.cpp.o CMakeFiles/obj.dir/Kernel/InterpretedLiteralEvaluator.cpp.o CMakeFiles/obj.dir/Kernel/Rebalancing.cpp.o CMakeFiles/obj.dir/Kernel/KBO.cpp.o CMakeFiles/obj.dir/Kernel/KBOForEPR.cpp.o CMakeFiles/obj.dir/Kernel/LiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/LookaheadLiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/MainLoop.cpp.o CMakeFiles/obj.dir/Kernel/Matcher.cpp.o CMakeFiles/obj.dir/Kernel/MaximalLiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o CMakeFiles/obj.dir/Kernel/MLMatcherSD.cpp.o CMakeFiles/obj.dir/Kernel/MLVariant.cpp.o CMakeFiles/obj.dir/Kernel/Ordering.cpp.o CMakeFiles/obj.dir/Kernel/Ordering_Equality.cpp.o CMakeFiles/obj.dir/Kernel/Problem.cpp.o CMakeFiles/obj.dir/Kernel/Renaming.cpp.o CMakeFiles/obj.dir/Kernel/RobSubstitution.cpp.o CMakeFiles/obj.dir/Kernel/MismatchHandler.cpp.o CMakeFiles/obj.dir/Kernel/Signature.cpp.o CMakeFiles/obj.dir/Kernel/SortHelper.cpp.o CMakeFiles/obj.dir/Kernel/OperatorType.cpp.o CMakeFiles/obj.dir/Kernel/SpassLiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/SubformulaIterator.cpp.o CMakeFiles/obj.dir/Kernel/Substitution.cpp.o CMakeFiles/obj.dir/Kernel/Term.cpp.o CMakeFiles/obj.dir/Kernel/TermIterators.cpp.o CMakeFiles/obj.dir/Kernel/TermTransformer.cpp.o CMakeFiles/obj.dir/Kernel/Theory.cpp.o CMakeFiles/obj.dir/Kernel/Unit.cpp.o CMakeFiles/obj.dir/Kernel/LPO.cpp.o CMakeFiles/obj.dir/Kernel/Polynomial.cpp.o CMakeFiles/obj.dir/Kernel/PolynomialNormalizer.cpp.o CMakeFiles/obj.dir/Kernel/ApplicativeHelper.cpp.o CMakeFiles/obj.dir/Kernel/SKIKBO.cpp.o CMakeFiles/obj.dir/Indexing/TypeSubstitutionTree.cpp.o CMakeFiles/obj.dir/Inferences/CNFOnTheFly.cpp.o CMakeFiles/obj.dir/Inferences/CombinatorDemodISE.cpp.o CMakeFiles/obj.dir/Inferences/CombinatorNormalisationISE.cpp.o CMakeFiles/obj.dir/Inferences/ArgCong.cpp.o CMakeFiles/obj.dir/Inferences/NegativeExt.cpp.o CMakeFiles/obj.dir/Inferences/Narrow.cpp.o CMakeFiles/obj.dir/Inferences/SubVarSup.cpp.o CMakeFiles/obj.dir/Inferences/BoolEqToDiseq.cpp.o CMakeFiles/obj.dir/Inferences/PrimitiveInstantiation.cpp.o CMakeFiles/obj.dir/Inferences/ElimLeibniz.cpp.o CMakeFiles/obj.dir/Inferences/Choice.cpp.o CMakeFiles/obj.dir/Inferences/Injectivity.cpp.o CMakeFiles/obj.dir/Inferences/BoolSimp.cpp.o CMakeFiles/obj.dir/Inferences/CasesSimp.cpp.o CMakeFiles/obj.dir/Inferences/Cases.cpp.o CMakeFiles/obj.dir/Shell/LambdaElimination.cpp.o CMakeFiles/obj.dir/Indexing/AcyclicityIndex.cpp.o CMakeFiles/obj.dir/Indexing/ClauseCodeTree.cpp.o CMakeFiles/obj.dir/Indexing/ClauseVariantIndex.cpp.o CMakeFiles/obj.dir/Indexing/CodeTree.cpp.o CMakeFiles/obj.dir/Indexing/CodeTreeInterfaces.cpp.o CMakeFiles/obj.dir/Indexing/GroundingIndex.cpp.o CMakeFiles/obj.dir/Indexing/Index.cpp.o CMakeFiles/obj.dir/Indexing/IndexManager.cpp.o CMakeFiles/obj.dir/Indexing/LiteralIndex.cpp.o CMakeFiles/obj.dir/Indexing/LiteralMiniIndex.cpp.o CMakeFiles/obj.dir/Indexing/LiteralSubstitutionTree.cpp.o CMakeFiles/obj.dir/Indexing/ResultSubstitution.cpp.o CMakeFiles/obj.dir/Indexing/SubstitutionTree.cpp.o CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastGen.cpp.o CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastInst.cpp.o CMakeFiles/obj.dir/Indexing/SubstitutionTree_Nodes.cpp.o CMakeFiles/obj.dir/Indexing/TermCodeTree.cpp.o CMakeFiles/obj.dir/Indexing/TermIndex.cpp.o CMakeFiles/obj.dir/Indexing/TermSharing.cpp.o CMakeFiles/obj.dir/Indexing/TermSubstitutionTree.cpp.o CMakeFiles/obj.dir/Inferences/BackwardDemodulation.cpp.o CMakeFiles/obj.dir/Inferences/BackwardSubsumptionDemodulation.cpp.o CMakeFiles/obj.dir/Inferences/BackwardSubsumptionResolution.cpp.o CMakeFiles/obj.dir/Inferences/BinaryResolution.cpp.o CMakeFiles/obj.dir/Inferences/Condensation.cpp.o CMakeFiles/obj.dir/Inferences/DistinctEqualitySimplifier.cpp.o CMakeFiles/obj.dir/Inferences/EqualityFactoring.cpp.o CMakeFiles/obj.dir/Inferences/EqualityResolution.cpp.o CMakeFiles/obj.dir/Inferences/ExtensionalityResolution.cpp.o CMakeFiles/obj.dir/Inferences/Factoring.cpp.o CMakeFiles/obj.dir/Inferences/FastCondensation.cpp.o CMakeFiles/obj.dir/Inferences/FOOLParamodulation.cpp.o CMakeFiles/obj.dir/Inferences/ForwardDemodulation.cpp.o CMakeFiles/obj.dir/Inferences/ForwardLiteralRewriting.cpp.o CMakeFiles/obj.dir/Inferences/ForwardSubsumptionAndResolution.cpp.o CMakeFiles/obj.dir/Inferences/ForwardSubsumptionDemodulation.cpp.o CMakeFiles/obj.dir/Inferences/GlobalSubsumption.cpp.o CMakeFiles/obj.dir/Inferences/HyperSuperposition.cpp.o CMakeFiles/obj.dir/Inferences/InnerRewriting.cpp.o CMakeFiles/obj.dir/Inferences/EquationalTautologyRemoval.cpp.o CMakeFiles/obj.dir/Inferences/Induction.cpp.o CMakeFiles/obj.dir/Inferences/InductionHelper.cpp.o CMakeFiles/obj.dir/Inferences/InferenceEngine.cpp.o CMakeFiles/obj.dir/Inferences/Instantiation.cpp.o CMakeFiles/obj.dir/Inferences/InterpretedEvaluation.cpp.o CMakeFiles/obj.dir/Inferences/PushUnaryMinus.cpp.o CMakeFiles/obj.dir/Inferences/Cancellation.cpp.o CMakeFiles/obj.dir/Inferences/ArithmeticSubtermGeneralization.cpp.o CMakeFiles/obj.dir/Kernel/NumTraits.cpp.o CMakeFiles/obj.dir/Inferences/GaussianVariableElimination.cpp.o CMakeFiles/obj.dir/Kernel/Rebalancing/Inverters.cpp.o CMakeFiles/obj.dir/Inferences/SLQueryBackwardSubsumption.cpp.o CMakeFiles/obj.dir/Inferences/Superposition.cpp.o CMakeFiles/obj.dir/Inferences/TautologyDeletionISE.cpp.o CMakeFiles/obj.dir/Inferences/TermAlgebraReasoning.cpp.o CMakeFiles/obj.dir/Inferences/URResolution.cpp.o CMakeFiles/obj.dir/Inferences/SubsumptionDemodulationHelper.cpp.o CMakeFiles/obj.dir/Inferences/TheoryInstAndSimp.cpp.o CMakeFiles/obj.dir/Inferences/PolynomialEvaluation.cpp.o CMakeFiles/obj.dir/InstGen/IGAlgorithm.cpp.o CMakeFiles/obj.dir/InstGen/ModelPrinter.cpp.o CMakeFiles/obj.dir/SAT/BufferedSolver.cpp.o CMakeFiles/obj.dir/SAT/DIMACS.cpp.o CMakeFiles/obj.dir/SAT/FallbackSolverWrapper.cpp.o CMakeFiles/obj.dir/SAT/MinimizingSolver.cpp.o CMakeFiles/obj.dir/SAT/Preprocess.cpp.o CMakeFiles/obj.dir/SAT/SAT2FO.cpp.o CMakeFiles/obj.dir/SAT/SATClause.cpp.o CMakeFiles/obj.dir/SAT/SATInference.cpp.o CMakeFiles/obj.dir/SAT/SATLiteral.cpp.o CMakeFiles/obj.dir/SAT/Z3Interfacing.cpp.o CMakeFiles/obj.dir/DP/ShortConflictMetaDP.cpp.o CMakeFiles/obj.dir/DP/SimpleCongruenceClosure.cpp.o CMakeFiles/obj.dir/Saturation/AWPassiveClauseContainer.cpp.o CMakeFiles/obj.dir/Saturation/ManCSPassiveClauseContainer.cpp.o CMakeFiles/obj.dir/Saturation/ClauseContainer.cpp.o CMakeFiles/obj.dir/Saturation/ConsequenceFinder.cpp.o CMakeFiles/obj.dir/Saturation/Discount.cpp.o CMakeFiles/obj.dir/Saturation/ExtensionalityClauseContainer.cpp.o CMakeFiles/obj.dir/Saturation/LabelFinder.cpp.o CMakeFiles/obj.dir/Saturation/LRS.cpp.o CMakeFiles/obj.dir/Saturation/Otter.cpp.o CMakeFiles/obj.dir/Saturation/ProvingHelper.cpp.o CMakeFiles/obj.dir/Saturation/SaturationAlgorithm.cpp.o CMakeFiles/obj.dir/Saturation/Splitter.cpp.o CMakeFiles/obj.dir/Saturation/SymElOutput.cpp.o CMakeFiles/obj.dir/Saturation/PredicateSplitPassiveClauseContainer.cpp.o CMakeFiles/obj.dir/Shell/AnswerExtractor.cpp.o CMakeFiles/obj.dir/Shell/CommandLine.cpp.o CMakeFiles/obj.dir/Shell/CNF.cpp.o CMakeFiles/obj.dir/Shell/NewCNF.cpp.o CMakeFiles/obj.dir/Shell/DistinctProcessor.cpp.o CMakeFiles/obj.dir/Shell/DistinctGroupExpansion.cpp.o CMakeFiles/obj.dir/Shell/EqResWithDeletion.cpp.o CMakeFiles/obj.dir/Shell/EqualityProxy.cpp.o CMakeFiles/obj.dir/Shell/EqualityProxyMono.cpp.o CMakeFiles/obj.dir/Shell/Flattening.cpp.o CMakeFiles/obj.dir/Shell/FunctionDefinition.cpp.o CMakeFiles/obj.dir/Shell/GeneralSplitting.cpp.o CMakeFiles/obj.dir/Shell/GoalGuessing.cpp.o CMakeFiles/obj.dir/Shell/Grounding.cpp.o CMakeFiles/obj.dir/Shell/InequalitySplitting.cpp.o CMakeFiles/obj.dir/Shell/InterpolantMinimizer.cpp.o CMakeFiles/obj.dir/Shell/InterpolantMinimizerNew.cpp.o CMakeFiles/obj.dir/Shell/Interpolants.cpp.o CMakeFiles/obj.dir/Shell/InterpolantsNew.cpp.o CMakeFiles/obj.dir/Shell/InterpretedNormalizer.cpp.o CMakeFiles/obj.dir/Shell/LaTeX.cpp.o CMakeFiles/obj.dir/Shell/Lexer.cpp.o CMakeFiles/obj.dir/Shell/LispLexer.cpp.o CMakeFiles/obj.dir/Shell/LispParser.cpp.o CMakeFiles/obj.dir/Shell/Naming.cpp.o CMakeFiles/obj.dir/Shell/NNF.cpp.o CMakeFiles/obj.dir/Shell/Normalisation.cpp.o CMakeFiles/obj.dir/Shell/Options.cpp.o CMakeFiles/obj.dir/Shell/PredicateDefinition.cpp.o CMakeFiles/obj.dir/Shell/Preprocess.cpp.o CMakeFiles/obj.dir/Shell/Property.cpp.o CMakeFiles/obj.dir/Shell/Rectify.cpp.o CMakeFiles/obj.dir/Shell/Skolem.cpp.o CMakeFiles/obj.dir/Shell/SimplifyFalseTrue.cpp.o CMakeFiles/obj.dir/Shell/SineUtils.cpp.o CMakeFiles/obj.dir/Shell/SMTFormula.cpp.o CMakeFiles/obj.dir/Shell/FOOLElimination.cpp.o CMakeFiles/obj.dir/Shell/Statistics.cpp.o CMakeFiles/obj.dir/Shell/SymbolDefinitionInlining.cpp.o CMakeFiles/obj.dir/Shell/SymbolOccurrenceReplacement.cpp.o CMakeFiles/obj.dir/Shell/SymCounter.cpp.o CMakeFiles/obj.dir/Shell/TermAlgebra.cpp.o CMakeFiles/obj.dir/Shell/TheoryAxioms.cpp.o CMakeFiles/obj.dir/Shell/TheoryFinder.cpp.o CMakeFiles/obj.dir/Shell/TheoryFlattening.cpp.o CMakeFiles/obj.dir/Shell/BlockedClauseElimination.cpp.o CMakeFiles/obj.dir/Shell/Token.cpp.o CMakeFiles/obj.dir/Shell/TPTPPrinter.cpp.o CMakeFiles/obj.dir/Shell/UIHelper.cpp.o CMakeFiles/obj.dir/Shell/VarManager.cpp.o CMakeFiles/obj.dir/Shell/UnificationWithAbstractionConfig.cpp.o CMakeFiles/obj.dir/Shell/SubexpressionIterator.cpp.o CMakeFiles/obj.dir/Parse/SMTLIB2.cpp.o CMakeFiles/obj.dir/Parse/TPTP.cpp.o CMakeFiles/obj.dir/FMB/ClauseFlattening.cpp.o CMakeFiles/obj.dir/FMB/FiniteModel.cpp.o CMakeFiles/obj.dir/FMB/FiniteModelBuilder.cpp.o CMakeFiles/obj.dir/FMB/FiniteModelMultiSorted.cpp.o CMakeFiles/obj.dir/FMB/FunctionRelationshipInference.cpp.o CMakeFiles/obj.dir/FMB/Monotonicity.cpp.o CMakeFiles/obj.dir/FMB/SortInference.cpp.o CMakeFiles/obj.dir/SAT/Z3MainLoop.cpp.o CMakeFiles/obj.dir/Minisat/core/Solver.cc.o CMakeFiles/obj.dir/Minisat/simp/SimpSolver.cc.o CMakeFiles/obj.dir/Minisat/utils/Options.cc.o CMakeFiles/obj.dir/Minisat/utils/System.cc.o CMakeFiles/obj.dir/SAT/MinisatInterfacing.cpp.o CMakeFiles/obj.dir/SAT/MinisatInterfacingNewSimp.cpp.o CMakeFiles/obj.dir/CASC/PortfolioMode.cpp.o CMakeFiles/obj.dir/CASC/Schedules.cpp.o CMakeFiles/obj.dir/CASC/ScheduleExecutor.cpp.o CMakeFiles/obj.dir/CASC/CLTBMode.cpp.o CMakeFiles/obj.dir/CASC/CLTBModeLearning.cpp.o CMakeFiles/obj.dir/version.cpp.o CMakeFiles/vampire.dir/vampire.cpp.o -o bin/vampire_z3_rel /usr/lib64/libz3.so.4.10.1.0 && : FAILED: bin/vampire_z3_rel : && /usr/bin/x86_64-pc-linux-gnu-g++ -pipe -march=native -fno-diagnostics-color -O2 -Wl,-O1 -Wl,--as-needed -Wl,--defsym=__gentoo_check_ldflags__=0 CMakeFiles/obj.dir/Debug/Assertion.cpp.o CMakeFiles/obj.dir/Debug/RuntimeStatistics.cpp.o CMakeFiles/obj.dir/Debug/Tracer.cpp.o CMakeFiles/obj.dir/Lib/Allocator.cpp.o CMakeFiles/obj.dir/Lib/DHMap.cpp.o CMakeFiles/obj.dir/Lib/Environment.cpp.o CMakeFiles/obj.dir/Lib/Event.cpp.o CMakeFiles/obj.dir/Lib/Exception.cpp.o CMakeFiles/obj.dir/Lib/Hash.cpp.o CMakeFiles/obj.dir/Lib/Int.cpp.o CMakeFiles/obj.dir/Lib/IntNameTable.cpp.o CMakeFiles/obj.dir/Lib/IntUnionFind.cpp.o CMakeFiles/obj.dir/Lib/MemoryLeak.cpp.o CMakeFiles/obj.dir/Lib/MultiCounter.cpp.o CMakeFiles/obj.dir/Lib/NameArray.cpp.o CMakeFiles/obj.dir/Lib/Random.cpp.o CMakeFiles/obj.dir/Lib/StringUtils.cpp.o CMakeFiles/obj.dir/Lib/System.cpp.o CMakeFiles/obj.dir/Lib/TimeCounter.cpp.o CMakeFiles/obj.dir/Lib/Timer.cpp.o CMakeFiles/obj.dir/Lib/Sys/Multiprocessing.cpp.o CMakeFiles/obj.dir/Lib/Sys/Semaphore.cpp.o CMakeFiles/obj.dir/Lib/Sys/SyncPipe.cpp.o CMakeFiles/obj.dir/Kernel/Clause.cpp.o CMakeFiles/obj.dir/Kernel/ClauseQueue.cpp.o CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o CMakeFiles/obj.dir/Kernel/ELiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/EqHelper.cpp.o CMakeFiles/obj.dir/Kernel/FlatTerm.cpp.o CMakeFiles/obj.dir/Kernel/Formula.cpp.o CMakeFiles/obj.dir/Kernel/FormulaTransformer.cpp.o CMakeFiles/obj.dir/Kernel/FormulaUnit.cpp.o CMakeFiles/obj.dir/Kernel/FormulaVarIterator.cpp.o CMakeFiles/obj.dir/Kernel/Grounder.cpp.o CMakeFiles/obj.dir/Kernel/Inference.cpp.o CMakeFiles/obj.dir/Kernel/InferenceStore.cpp.o CMakeFiles/obj.dir/Kernel/InterpretedLiteralEvaluator.cpp.o CMakeFiles/obj.dir/Kernel/Rebalancing.cpp.o CMakeFiles/obj.dir/Kernel/KBO.cpp.o CMakeFiles/obj.dir/Kernel/KBOForEPR.cpp.o CMakeFiles/obj.dir/Kernel/LiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/LookaheadLiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/MainLoop.cpp.o CMakeFiles/obj.dir/Kernel/Matcher.cpp.o CMakeFiles/obj.dir/Kernel/MaximalLiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o CMakeFiles/obj.dir/Kernel/MLMatcherSD.cpp.o CMakeFiles/obj.dir/Kernel/MLVariant.cpp.o CMakeFiles/obj.dir/Kernel/Ordering.cpp.o CMakeFiles/obj.dir/Kernel/Ordering_Equality.cpp.o CMakeFiles/obj.dir/Kernel/Problem.cpp.o CMakeFiles/obj.dir/Kernel/Renaming.cpp.o CMakeFiles/obj.dir/Kernel/RobSubstitution.cpp.o CMakeFiles/obj.dir/Kernel/MismatchHandler.cpp.o CMakeFiles/obj.dir/Kernel/Signature.cpp.o CMakeFiles/obj.dir/Kernel/SortHelper.cpp.o CMakeFiles/obj.dir/Kernel/OperatorType.cpp.o CMakeFiles/obj.dir/Kernel/SpassLiteralSelector.cpp.o CMakeFiles/obj.dir/Kernel/SubformulaIterator.cpp.o CMakeFiles/obj.dir/Kernel/Substitution.cpp.o CMakeFiles/obj.dir/Kernel/Term.cpp.o CMakeFiles/obj.dir/Kernel/TermIterators.cpp.o CMakeFiles/obj.dir/Kernel/TermTransformer.cpp.o CMakeFiles/obj.dir/Kernel/Theory.cpp.o CMakeFiles/obj.dir/Kernel/Unit.cpp.o CMakeFiles/obj.dir/Kernel/LPO.cpp.o CMakeFiles/obj.dir/Kernel/Polynomial.cpp.o CMakeFiles/obj.dir/Kernel/PolynomialNormalizer.cpp.o CMakeFiles/obj.dir/Kernel/ApplicativeHelper.cpp.o CMakeFiles/obj.dir/Kernel/SKIKBO.cpp.o CMakeFiles/obj.dir/Indexing/TypeSubstitutionTree.cpp.o CMakeFiles/obj.dir/Inferences/CNFOnTheFly.cpp.o CMakeFiles/obj.dir/Inferences/CombinatorDemodISE.cpp.o CMakeFiles/obj.dir/Inferences/CombinatorNormalisationISE.cpp.o CMakeFiles/obj.dir/Inferences/ArgCong.cpp.o CMakeFiles/obj.dir/Inferences/NegativeExt.cpp.o CMakeFiles/obj.dir/Inferences/Narrow.cpp.o CMakeFiles/obj.dir/Inferences/SubVarSup.cpp.o CMakeFiles/obj.dir/Inferences/BoolEqToDiseq.cpp.o CMakeFiles/obj.dir/Inferences/PrimitiveInstantiation.cpp.o CMakeFiles/obj.dir/Inferences/ElimLeibniz.cpp.o CMakeFiles/obj.dir/Inferences/Choice.cpp.o CMakeFiles/obj.dir/Inferences/Injectivity.cpp.o CMakeFiles/obj.dir/Inferences/BoolSimp.cpp.o CMakeFiles/obj.dir/Inferences/CasesSimp.cpp.o CMakeFiles/obj.dir/Inferences/Cases.cpp.o CMakeFiles/obj.dir/Shell/LambdaElimination.cpp.o CMakeFiles/obj.dir/Indexing/AcyclicityIndex.cpp.o CMakeFiles/obj.dir/Indexing/ClauseCodeTree.cpp.o CMakeFiles/obj.dir/Indexing/ClauseVariantIndex.cpp.o CMakeFiles/obj.dir/Indexing/CodeTree.cpp.o CMakeFiles/obj.dir/Indexing/CodeTreeInterfaces.cpp.o CMakeFiles/obj.dir/Indexing/GroundingIndex.cpp.o CMakeFiles/obj.dir/Indexing/Index.cpp.o CMakeFiles/obj.dir/Indexing/IndexManager.cpp.o CMakeFiles/obj.dir/Indexing/LiteralIndex.cpp.o CMakeFiles/obj.dir/Indexing/LiteralMiniIndex.cpp.o CMakeFiles/obj.dir/Indexing/LiteralSubstitutionTree.cpp.o CMakeFiles/obj.dir/Indexing/ResultSubstitution.cpp.o CMakeFiles/obj.dir/Indexing/SubstitutionTree.cpp.o CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastGen.cpp.o CMakeFiles/obj.dir/Indexing/SubstitutionTree_FastInst.cpp.o CMakeFiles/obj.dir/Indexing/SubstitutionTree_Nodes.cpp.o CMakeFiles/obj.dir/Indexing/TermCodeTree.cpp.o CMakeFiles/obj.dir/Indexing/TermIndex.cpp.o CMakeFiles/obj.dir/Indexing/TermSharing.cpp.o CMakeFiles/obj.dir/Indexing/TermSubstitutionTree.cpp.o CMakeFiles/obj.dir/Inferences/BackwardDemodulation.cpp.o CMakeFiles/obj.dir/Inferences/BackwardSubsumptionDemodulation.cpp.o CMakeFiles/obj.dir/Inferences/BackwardSubsumptionResolution.cpp.o CMakeFiles/obj.dir/Inferences/BinaryResolution.cpp.o CMakeFiles/obj.dir/Inferences/Condensation.cpp.o CMakeFiles/obj.dir/Inferences/DistinctEqualitySimplifier.cpp.o CMakeFiles/obj.dir/Inferences/EqualityFactoring.cpp.o CMakeFiles/obj.dir/Inferences/EqualityResolution.cpp.o CMakeFiles/obj.dir/Inferences/ExtensionalityResolution.cpp.o CMakeFiles/obj.dir/Inferences/Factoring.cpp.o CMakeFiles/obj.dir/Inferences/FastCondensation.cpp.o CMakeFiles/obj.dir/Inferences/FOOLParamodulation.cpp.o CMakeFiles/obj.dir/Inferences/ForwardDemodulation.cpp.o CMakeFiles/obj.dir/Inferences/ForwardLiteralRewriting.cpp.o CMakeFiles/obj.dir/Inferences/ForwardSubsumptionAndResolution.cpp.o CMakeFiles/obj.dir/Inferences/ForwardSubsumptionDemodulation.cpp.o CMakeFiles/obj.dir/Inferences/GlobalSubsumption.cpp.o CMakeFiles/obj.dir/Inferences/HyperSuperposition.cpp.o CMakeFiles/obj.dir/Inferences/InnerRewriting.cpp.o CMakeFiles/obj.dir/Inferences/EquationalTautologyRemoval.cpp.o CMakeFiles/obj.dir/Inferences/Induction.cpp.o CMakeFiles/obj.dir/Inferences/InductionHelper.cpp.o CMakeFiles/obj.dir/Inferences/InferenceEngine.cpp.o CMakeFiles/obj.dir/Inferences/Instantiation.cpp.o CMakeFiles/obj.dir/Inferences/InterpretedEvaluation.cpp.o CMakeFiles/obj.dir/Inferences/PushUnaryMinus.cpp.o CMakeFiles/obj.dir/Inferences/Cancellation.cpp.o CMakeFiles/obj.dir/Inferences/ArithmeticSubtermGeneralization.cpp.o CMakeFiles/obj.dir/Kernel/NumTraits.cpp.o CMakeFiles/obj.dir/Inferences/GaussianVariableElimination.cpp.o CMakeFiles/obj.dir/Kernel/Rebalancing/Inverters.cpp.o CMakeFiles/obj.dir/Inferences/SLQueryBackwardSubsumption.cpp.o CMakeFiles/obj.dir/Inferences/Superposition.cpp.o CMakeFiles/obj.dir/Inferences/TautologyDeletionISE.cpp.o CMakeFiles/obj.dir/Inferences/TermAlgebraReasoning.cpp.o CMakeFiles/obj.dir/Inferences/URResolution.cpp.o CMakeFiles/obj.dir/Inferences/SubsumptionDemodulationHelper.cpp.o CMakeFiles/obj.dir/Inferences/TheoryInstAndSimp.cpp.o CMakeFiles/obj.dir/Inferences/PolynomialEvaluation.cpp.o CMakeFiles/obj.dir/InstGen/IGAlgorithm.cpp.o CMakeFiles/obj.dir/InstGen/ModelPrinter.cpp.o CMakeFiles/obj.dir/SAT/BufferedSolver.cpp.o CMakeFiles/obj.dir/SAT/DIMACS.cpp.o CMakeFiles/obj.dir/SAT/FallbackSolverWrapper.cpp.o CMakeFiles/obj.dir/SAT/MinimizingSolver.cpp.o CMakeFiles/obj.dir/SAT/Preprocess.cpp.o CMakeFiles/obj.dir/SAT/SAT2FO.cpp.o CMakeFiles/obj.dir/SAT/SATClause.cpp.o CMakeFiles/obj.dir/SAT/SATInference.cpp.o CMakeFiles/obj.dir/SAT/SATLiteral.cpp.o CMakeFiles/obj.dir/SAT/Z3Interfacing.cpp.o CMakeFiles/obj.dir/DP/ShortConflictMetaDP.cpp.o CMakeFiles/obj.dir/DP/SimpleCongruenceClosure.cpp.o CMakeFiles/obj.dir/Saturation/AWPassiveClauseContainer.cpp.o CMakeFiles/obj.dir/Saturation/ManCSPassiveClauseContainer.cpp.o CMakeFiles/obj.dir/Saturation/ClauseContainer.cpp.o CMakeFiles/obj.dir/Saturation/ConsequenceFinder.cpp.o CMakeFiles/obj.dir/Saturation/Discount.cpp.o CMakeFiles/obj.dir/Saturation/ExtensionalityClauseContainer.cpp.o CMakeFiles/obj.dir/Saturation/LabelFinder.cpp.o CMakeFiles/obj.dir/Saturation/LRS.cpp.o CMakeFiles/obj.dir/Saturation/Otter.cpp.o CMakeFiles/obj.dir/Saturation/ProvingHelper.cpp.o CMakeFiles/obj.dir/Saturation/SaturationAlgorithm.cpp.o CMakeFiles/obj.dir/Saturation/Splitter.cpp.o CMakeFiles/obj.dir/Saturation/SymElOutput.cpp.o CMakeFiles/obj.dir/Saturation/PredicateSplitPassiveClauseContainer.cpp.o CMakeFiles/obj.dir/Shell/AnswerExtractor.cpp.o CMakeFiles/obj.dir/Shell/CommandLine.cpp.o CMakeFiles/obj.dir/Shell/CNF.cpp.o CMakeFiles/obj.dir/Shell/NewCNF.cpp.o CMakeFiles/obj.dir/Shell/DistinctProcessor.cpp.o CMakeFiles/obj.dir/Shell/DistinctGroupExpansion.cpp.o CMakeFiles/obj.dir/Shell/EqResWithDeletion.cpp.o CMakeFiles/obj.dir/Shell/EqualityProxy.cpp.o CMakeFiles/obj.dir/Shell/EqualityProxyMono.cpp.o CMakeFiles/obj.dir/Shell/Flattening.cpp.o CMakeFiles/obj.dir/Shell/FunctionDefinition.cpp.o CMakeFiles/obj.dir/Shell/GeneralSplitting.cpp.o CMakeFiles/obj.dir/Shell/GoalGuessing.cpp.o CMakeFiles/obj.dir/Shell/Grounding.cpp.o CMakeFiles/obj.dir/Shell/InequalitySplitting.cpp.o CMakeFiles/obj.dir/Shell/InterpolantMinimizer.cpp.o CMakeFiles/obj.dir/Shell/InterpolantMinimizerNew.cpp.o CMakeFiles/obj.dir/Shell/Interpolants.cpp.o CMakeFiles/obj.dir/Shell/InterpolantsNew.cpp.o CMakeFiles/obj.dir/Shell/InterpretedNormalizer.cpp.o CMakeFiles/obj.dir/Shell/LaTeX.cpp.o CMakeFiles/obj.dir/Shell/Lexer.cpp.o CMakeFiles/obj.dir/Shell/LispLexer.cpp.o CMakeFiles/obj.dir/Shell/LispParser.cpp.o CMakeFiles/obj.dir/Shell/Naming.cpp.o CMakeFiles/obj.dir/Shell/NNF.cpp.o CMakeFiles/obj.dir/Shell/Normalisation.cpp.o CMakeFiles/obj.dir/Shell/Options.cpp.o CMakeFiles/obj.dir/Shell/PredicateDefinition.cpp.o CMakeFiles/obj.dir/Shell/Preprocess.cpp.o CMakeFiles/obj.dir/Shell/Property.cpp.o CMakeFiles/obj.dir/Shell/Rectify.cpp.o CMakeFiles/obj.dir/Shell/Skolem.cpp.o CMakeFiles/obj.dir/Shell/SimplifyFalseTrue.cpp.o CMakeFiles/obj.dir/Shell/SineUtils.cpp.o CMakeFiles/obj.dir/Shell/SMTFormula.cpp.o CMakeFiles/obj.dir/Shell/FOOLElimination.cpp.o CMakeFiles/obj.dir/Shell/Statistics.cpp.o CMakeFiles/obj.dir/Shell/SymbolDefinitionInlining.cpp.o CMakeFiles/obj.dir/Shell/SymbolOccurrenceReplacement.cpp.o CMakeFiles/obj.dir/Shell/SymCounter.cpp.o CMakeFiles/obj.dir/Shell/TermAlgebra.cpp.o CMakeFiles/obj.dir/Shell/TheoryAxioms.cpp.o CMakeFiles/obj.dir/Shell/TheoryFinder.cpp.o CMakeFiles/obj.dir/Shell/TheoryFlattening.cpp.o CMakeFiles/obj.dir/Shell/BlockedClauseElimination.cpp.o CMakeFiles/obj.dir/Shell/Token.cpp.o CMakeFiles/obj.dir/Shell/TPTPPrinter.cpp.o CMakeFiles/obj.dir/Shell/UIHelper.cpp.o CMakeFiles/obj.dir/Shell/VarManager.cpp.o CMakeFiles/obj.dir/Shell/UnificationWithAbstractionConfig.cpp.o CMakeFiles/obj.dir/Shell/SubexpressionIterator.cpp.o CMakeFiles/obj.dir/Parse/SMTLIB2.cpp.o CMakeFiles/obj.dir/Parse/TPTP.cpp.o CMakeFiles/obj.dir/FMB/ClauseFlattening.cpp.o CMakeFiles/obj.dir/FMB/FiniteModel.cpp.o CMakeFiles/obj.dir/FMB/FiniteModelBuilder.cpp.o CMakeFiles/obj.dir/FMB/FiniteModelMultiSorted.cpp.o CMakeFiles/obj.dir/FMB/FunctionRelationshipInference.cpp.o CMakeFiles/obj.dir/FMB/Monotonicity.cpp.o CMakeFiles/obj.dir/FMB/SortInference.cpp.o CMakeFiles/obj.dir/SAT/Z3MainLoop.cpp.o CMakeFiles/obj.dir/Minisat/core/Solver.cc.o CMakeFiles/obj.dir/Minisat/simp/SimpSolver.cc.o CMakeFiles/obj.dir/Minisat/utils/Options.cc.o CMakeFiles/obj.dir/Minisat/utils/System.cc.o CMakeFiles/obj.dir/SAT/MinisatInterfacing.cpp.o CMakeFiles/obj.dir/SAT/MinisatInterfacingNewSimp.cpp.o CMakeFiles/obj.dir/CASC/PortfolioMode.cpp.o CMakeFiles/obj.dir/CASC/Schedules.cpp.o CMakeFiles/obj.dir/CASC/ScheduleExecutor.cpp.o CMakeFiles/obj.dir/CASC/CLTBMode.cpp.o CMakeFiles/obj.dir/CASC/CLTBModeLearning.cpp.o CMakeFiles/obj.dir/version.cpp.o CMakeFiles/vampire.dir/vampire.cpp.o -o bin/vampire_z3_rel /usr/lib64/libz3.so.4.10.1.0 && : /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Kernel/LookaheadLiteralSelector.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': LookaheadLiteralSelector.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Kernel/LookaheadLiteralSelector.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': LookaheadLiteralSelector.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Kernel/MainLoop.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': MainLoop.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Kernel/MainLoop.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': MainLoop.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/CNFOnTheFly.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': CNFOnTheFly.cpp:(.text+0x640): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/CNFOnTheFly.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': CNFOnTheFly.cpp:(.text+0x640): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ArgCong.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ArgCong.cpp:(.text+0x190): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ArgCong.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ArgCong.cpp:(.text+0x190): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/NegativeExt.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': NegativeExt.cpp:(.text+0x130): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/NegativeExt.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': NegativeExt.cpp:(.text+0x130): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Narrow.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Narrow.cpp:(.text+0xd0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Narrow.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Narrow.cpp:(.text+0xd0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/SubVarSup.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': SubVarSup.cpp:(.text+0x3f0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/SubVarSup.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': SubVarSup.cpp:(.text+0x3f0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/PrimitiveInstantiation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': PrimitiveInstantiation.cpp:(.text+0x50): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/PrimitiveInstantiation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': PrimitiveInstantiation.cpp:(.text+0x50): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ElimLeibniz.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ElimLeibniz.cpp:(.text+0xb0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ElimLeibniz.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ElimLeibniz.cpp:(.text+0xb0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Choice.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Choice.cpp:(.text+0x260): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Choice.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Choice.cpp:(.text+0x260): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Cases.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Cases.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Cases.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Cases.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Indexing/GroundingIndex.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': GroundingIndex.cpp:(.text+0x10): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Indexing/GroundingIndex.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': GroundingIndex.cpp:(.text+0x10): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Indexing/IndexManager.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': IndexManager.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Indexing/IndexManager.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': IndexManager.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/BackwardDemodulation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': BackwardDemodulation.cpp:(.text+0x330): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/BackwardDemodulation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': BackwardDemodulation.cpp:(.text+0x330): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/BackwardSubsumptionDemodulation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': BackwardSubsumptionDemodulation.cpp:(.text+0x2d0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/BackwardSubsumptionDemodulation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': BackwardSubsumptionDemodulation.cpp:(.text+0x2d0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/BackwardSubsumptionResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': BackwardSubsumptionResolution.cpp:(.text+0x510): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/BackwardSubsumptionResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': BackwardSubsumptionResolution.cpp:(.text+0x510): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/BinaryResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': BinaryResolution.cpp:(.text+0xf0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/BinaryResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': BinaryResolution.cpp:(.text+0xf0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/EqualityFactoring.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': EqualityFactoring.cpp:(.text+0x90): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/EqualityFactoring.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': EqualityFactoring.cpp:(.text+0x90): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/EqualityResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': EqualityResolution.cpp:(.text+0x1a0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/EqualityResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': EqualityResolution.cpp:(.text+0x1a0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ExtensionalityResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ExtensionalityResolution.cpp:(.text+0x90): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ExtensionalityResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ExtensionalityResolution.cpp:(.text+0x90): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Factoring.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Factoring.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Factoring.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Factoring.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ForwardDemodulation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ForwardDemodulation.cpp:(.text+0x2b0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ForwardDemodulation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ForwardDemodulation.cpp:(.text+0x2b0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ForwardLiteralRewriting.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ForwardLiteralRewriting.cpp:(.text+0x50): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ForwardLiteralRewriting.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ForwardLiteralRewriting.cpp:(.text+0x50): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ForwardSubsumptionAndResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ForwardSubsumptionAndResolution.cpp:(.text+0x80): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ForwardSubsumptionAndResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ForwardSubsumptionAndResolution.cpp:(.text+0x80): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ForwardSubsumptionDemodulation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ForwardSubsumptionDemodulation.cpp:(.text+0x330): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/ForwardSubsumptionDemodulation.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ForwardSubsumptionDemodulation.cpp:(.text+0x330): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/GlobalSubsumption.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': GlobalSubsumption.cpp:(.text+0x580): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/GlobalSubsumption.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': GlobalSubsumption.cpp:(.text+0x580): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/HyperSuperposition.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': HyperSuperposition.cpp:(.text+0x80): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/HyperSuperposition.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': HyperSuperposition.cpp:(.text+0x80): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/InnerRewriting.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': InnerRewriting.cpp:(.text+0x2a0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/InnerRewriting.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': InnerRewriting.cpp:(.text+0x2a0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Induction.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Induction.cpp:(.text+0xcf0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Induction.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Induction.cpp:(.text+0xcf0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/InferenceEngine.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': InferenceEngine.cpp:(.text+0x2c30): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/InferenceEngine.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': InferenceEngine.cpp:(.text+0x2c30): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/SLQueryBackwardSubsumption.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': SLQueryBackwardSubsumption.cpp:(.text+0x510): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/SLQueryBackwardSubsumption.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': SLQueryBackwardSubsumption.cpp:(.text+0x510): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Superposition.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Superposition.cpp:(.text+0x240): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/Superposition.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Superposition.cpp:(.text+0x240): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/TermAlgebraReasoning.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': TermAlgebraReasoning.cpp:(.text+0xe0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/TermAlgebraReasoning.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': TermAlgebraReasoning.cpp:(.text+0xe0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/URResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': URResolution.cpp:(.text+0xa0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/URResolution.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': URResolution.cpp:(.text+0xa0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/TheoryInstAndSimp.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': TheoryInstAndSimp.cpp:(.text+0x720): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Inferences/TheoryInstAndSimp.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': TheoryInstAndSimp.cpp:(.text+0x720): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/InstGen/IGAlgorithm.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': IGAlgorithm.cpp:(.text+0x490): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/InstGen/IGAlgorithm.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': IGAlgorithm.cpp:(.text+0x490): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/SAT/Z3Interfacing.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Z3Interfacing.cpp:(.text+0x550): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/SAT/Z3Interfacing.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Z3Interfacing.cpp:(.text+0x550): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/AWPassiveClauseContainer.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': AWPassiveClauseContainer.cpp:(.text+0x1130): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/AWPassiveClauseContainer.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': AWPassiveClauseContainer.cpp:(.text+0x1130): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/ClauseContainer.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ClauseContainer.cpp:(.text+0xeb0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/ClauseContainer.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ClauseContainer.cpp:(.text+0xeb0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/ConsequenceFinder.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ConsequenceFinder.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/ConsequenceFinder.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ConsequenceFinder.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/Discount.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Discount.cpp:(.text+0x60): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/Discount.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Discount.cpp:(.text+0x60): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/LabelFinder.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': LabelFinder.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/LabelFinder.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': LabelFinder.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/LRS.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': LRS.cpp:(.text+0x20): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/LRS.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': LRS.cpp:(.text+0x20): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/Otter.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Otter.cpp:(.text+0x90): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/Otter.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Otter.cpp:(.text+0x90): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/ProvingHelper.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ProvingHelper.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/ProvingHelper.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': ProvingHelper.cpp:(.text+0x0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/SaturationAlgorithm.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': SaturationAlgorithm.cpp:(.text+0x4a0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/SaturationAlgorithm.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': SaturationAlgorithm.cpp:(.text+0x4a0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/Splitter.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Splitter.cpp:(.text+0x8d0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Saturation/Splitter.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Splitter.cpp:(.text+0x8d0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Shell/CommandLine.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': CommandLine.cpp:(.text+0xb0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Shell/CommandLine.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': CommandLine.cpp:(.text+0xb0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Shell/InterpolantMinimizerNew.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': InterpolantMinimizerNew.cpp:(.text+0xd0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Shell/InterpolantMinimizerNew.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': InterpolantMinimizerNew.cpp:(.text+0xd0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Shell/Statistics.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Statistics.cpp:(.text+0x70): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/Shell/Statistics.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Statistics.cpp:(.text+0x70): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/FMB/FiniteModelBuilder.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': FiniteModelBuilder.cpp:(.text+0x17b0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/FMB/FiniteModelBuilder.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': FiniteModelBuilder.cpp:(.text+0x17b0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/FMB/FunctionRelationshipInference.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': FunctionRelationshipInference.cpp:(.text+0x880): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/FMB/FunctionRelationshipInference.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': FunctionRelationshipInference.cpp:(.text+0x880): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/SAT/Z3MainLoop.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Z3MainLoop.cpp:(.text+0xc0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/SAT/Z3MainLoop.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': Z3MainLoop.cpp:(.text+0xc0): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/vampire.dir/vampire.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': vampire.cpp:(.text+0x120): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/vampire.dir/vampire.cpp.o: in function `z3::constructor_list::constructor_list(z3::constructors const&)': vampire.cpp:(.text+0x120): multiple definition of `z3::constructor_list::constructor_list(z3::constructors const&)'; CMakeFiles/obj.dir/Kernel/ColorHelper.cpp.o:ColorHelper.cpp:(.text+0x280): first defined here /usr/lib/gcc/x86_64-pc-linux-gnu/12.1.1/../../../../x86_64-pc-linux-gnu/bin/ld: CMakeFiles/obj.dir/CASC/PortfolioMode.cpp.o: in function `CASC::PortfolioMode::PortfolioMode()': PortfolioMode.cpp:(.text+0x703): warning: the use of `tmpnam' is dangerous, better use `mkstemp' collect2: error: ld returned 1 exit status ninja: build stopped: subcommand failed. * ERROR: sci-mathematics/vampire-4.6.1::gentoo failed (compile phase): * ninja -v -j4 -l0 failed * * Call stack: * ebuild.sh, line 122: Called src_compile * environment, line 2214: Called cmake_src_compile * environment, line 985: Called cmake_build * environment, line 954: Called eninja * environment, line 1405: Called die * The specific snippet of code: * "$@" || die "${nonfatal_args[@]}" "${*} failed" * * If you need support, post the output of `emerge --info '=sci-mathematics/vampire-4.6.1::gentoo'`, * the complete build log and the output of `emerge -pqv '=sci-mathematics/vampire-4.6.1::gentoo'`. * The complete build log is located at '/var/log/portage/sci-mathematics:vampire-4.6.1:20220723-082828.log'. * For convenience, a symlink to the build log is located at '/var/tmp/portage/sci-mathematics/vampire-4.6.1/temp/build.log'. * The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/vampire-4.6.1/temp/environment'. * Working directory: '/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1_build' * S: '/var/tmp/portage/sci-mathematics/vampire-4.6.1/work/vampire-4.6.1'