Attachment 929686 Details for Bug 1133066 – log with cbmc patched to retrieve arch ppc64 little endian

log with cbmc patched to retrieve arch ppc64 little endian

cbmc-with-patch.log (text/x-log), 165.75 KB, created by Menanteau Guy on 2014-08-22 15:22:02 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Menanteau Guy

Created: 2014-08-22 15:22:02 UTC

Size: 165.75 KB

patch

obsolete

>Building target platforms: ppc64le
>Building for target ppc64le
>Executing(%prep): /bin/sh -e /home/root/rpmbuild/tmp/rpm-tmp.YXpbGd
>+ umask 022
>+ cd /home/root/rpmbuild/BUILD
>+ cd /home/root/rpmbuild/BUILD
>+ rm -rf cbmc-4.7
>+ /usr/bin/tar -xf -
>+ /usr/bin/xz -dc /home/root/ppc64le/stage2/cbmc/cbmc-4.7.tar.xz
>+ STATUS=0
>+ '[' 0 -ne 0 ']'
>+ cd cbmc-4.7
>+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
>+ echo 'Patch #0 (cbmc-4.7-fix-build.patch):'
>Patch #0 (cbmc-4.7-fix-build.patch):
>+ /usr/bin/patch -p0 --fuzz=0
>+ /usr/bin/cat /home/root/ppc64le/stage2/cbmc/cbmc-4.7-fix-build.patch
>patching file src/cbmc/Makefile
>patching file src/common
>patching file src/config.inc
>patching file src/goto-instrument/Makefile
>patching file src/solvers/Makefile
>+ echo 'Patch #1 (cbmc-4.7-alias.patch):'
>Patch #1 (cbmc-4.7-alias.patch):
>+ /usr/bin/patch -p0 --fuzz=0
>+ /usr/bin/cat /home/root/ppc64le/stage2/cbmc/cbmc-4.7-alias.patch
>patching file src/cpp/cpp_typecheck_constructor.cpp
>patching file src/util/expr.h
>+ echo 'Patch #2 (cbmc-4.7-cudd.patch):'
>Patch #2 (cbmc-4.7-cudd.patch):
>+ /usr/bin/patch -p0 --fuzz=0
>+ /usr/bin/cat /home/root/ppc64le/stage2/cbmc/cbmc-4.7-cudd.patch
>patching file src/solvers/qbf/qbf_bdd_core.cpp
>patching file src/solvers/qbf/qbf_skizzo_core.cpp
>+ echo 'Patch #3 (guy.patch):'
>Patch #3 (guy.patch):
>+ /usr/bin/patch -p0 --fuzz=0
>+ /usr/bin/cat /home/root/ppc64le/stage2/cbmc/guy.patch
>patching file src/util/config.cpp
>+ sed -e 's|@RPM_OPT_FLAGS@|-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64|' -e 's|@RPM_LD_FLAGS@|-Wl,--as-needed -Wl,-z,relro |' -i src/config.inc
>+ exit 0
>Executing(%build): /bin/sh -e /home/root/rpmbuild/tmp/rpm-tmp.UzcQBW
>+ umask 022
>+ cd /home/root/rpmbuild/BUILD
>+ cd cbmc-4.7
>+ make -j2 -C src
>make: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src'
>## Entering big-int
>make  -C big-int
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/big-int'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64  -o bigint-func.o bigint-func.cc
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64  -o bigint.o bigint.cc
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64  -o bigint-test.o bigint-test.cc
>ld -r -o big-int.a bigint-func.o bigint.o
>g++  -o test-bigint bigint-func.o bigint.o bigint-test.o -Wl,--as-needed -Wl,-z,relro  
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/big-int'
>## Entering util
>make  -C util
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/util'
>g++ -o irep_ids_convert irep_ids_convert.cpp
>./irep_ids_convert header < irep_ids.txt > irep_ids.h
>./irep_ids_convert table < irep_ids.txt > irep_ids.inc
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o arith_tools.o arith_tools.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o base_type.o base_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cmdline.o cmdline.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o config.o config.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symbol_table.o symbol_table.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o expr.o expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o expr_util.o expr_util.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o i2string.o i2string.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o irep.o irep.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o language.o language.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o lispexpr.o lispexpr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o lispirep.o lispirep.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o location.o location.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o message.o message.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o language_file.o language_file.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o mp_arith.o mp_arith.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o namespace.o namespace.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o parseoptions.o parseoptions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o rename.o rename.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o replace_expr.o replace_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o threeval.o threeval.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o typecheck.o typecheck.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o graph.o graph.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o type.o type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cnf_simplify.o cnf_simplify.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o pointer_predicates.o pointer_predicates.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o merge_irep.o merge_irep.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o bitvector.o bitvector.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o parser.o parser.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o map_util.o map_util.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o replace_symbol.o replace_symbol.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o actuals.o actuals.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o get_module.o get_module.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o string_hash.o string_hash.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o string_container.o string_container.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o identifier.o identifier.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o rational.o rational.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o options.o options.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_misc.o c_misc.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o simplify_expr.o simplify_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o dstring.o dstring.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o find_symbols.o find_symbols.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o rational_tools.o rational_tools.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ui_message.o ui_message.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o simplify_utils.o simplify_utils.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o time_stopping.o time_stopping.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symbol.o symbol.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o irep_hash_container.o irep_hash_container.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cout_message.o cout_message.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o type_eq.o type_eq.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o guard.o guard.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o array_name.o array_name.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o message_stream.o message_stream.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o substitute.o substitute.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o decision_procedure.o decision_procedure.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o union_find.o union_find.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o xml.o xml.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o xml_irep.o xml_irep.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o xml_expr.o xml_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o std_types.o std_types.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o std_code.o std_code.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o format_constant.o format_constant.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o find_macros.o find_macros.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ref_expr_set.o ref_expr_set.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o std_expr.o std_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o irep_serialization.o irep_serialization.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symbol_serialization.o symbol_serialization.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o fixedbv.o fixedbv.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ieee_float.o ieee_float.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o signal_catcher.o signal_catcher.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o pointer_offset_size.o pointer_offset_size.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o bv_arithmetic.o bv_arithmetic.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o tempdir.o tempdir.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o tempfile.o tempfile.cpp
>tempdir.cpp: In constructor 'temp_working_dirt::temp_working_dirt(const string&)':
>tempdir.cpp:166:22: warning: ignoring return value of 'int chdir(const char*)', declared with attribute warn_unused_result [-Wunused-result]
>   chdir(path.c_str());
>                      ^
>tempdir.cpp: In destructor 'temp_working_dirt::~temp_working_dirt()':
>tempdir.cpp:183:39: warning: ignoring return value of 'int chdir(const char*)', declared with attribute warn_unused_result [-Wunused-result]
>   chdir(old_working_directory.c_str());
>                                       ^
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o timer.o timer.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o unicode.o unicode.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o irep_ids.o irep_ids.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o byte_operators.o byte_operators.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o string2int.o string2int.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o file_util.o file_util.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o memory_info.o memory_info.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o pipe_stream.o pipe_stream.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ieee_float_test.o ieee_float_test.cpp
>ld -r -o util.a arith_tools.o base_type.o cmdline.o config.o symbol_table.o expr.o expr_util.o i2string.o irep.o language.o lispexpr.o lispirep.o location.o message.o language_file.o mp_arith.o namespace.o parseoptions.o rename.o replace_expr.o threeval.o typecheck.o graph.o type.o cnf_simplify.o pointer_predicates.o merge_irep.o bitvector.o parser.o map_util.o replace_symbol.o actuals.o get_module.o string_hash.o string_container.o identifier.o rational.o options.o c_misc.o simplify_expr.o dstring.o find_symbols.o rational_tools.o ui_message.o simplify_utils.o time_stopping.o symbol.o irep_hash_container.o cout_message.o type_eq.o guard.o array_name.o message_stream.o substitute.o decision_procedure.o union_find.o xml.o xml_irep.o xml_expr.o std_types.o std_code.o format_constant.o find_macros.o ref_expr_set.o std_expr.o irep_serialization.o symbol_serialization.o fixedbv.o ieee_float.o signal_catcher.o pointer_offset_size.o bv_arithmetic.o tempdir.o tempfile.o timer.o unicode.o irep_ids.o byte_operators.o string2int.o file_util.o memory_info.o pipe_stream.o
>g++  -o ieee_float_test ieee_float_test.o util.a -Wl,--as-needed -Wl,-z,relro  ../big-int/bigint.o ../big-int/bigint-func.o
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/util'
>## Entering langapi
>## Entering cpp
>make  -C langapi
>make  -C cpp
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/langapi'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o mode.o mode.cpp
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/cpp'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_id.o cpp_id.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o language_ui.o language_ui.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_language.o cpp_language.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o languages.o languages.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o expr2cpp.o expr2cpp.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o language_util.o language_util.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_parser.o cpp_parser.cpp
>ld -r -o langapi.a mode.o language_ui.o languages.o language_util.o
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/langapi'
>## Entering ansi-c
>make  -C ansi-c
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/ansi-c'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_typecast.o c_typecast.cpp
>flex -Pyycpp -ocpp_lex.yy.cpp scanner.l
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck.o cpp_typecheck.cpp
>bison -y -v $flags -pyyansi_c -d parser.y -o ansi_c_y.tab.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_convert_type.o cpp_convert_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_expr.o cpp_typecheck_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_code.o cpp_typecheck_code.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_type.o cpp_typecheck_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o parse.o parse.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_parse_tree.o cpp_parse_tree.cpp
>flex -Pyyansi_c -oansi_c_lex.yy.cpp scanner.l
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_token_buffer.o cpp_token_buffer.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_parser.o ansi_c_parser.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_fargs.o cpp_typecheck_fargs.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o expr2c.o expr2c.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_resolve.o cpp_typecheck_resolve.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_language.o ansi_c_language.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_util.o cpp_util.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_sizeof.o c_sizeof.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_enum_type.o cpp_enum_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_types.o c_types.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_function.o cpp_typecheck_function.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o trans_unit.o trans_unit.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_namespace.o cpp_typecheck_namespace.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_typecheck.o ansi_c_typecheck.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_name.o cpp_name.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_preprocess.o c_preprocess.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_is_pod.o cpp_is_pod.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_typecheck_base.o c_typecheck_base.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_scope.o cpp_scope.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_typecheck_initializer.o c_typecheck_initializer.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_find_constructor.o cpp_typecheck_find_constructor.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_typecheck_typecast.o c_typecheck_typecast.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o template_map.o template_map.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_typecheck_code.o c_typecheck_code.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_scopes.o cpp_scopes.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_typecheck_expr.o c_typecheck_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_declarator.o cpp_declarator.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_typecheck_type.o c_typecheck_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_instantiate_template.o cpp_instantiate_template.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o string_constant.o string_constant.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_internal_additions.o cpp_internal_additions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_qualifiers.o c_qualifiers.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_type2name.o cpp_type2name.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o c_typecheck_argc_argv.o c_typecheck_argc_argv.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_linkage_spec.o cpp_typecheck_linkage_spec.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_parse_tree.o ansi_c_parse_tree.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_template.o cpp_typecheck_template.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o preprocessor_line.o preprocessor_line.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_function_bodies.o cpp_typecheck_function_bodies.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_convert.o ansi_c_convert.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_initializer.o cpp_typecheck_initializer.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_convert_type.o ansi_c_convert_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_compound_type.o cpp_typecheck_compound_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o type2name.o type2name.cpp
>g++ -o library/converter library/converter.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_constructor.o cpp_constructor.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_destructor.o cpp_destructor.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o anonymous_member.o anonymous_member.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_conversions.o cpp_typecheck_conversions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o printf_formatter.o printf_formatter.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_declaration.o cpp_typecheck_declaration.cpp
>g++ -o file_converter file_converter.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_declarator_converter.o cpp_declarator_converter.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_declaration.o cpp_declaration.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o padding.o padding.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_namespace_spec.o cpp_namespace_spec.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_declaration.o ansi_c_declaration.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_using.o cpp_typecheck_using.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o designator.o designator.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_exception_id.o cpp_exception_id.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o literals/parse_float.o literals/parse_float.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_enum_type.o cpp_typecheck_enum_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o literals/unescape_string.o literals/unescape_string.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o literals/convert_float_literal.o literals/convert_float_literal.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_bases.o cpp_typecheck_bases.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o literals/convert_character_literal.o literals/convert_character_literal.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_constructor.o cpp_typecheck_constructor.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o literals/convert_integer_literal.o literals/convert_integer_literal.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_virtual_table.o cpp_typecheck_virtual_table.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o literals/convert_string_literal.o literals/convert_string_literal.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_typecheck_static_assert.o cpp_typecheck_static_assert.cpp
>if [ -e ansi_c_y.tab.hpp ] ; then mv ansi_c_y.tab.hpp ansi_c_y.tab.h ; else \
>        mv ansi_c_y.tab.cpp.h ansi_c_y.tab.h ; fi
>cat library/*.c | library/converter > cprover_library.inc
>./file_converter < gcc_builtin_headers_generic.h > gcc_builtin_headers_generic.inc
>./file_converter < gcc_builtin_headers_ia32.h > gcc_builtin_headers_ia32.inc
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cpp_lex.yy.o cpp_lex.yy.cpp
>./file_converter < gcc_builtin_headers_alpha.h > gcc_builtin_headers_alpha.inc
>./file_converter < gcc_builtin_headers_arm.h > gcc_builtin_headers_arm.inc
>./file_converter < gcc_builtin_headers_mips.h > gcc_builtin_headers_mips.inc
>./file_converter < gcc_builtin_headers_power.h > gcc_builtin_headers_power.inc
>./file_converter < arm_builtin_headers.h > arm_builtin_headers.inc
>./file_converter < cw_builtin_headers.h > cw_builtin_headers.inc
>./file_converter < clang_builtin_headers.h > clang_builtin_headers.inc
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_y.tab.o ansi_c_y.tab.cpp
>ld -r -o cpp.a cpp_id.o cpp_language.o expr2cpp.o cpp_parser.o cpp_lex.yy.o cpp_typecheck.o cpp_convert_type.o cpp_typecheck_expr.o cpp_typecheck_code.o cpp_typecheck_type.o parse.o cpp_parse_tree.o cpp_token_buffer.o cpp_typecheck_fargs.o cpp_typecheck_resolve.o cpp_util.o cpp_enum_type.o cpp_typecheck_function.o cpp_typecheck_namespace.o cpp_name.o cpp_is_pod.o cpp_scope.o cpp_typecheck_find_constructor.o template_map.o cpp_scopes.o cpp_declarator.o cpp_instantiate_template.o cpp_internal_additions.o cpp_type2name.o cpp_typecheck_linkage_spec.o cpp_typecheck_template.o cpp_typecheck_function_bodies.o cpp_typecheck_initializer.o cpp_typecheck_compound_type.o cpp_constructor.o cpp_destructor.o cpp_typecheck_conversions.o cpp_typecheck_declaration.o cpp_declarator_converter.o cpp_declaration.o cpp_namespace_spec.o cpp_typecheck_using.o cpp_exception_id.o cpp_typecheck_enum_type.o cpp_typecheck_bases.o cpp_typecheck_constructor.o cpp_typecheck_virtual_table.o cpp_typecheck_static_assert.o
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_lex.yy.o ansi_c_lex.yy.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o cprover_library.o cprover_library.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ansi_c_internal_additions.o ansi_c_internal_additions.cpp
>ld -r -o ansi-c.a c_typecast.o ansi_c_y.tab.o ansi_c_lex.yy.o ansi_c_parser.o expr2c.o ansi_c_language.o c_sizeof.o c_types.o trans_unit.o ansi_c_typecheck.o c_preprocess.o c_typecheck_base.o c_typecheck_initializer.o c_typecheck_typecast.o c_typecheck_code.o c_typecheck_expr.o c_typecheck_type.o string_constant.o c_qualifiers.o c_typecheck_argc_argv.o ansi_c_parse_tree.o preprocessor_line.o ansi_c_convert.o ansi_c_convert_type.o type2name.o cprover_library.o anonymous_member.o printf_formatter.o ansi_c_internal_additions.o padding.o ansi_c_declaration.o designator.o literals/parse_float.o literals/unescape_string.o literals/convert_float_literal.o literals/convert_character_literal.o literals/convert_integer_literal.o literals/convert_string_literal.o
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/cpp'
>## Entering xmllang
>make  -C xmllang
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/xmllang'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o xml_parser.o xml_parser.cpp
>bison -y -v $flags -pyyxml -d parser.y -o xml_y.tab.cpp
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/ansi-c'
>## Entering assembler
>flex -Pyyxml -oxml_lex.yy.cpp scanner.l
>make  -C assembler
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o xml_parse_tree.o xml_parse_tree.cpp
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/assembler'
>flex -Pyyassembler -oassembler_lex.yy.cpp scanner.l
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o assembler_parser.o assembler_parser.cpp
>if [ -e xml_y.tab.hpp ] ; then mv xml_y.tab.hpp xml_y.tab.h ; else \
>        mv xml_y.tab.cpp.h xml_y.tab.h ; fi
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o xml_y.tab.o xml_y.tab.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o assembler_lex.yy.o assembler_lex.yy.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o xml_lex.yy.o xml_lex.yy.cpp
>ld -r -o assembler.a assembler_lex.yy.o assembler_parser.o
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/assembler'
>## Entering java_bytecode
>make  -C java_bytecode
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/java_bytecode'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_bytecode_language.o java_bytecode_language.cpp
>ld -r -o xmllang.a xml_parser.o xml_y.tab.o xml_lex.yy.o xml_parse_tree.o
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/xmllang'
>## Entering solvers
>make  -C solvers
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/solvers'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o sat/satcheck_minisat2.o sat/satcheck_minisat2.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_bytecode_parse_tree.o java_bytecode_parse_tree.cpp
>In file included from /usr/include/minisat/core/Solver.h:27:0,
>                 from sat/satcheck_minisat2.cpp:21:
>/usr/include/minisat/utils/Options.h: In member function 'bool Minisat::Option::OptionLt::operator()(const Minisat::Option*, const Minisat::Option*)':
>/usr/include/minisat/utils/Options.h:63:44: warning: suggest parentheses around '&&' within '||' [-Wparentheses]
>             return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
>                                            ^
>In file included from /usr/include/minisat/core/Solver.h:24:0,
>                 from sat/satcheck_minisat2.cpp:21:
>/usr/include/minisat/mtl/Vec.h: In instantiation of 'void Minisat::vec<T>::capacity(int) [with T = Minisat::Lit]':
>sat/satcheck_minisat2.cpp:42:26:   required from here
>/usr/include/minisat/mtl/Vec.h:99:32: warning: suggest parentheses around '&&' within '||' [-Wparentheses]
>     if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
>                                ^
>/usr/include/minisat/mtl/Vec.h: In instantiation of 'void Minisat::vec<T>::capacity(int) [with T = Minisat::Option*]':
>/usr/include/minisat/mtl/Vec.h:74:61:   required from 'void Minisat::vec<T>::push(const T&) [with T = Minisat::Option*]'
>/usr/include/minisat/utils/Options.h:76:34:   required from here
>/usr/include/minisat/mtl/Vec.h:99:32: warning: suggest parentheses around '&&' within '||' [-Wparentheses]
>/usr/include/minisat/mtl/Vec.h: In instantiation of 'void Minisat::vec<T>::capacity(int) [with T = int]':
>/usr/include/minisat/mtl/Vec.h:74:61:   required from 'void Minisat::vec<T>::push(const T&) [with T = int]'
>/usr/include/minisat/core/Solver.h:317:69:   required from here
>/usr/include/minisat/mtl/Vec.h:99:32: warning: suggest parentheses around '&&' within '||' [-Wparentheses]
>/usr/include/minisat/mtl/Vec.h: In instantiation of 'void Minisat::vec<T>::capacity(int) [with T = Minisat::lbool]':
>/usr/include/minisat/mtl/Vec.h:115:18:   required from 'void Minisat::vec<T>::growTo(int) [with T = Minisat::lbool]'
>sat/satcheck_minisat2.cpp:256:3:   required from 'void satcheck_minisat2_baset<T>::set_assignment(literalt, bool) [with T = Minisat::SimpSolver]'
>sat/satcheck_minisat2.cpp:418:1:   required from here
>/usr/include/minisat/mtl/Vec.h:99:32: warning: suggest parentheses around '&&' within '||' [-Wparentheses]
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o qbf/qbf_bdd_core.o qbf/qbf_bdd_core.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_bytecode_typecheck.o java_bytecode_typecheck.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o javap_parse.o javap_parse.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o qbf/qbf_skizzo_core.o qbf/qbf_skizzo_core.cpp
>qbf/qbf_skizzo_core.cpp: In member function 'virtual propt::resultt qbf_skizzo_coret::prop_solve()':
>qbf/qbf_skizzo_core.cpp:124:41: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result]
>          " > "+result_tmp_file).c_str());
>                                         ^
>qbf/qbf_skizzo_core.cpp: In member function 'bool qbf_skizzo_coret::get_certificate()':
>qbf/qbf_skizzo_core.cpp:235:42: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result]
>           " > "+result_tmp_file).c_str());
>                                          ^
>qbf/qbf_skizzo_core.cpp:327:81: warning: ignoring return value of 'int system(const char*)', declared with attribute warn_unused_result [-Wunused-result]
>     system(("sed -e \"s/^#.*$/# no comment/\" -i "+qbf_tmp_file+".qbm").c_str());
>                                                                                 ^
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_bytecode_convert.o java_bytecode_convert.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o sat/cnf.o sat/cnf.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o sat/dimacs_cnf.o sat/dimacs_cnf.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_types.o java_types.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o sat/cnf_clause_list.o sat/cnf_clause_list.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_entry_point.o java_entry_point.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o sat/pbs_dimacs_cnf.o sat/pbs_dimacs_cnf.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_bytecode_typecheck_code.o java_bytecode_typecheck_code.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_bytecode_typecheck_expr.o java_bytecode_typecheck_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o sat/read_dimacs_cnf.o sat/read_dimacs_cnf.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_bytecode_typecheck_type.o java_bytecode_typecheck_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o sat/resolution_proof.o sat/resolution_proof.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o sat/satcheck.o sat/satcheck.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o java_bytecode_internal_additions.o java_bytecode_internal_additions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o qbf/qdimacs_cnf.o qbf/qdimacs_cnf.cpp
>ld -r -o java_bytecode.a java_bytecode_language.o java_bytecode_parse_tree.o java_bytecode_typecheck.o javap_parse.o java_bytecode_convert.o java_types.o java_entry_point.o java_bytecode_typecheck_code.o java_bytecode_typecheck_expr.o java_bytecode_typecheck_type.o java_bytecode_internal_additions.o
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/java_bytecode'
>## Entering goto-symex
>make  -C goto-symex
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o qbf/qbf_quantor.o qbf/qbf_quantor.cpp
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/goto-symex'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_target.o symex_target.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o qbf/qbf_skizzo.o qbf/qbf_skizzo.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_target_equation.o symex_target_equation.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o qbf/qdimacs_core.o qbf/qdimacs_core.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_symex.o goto_symex.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o qbf/qbf_qube.o qbf/qbf_qube.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_main.o symex_main.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o qbf/qbf_qube_core.o qbf/qbf_qube_core.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o build_goto_trace.o build_goto_trace.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o prop/prop.o prop/prop.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o adjust_float_expressions.o adjust_float_expressions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o prop/prop_conv.o prop/prop_conv.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_function_call.o symex_function_call.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o prop/prop_conv_store.o prop/prop_conv_store.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o prop/cover_goals.o prop/cover_goals.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_symex_state.o goto_symex_state.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o prop/aig.o prop/aig.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o prop/aig_prop.o prop/aig_prop.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_dereference.o symex_dereference.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o prop/minimize.o prop/minimize.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_goto.o symex_goto.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o prop/prop_assignment.o prop/prop_assignment.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_builtin_functions.o symex_builtin_functions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o cvc/cvc_conv.o cvc/cvc_conv.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o slice.o slice.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o cvc/cvc_dec.o cvc/cvc_dec.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_other.o symex_other.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o slice_by_trace.o slice_by_trace.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o smt1/smt1_dec.o smt1/smt1_dec.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_decl.o symex_decl.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o smt1/smt1_conv.o smt1/smt1_conv.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_dead.o symex_dead.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o smt2/smt2_dec.o smt2/smt2_dec.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o precondition.o precondition.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o smt2/smt2_conv.o smt2/smt2_conv.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o postcondition.o postcondition.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/equality.o flattening/equality.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_clean_expr.o symex_clean_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/arrays.o flattening/arrays.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_dereference_state.o symex_dereference_state.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/functions.o flattening/functions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o auto_objects.o auto_objects.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_catch.o symex_catch.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/bv_minimize.o flattening/bv_minimize.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_start_thread.o symex_start_thread.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_width.o flattening/boolbv_width.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv.o flattening/boolbv.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_assign.o symex_assign.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_throw.o symex_throw.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_constraint_select_one.o flattening/boolbv_constraint_select_one.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o symex_atomic_section.o symex_atomic_section.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/bv_pointers.o flattening/bv_pointers.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o memory_model.o memory_model.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/bv_utils.o flattening/bv_utils.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o memory_model_sc.o memory_model_sc.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_abs.o flattening/boolbv_abs.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o partial_order_concurrency.o partial_order_concurrency.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_with.o flattening/boolbv_with.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o memory_model_tso.o memory_model_tso.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_typecast.o flattening/boolbv_typecast.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o memory_model_pso.o memory_model_pso.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_index.o flattening/boolbv_index.cpp
>ld -r -o goto-symex.a symex_target.o symex_target_equation.o goto_symex.o symex_main.o build_goto_trace.o adjust_float_expressions.o symex_function_call.o goto_symex_state.o symex_dereference.o symex_goto.o symex_builtin_functions.o slice.o symex_other.o slice_by_trace.o symex_decl.o symex_dead.o precondition.o postcondition.o symex_clean_expr.o symex_dereference_state.o auto_objects.o symex_catch.o symex_start_thread.o symex_assign.o symex_throw.o symex_atomic_section.o memory_model.o memory_model_sc.o partial_order_concurrency.o memory_model_tso.o memory_model_pso.o
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_member.o flattening/boolbv_member.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_if.o flattening/boolbv_if.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_byte_extract.o flattening/boolbv_byte_extract.cpp
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/goto-symex'
>## Entering analyses
>make  -C analyses
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_add_sub.o flattening/boolbv_add_sub.cpp
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/analyses'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o natural_loops.o natural_loops.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_mult.o flattening/boolbv_mult.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o is_threaded.o is_threaded.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_constant.o flattening/boolbv_constant.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o dirty.o dirty.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_extractbit.o flattening/boolbv_extractbit.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o interval_analysis.o interval_analysis.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_bv_rel.o flattening/boolbv_bv_rel.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o invariant_set.o invariant_set.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_shift.o flattening/boolbv_shift.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o invariant_set_domain.o invariant_set_domain.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_case.o flattening/boolbv_case.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o invariant_propagation.o invariant_propagation.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_cond.o flattening/boolbv_cond.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o static_analysis.o static_analysis.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_concatenation.o flattening/boolbv_concatenation.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o uninitialized_domain.o uninitialized_domain.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_div.o flattening/boolbv_div.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o local_may_alias.o local_may_alias.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_mod.o flattening/boolbv_mod.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o locals.o locals.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_extractbits.o flattening/boolbv_extractbits.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_check.o goto_check.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_replication.o flattening/boolbv_replication.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o call_graph.o call_graph.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_reduction.o flattening/boolbv_reduction.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o interval_domain.o interval_domain.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_overflow.o flattening/boolbv_overflow.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o reaching_definitions.o reaching_definitions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_get.o flattening/boolbv_get.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_bitwise.o flattening/boolbv_bitwise.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o ai.o ai.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_equality.o flattening/boolbv_equality.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o local_cfg.o local_cfg.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_unary_minus.o flattening/boolbv_unary_minus.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o local_bitvector_analysis.o local_bitvector_analysis.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_ieee_float_rel.o flattening/boolbv_ieee_float_rel.cpp
>ld -r -o analyses.a natural_loops.o is_threaded.o dirty.o interval_analysis.o invariant_set.o invariant_set_domain.o invariant_propagation.o static_analysis.o uninitialized_domain.o local_may_alias.o locals.o goto_check.o call_graph.o interval_domain.o reaching_definitions.o ai.o local_cfg.o local_bitvector_analysis.o
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/pointer_logic.o flattening/pointer_logic.cpp
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/analyses'
>## Entering pointer-analysis
>make  -C pointer-analysis
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/pointer-analysis'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set.o value_set.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_quantifier.o flattening/boolbv_quantifier.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_program_dereference.o goto_program_dereference.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_struct.o flattening/boolbv_struct.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_analysis.o value_set_analysis.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_byte_update.o flattening/boolbv_byte_update.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o dereference.o dereference.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_array_of.o flattening/boolbv_array_of.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o pointer_offset_sum.o pointer_offset_sum.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o add_failed_symbols.o add_failed_symbols.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_map.o flattening/boolbv_map.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o show_value_sets.o show_value_sets.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_type.o flattening/boolbv_type.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_array.o flattening/boolbv_array.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_domain.o value_set_domain.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o rewrite_index.o rewrite_index.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_vector.o flattening/boolbv_vector.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_analysis_fi.o value_set_analysis_fi.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_complex.o flattening/boolbv_complex.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_fi.o value_set_fi.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_floatbv_op.o flattening/boolbv_floatbv_op.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_domain_fi.o value_set_domain_fi.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_union.o flattening/boolbv_union.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_analysis_fivr.o value_set_analysis_fivr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/flatten_byte_operators.o flattening/flatten_byte_operators.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_fivr.o value_set_fivr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o flattening/boolbv_update.o flattening/boolbv_update.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_domain_fivr.o value_set_domain_fivr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o floatbv/float_utils.o floatbv/float_utils.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_analysis_fivrns.o value_set_analysis_fivrns.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o floatbv/float_bv.o floatbv/float_bv.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_fivrns.o value_set_fivrns.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o refinement/bv_refinement_loop.o refinement/bv_refinement_loop.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o refinement/refine_arithmetic.o refinement/refine_arithmetic.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_domain_fivrns.o value_set_domain_fivrns.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches -m64 -I ..    -I /usr/include/minisat   -I /usr/include/cudd     -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -DHAVE_QBF_CORE -o refinement/refine_arrays.o refinement/refine_arrays.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o value_set_dereference.o value_set_dereference.cpp
>ld -r -o solvers.a sat/satcheck_minisat2.o qbf/qbf_bdd_core.o qbf/qbf_skizzo_core.o sat/cnf.o sat/dimacs_cnf.o sat/cnf_clause_list.o sat/pbs_dimacs_cnf.o sat/read_dimacs_cnf.o sat/resolution_proof.o sat/satcheck.o qbf/qdimacs_cnf.o qbf/qbf_quantor.o qbf/qbf_skizzo.o qbf/qdimacs_core.o qbf/qbf_qube.o qbf/qbf_qube_core.o prop/prop.o prop/prop_conv.o prop/prop_conv_store.o prop/cover_goals.o prop/aig.o prop/aig_prop.o prop/minimize.o prop/prop_assignment.o cvc/cvc_conv.o cvc/cvc_dec.o smt1/smt1_dec.o smt1/smt1_conv.o smt2/smt2_dec.o smt2/smt2_conv.o flattening/equality.o flattening/arrays.o flattening/functions.o flattening/bv_minimize.o flattening/boolbv_width.o flattening/boolbv.o flattening/boolbv_constraint_select_one.o flattening/bv_pointers.o flattening/bv_utils.o flattening/boolbv_abs.o flattening/boolbv_with.o flattening/boolbv_typecast.o flattening/boolbv_index.o flattening/boolbv_member.o flattening/boolbv_if.o flattening/boolbv_byte_extract.o flattening/boolbv_add_sub.o flattening/boolbv_mult.o flattening/boolbv_constant.o flattening/boolbv_extractbit.o flattening/boolbv_bv_rel.o flattening/boolbv_shift.o flattening/boolbv_case.o flattening/boolbv_cond.o flattening/boolbv_concatenation.o flattening/boolbv_div.o flattening/boolbv_mod.o flattening/boolbv_extractbits.o flattening/boolbv_replication.o flattening/boolbv_reduction.o flattening/boolbv_overflow.o flattening/boolbv_get.o flattening/boolbv_bitwise.o flattening/boolbv_equality.o flattening/boolbv_unary_minus.o flattening/boolbv_ieee_float_rel.o flattening/pointer_logic.o flattening/boolbv_quantifier.o flattening/boolbv_struct.o flattening/boolbv_byte_update.o flattening/boolbv_array_of.o flattening/boolbv_map.o flattening/boolbv_type.o flattening/boolbv_array.o flattening/boolbv_vector.o flattening/boolbv_complex.o flattening/boolbv_floatbv_op.o flattening/boolbv_union.o flattening/flatten_byte_operators.o flattening/boolbv_update.o floatbv/float_utils.o floatbv/float_bv.o refinement/bv_refinement_loop.o refinement/refine_arithmetic.o refinement/refine_arrays.o
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o dereference_callback.o dereference_callback.cpp
>ld -r -o pointer-analysis.a value_set.o goto_program_dereference.o value_set_analysis.o dereference.o pointer_offset_sum.o add_failed_symbols.o show_value_sets.o value_set_domain.o rewrite_index.o value_set_analysis_fi.o value_set_fi.o value_set_domain_fi.o value_set_analysis_fivr.o value_set_fivr.o value_set_domain_fivr.o value_set_analysis_fivrns.o value_set_fivrns.o value_set_domain_fivrns.o value_set_dereference.o dereference_callback.o
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/pointer-analysis'
>## Entering goto-programs
>make  -C goto-programs
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/goto-programs'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_convert.o goto_convert.cpp
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/solvers'
>## Entering linking
>make  -C linking
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_convert_function_call.o goto_convert_function_call.cpp
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/linking'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o linking.o linking.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_convert_side_effect.o goto_convert_side_effect.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o linking_type_eq.o linking_type_eq.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o zero_initializer.o zero_initializer.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_program.o goto_program.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o remove_internal_symbols.o remove_internal_symbols.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o basic_blocks.o basic_blocks.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o entry_point.o entry_point.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_convert_exceptions.o goto_convert_exceptions.cpp
>ld -r -o linking.a linking.o linking_type_eq.o zero_initializer.o remove_internal_symbols.o entry_point.o
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o remove_function_pointers.o remove_function_pointers.cpp
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/linking'
>## Entering path-symex
>make  -C path-symex
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/path-symex'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o locs.o locs.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_functions.o goto_functions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o var_map.o var_map.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_inline.o goto_inline.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o path_symex_history.o path_symex_history.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o remove_skip.o remove_skip.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o path_symex_state.o path_symex_state.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_convert_functions.o goto_convert_functions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o path_symex.o path_symex.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o string_instrumentation.o string_instrumentation.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o build_goto_trace.o build_goto_trace.cpp
>ld -r -o path-symex.a locs.o var_map.o path_symex_history.o path_symex_state.o path_symex.o build_goto_trace.o
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o builtin_functions.o builtin_functions.cpp
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/path-symex'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o show_properties.o show_properties.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o set_properties.o set_properties.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o read_goto_binary.o read_goto_binary.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_asm.o goto_asm.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o elf_reader.o elf_reader.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o string_abstraction.o string_abstraction.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o destructor.o destructor.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_program_serialization.o goto_program_serialization.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_function_serialization.o goto_function_serialization.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o read_bin_goto_object.o read_bin_goto_object.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_program_irep.o goto_program_irep.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o interpreter.o interpreter.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o interpreter_evaluate.o interpreter_evaluate.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o flow_insensitive_analysis.o flow_insensitive_analysis.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o format_strings.o format_strings.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o loop_ids.o loop_ids.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o pointer_arithmetic.o pointer_arithmetic.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_program_template.o goto_program_template.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o write_goto_binary.o write_goto_binary.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o remove_unreachable.o remove_unreachable.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o remove_unused_functions.o remove_unused_functions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o wp.o wp.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_rw.o goto_rw.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_clean_expr.o goto_clean_expr.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o safety_checker.o safety_checker.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o compute_called_functions.o compute_called_functions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o link_to_library.o link_to_library.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o remove_returns.o remove_returns.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o osx_fat_reader.o osx_fat_reader.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o goto_trace.o goto_trace.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o xml_goto_trace.o xml_goto_trace.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -o vcd_goto_trace.o vcd_goto_trace.cpp
>ld -r -o goto-programs.a goto_convert.o goto_convert_function_call.o goto_convert_side_effect.o goto_program.o basic_blocks.o goto_convert_exceptions.o remove_function_pointers.o goto_functions.o goto_inline.o remove_skip.o goto_convert_functions.o string_instrumentation.o builtin_functions.o show_properties.o set_properties.o read_goto_binary.o goto_asm.o elf_reader.o string_abstraction.o destructor.o goto_program_serialization.o goto_function_serialization.o read_bin_goto_object.o goto_program_irep.o interpreter.o interpreter_evaluate.o flow_insensitive_analysis.o format_strings.o loop_ids.o pointer_arithmetic.o goto_program_template.o write_goto_binary.o remove_unreachable.o remove_unused_functions.o wp.o goto_rw.o goto_clean_expr.o safety_checker.o compute_called_functions.o link_to_library.o remove_returns.o osx_fat_reader.o goto_trace.o xml_goto_trace.o vcd_goto_trace.o
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/goto-programs'
>## Entering cbmc
>## Entering goto-cc
>make  -C goto-cc
>make  -C cbmc
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/goto-cc'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o goto_cc_main.o goto_cc_main.cpp
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/cbmc'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o cbmc_main.o cbmc_main.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o cbmc_parseoptions.o cbmc_parseoptions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o goto_cc_mode.o goto_cc_mode.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o gcc_mode.o gcc_mode.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o bmc.o bmc.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o get_base_name.o get_base_name.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o dimacs.o dimacs.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o gcc_cmdline.o gcc_cmdline.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o cbmc_languages.o cbmc_languages.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o ms_cl_cmdline.o ms_cl_cmdline.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o ld_cmdline.o ld_cmdline.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o counterexample_beautification.o counterexample_beautification.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o compile.o compile.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o bv_cbmc.o bv_cbmc.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o symex_bmc.o symex_bmc.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o armcc_cmdline.o armcc_cmdline.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o run.o run.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o show_vcc.o show_vcc.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o goto_cc_languages.o goto_cc_languages.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o cbmc_solvers.o cbmc_solvers.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o goto_cc_cmdline.o goto_cc_cmdline.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o ms_cl_mode.o ms_cl_mode.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o xml_interface.o xml_interface.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o armcc_mode.o armcc_mode.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o cover.o cover.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o cw_mode.o cw_mode.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -DHAVE_JAVA_BYTECODE -o all_claims.o all_claims.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -D HAVE_CPP -o ld_mode.o ld_mode.cpp
>g++  -o cbmc ../ansi-c/ansi-c.a ../linking/linking.a ../big-int/big-int.a ../goto-programs/goto-programs.a ../goto-symex/goto-symex.a ../pointer-analysis/value_set.o ../pointer-analysis/value_set_dereference.o ../pointer-analysis/dereference_callback.o ../pointer-analysis/add_failed_symbols.o ../pointer-analysis/rewrite_index.o ../pointer-analysis/goto_program_dereference.o ../analyses/analyses.a ../langapi/langapi.a ../xmllang/xmllang.a ../assembler/assembler.a ../solvers/solvers.a ../util/util.a cbmc_main.o cbmc_parseoptions.o bmc.o dimacs.o cbmc_languages.o counterexample_beautification.o bv_cbmc.o symex_bmc.o show_vcc.o cbmc_solvers.o xml_interface.o cover.o all_claims.o ../cpp/cpp.a ../java_bytecode/java_bytecode.a -Wl,--as-needed -Wl,-z,relro  -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
>g++  -o goto-cc ../big-int/big-int.a ../goto-programs/goto-programs.a ../util/util.a ../linking/linking.a ../ansi-c/ansi-c.a ../xmllang/xmllang.a ../assembler/assembler.a ../langapi/langapi.a goto_cc_main.o goto_cc_mode.o gcc_mode.o get_base_name.o gcc_cmdline.o ms_cl_cmdline.o ld_cmdline.o compile.o armcc_cmdline.o run.o goto_cc_languages.o goto_cc_cmdline.o ms_cl_mode.o armcc_mode.o cw_mode.o ld_mode.o ../cpp/cpp.a -Wl,--as-needed -Wl,-z,relro  
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/goto-cc'
>## Entering goto-instrument
>make  -C goto-instrument
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/goto-instrument'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o goto_instrument_main.o goto_instrument_main.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o goto_instrument_parseoptions.o goto_instrument_parseoptions.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o document_properties.o document_properties.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o goto_instrument_languages.o goto_instrument_languages.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o uninitialized.o uninitialized.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o full_slicer.o full_slicer.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o k_induction.o k_induction.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o object_id.o object_id.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o show_locations.o show_locations.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o points_to.o points_to.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o alignment_checks.o alignment_checks.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o race_check.o race_check.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o rw_set.o rw_set.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o nondet_volatile.o nondet_volatile.cpp
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/cbmc'
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o interrupt.o interrupt.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o function.o function.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o branch.o branch.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o mmio.o mmio.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o stack_depth.o stack_depth.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o nondet_static.o nondet_static.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o concurrency.o concurrency.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o dump_c.o dump_c.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o dot.o dot.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o havoc_loops.o havoc_loops.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o wmm/weak_memory.o wmm/weak_memory.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o wmm/fence.o wmm/fence.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o wmm/event_graph.o wmm/event_graph.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o wmm/goto2graph.o wmm/goto2graph.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o wmm/data_dp.o wmm/data_dp.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o wmm/abstract_event.o wmm/abstract_event.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o wmm/instrumenter_strategies.o wmm/instrumenter_strategies.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o wmm/cycle_collection.o wmm/cycle_collection.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o call_sequences.o call_sequences.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o unwind.o unwind.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o accelerate/accelerate.o accelerate/accelerate.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o accelerate/polynomial.o accelerate/polynomial.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o accelerate/scratch_program.o accelerate/scratch_program.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o accelerate/polynomial_accelerator.o accelerate/polynomial_accelerator.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o accelerate/util.o accelerate/util.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o count_eloc.o count_eloc.cpp
>g++ -c -MMD -MP -DSTL_HASH_TR1 -O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -fstack-protector-strong --param=ssp-buffer-size=4 -grecord-gcc-switches  -m64 -I .. -DHAVE_CPP -o reachability_slicer.o reachability_slicer.cpp
>g++  -o goto-instrument ../ansi-c/ansi-c.a ../linking/linking.a ../big-int/big-int.a ../goto-programs/goto-programs.a ../goto-symex/goto-symex.a ../assembler/assembler.a ../pointer-analysis/pointer-analysis.a ../analyses/analyses.a ../langapi/langapi.a ../util/util.a ../solvers/solvers.a goto_instrument_main.o goto_instrument_parseoptions.o document_properties.o goto_instrument_languages.o uninitialized.o full_slicer.o k_induction.o object_id.o show_locations.o points_to.o alignment_checks.o race_check.o rw_set.o nondet_volatile.o interrupt.o function.o branch.o mmio.o stack_depth.o nondet_static.o concurrency.o dump_c.o dot.o havoc_loops.o wmm/weak_memory.o wmm/fence.o wmm/event_graph.o wmm/goto2graph.o wmm/data_dp.o wmm/abstract_event.o wmm/instrumenter_strategies.o wmm/cycle_collection.o call_sequences.o unwind.o accelerate/accelerate.o accelerate/polynomial.o accelerate/scratch_program.o accelerate/polynomial_accelerator.o accelerate/util.o count_eloc.o reachability_slicer.o ../cpp/cpp.a -Wl,--as-needed -Wl,-z,relro  -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src/goto-instrument'
>make: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/src'
>+ pushd doc/guide
>~/rpmbuild/BUILD/cbmc-4.7/doc/guide ~/rpmbuild/BUILD/cbmc-4.7
>+ pdflatex CBMC-guide.tex
>This is pdfTeX, Version 3.14159265-2.6-1.40.15 (TeX Live 2014) (preloaded format=pdflatex)
> restricted \write18 enabled.
>entering extended mode
>(./CBMC-guide.tex
>LaTeX2e <2011/06/27>
>Babel <3.9k> and hyphenation patterns for 2 languages loaded.
>(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
>Document Class: article 2007/10/19 v1.4h Standard LaTeX document class
>(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo))
>No file CBMC-guide.aux.
>
>LaTeX Warning: Reference `section:other-apps' on page 1 undefined on input line
> 41.
>
>
>LaTeX Warning: Reference `section:util' on page 1 undefined on input line 48.
>
>[1{/usr/share/texlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}]
>
>LaTeX Warning: Reference `section:CBMC' on page 2 undefined on input line 93.
>
>
>LaTeX Warning: Reference `section:goto-cc' on page 2 undefined on input line 96
>.
>
>
>LaTeX Warning: Reference `section:goto-instrument' on page 2 undefined on input
> line 99.
>
>[2] [3]
>
>LaTeX Warning: Reference `section:irept' on page 4 undefined on input line 241.
>
>
>[4]
>Overfull \hbox (2.44667pt too wide) in paragraph at lines 260--262
>[]\OT1/cmr/m/n/10 The wrap-per class for multi-precision arith-metic within CPR
>OVER.
>[5]
>
>LaTeX Warning: Reference `section:goto-programs' on page 6 undefined on input l
>ine 325.
>
>[6] [7]
>Overfull \hbox (12.80382pt too wide) in paragraph at lines 440--448
>[]\OT1/cmr/m/n/10 Provides the \OT1/cmtt/m/n/10 smt2[]dect \OT1/cmr/m/n/10 type
> which func-tions in a sim-i-lar way to \OT1/cmtt/m/n/10 smt1[]dect\OT1/cmr/m/n
>/10 ,
>[8]
>Overfull \hbox (6.13939pt too wide) in paragraph at lines 568--576
>\OT1/cmr/m/n/10 There are a large num-ber of kind of tree struc-tured or tree-l
>ike data in CPROVER.
>[9] [10]
>Overfull \hbox (18.3098pt too wide) in paragraph at lines 653--671
>\OT1/cmr/m/n/10 The com-mon start-ing point for work-ing with goto-programs is 
>the \OT1/cmtt/m/n/10 read[]goto[]binary
>
>Overfull \hbox (27.36626pt too wide) in paragraph at lines 653--671
>\OT1/cmtt/m/n/10 goto[]functions.h \OT1/cmr/m/n/10 and is an in-stan-ti-a-tion 
>of the tem-plate \OT1/cmtt/m/n/10 goto[]functions[]templatet
>
>Overfull \hbox (48.46867pt too wide) in paragraph at lines 691--711
>\OT1/cmr/m/n/10 one step in the func-tion. Each has a type, an in-stance of \OT
>1/cmtt/m/n/10 goto[]program[]instruction[]typet
>[11] [12] (./CBMC-guide.aux)
>
>LaTeX Warning: There were undefined references.
>
>
>LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
>
> )
>(see the transcript file for additional information)</usr/share/texlive/texmf-d
>ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
>nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
>pe1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
>lic/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
>fonts/cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
>m/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.p
>fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr
>/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy6.pfb></usr/share/
>texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive
>/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf
>-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-dist/
>fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fonts/
>type1/public/amsfonts/cm/cmtt8.pfb>
>Output written on CBMC-guide.pdf (12 pages, 184199 bytes).
>Transcript written on CBMC-guide.log.
>+ pdflatex CBMC-guide.tex
>This is pdfTeX, Version 3.14159265-2.6-1.40.15 (TeX Live 2014) (preloaded format=pdflatex)
> restricted \write18 enabled.
>entering extended mode
>(./CBMC-guide.tex
>LaTeX2e <2011/06/27>
>Babel <3.9k> and hyphenation patterns for 2 languages loaded.
>(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
>Document Class: article 2007/10/19 v1.4h Standard LaTeX document class
>(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo)) (./CBMC-guide.aux)
>[1{/usr/share/texlive/texmf-dist/fonts/map/pdftex/updmap/pdftex.map}] [2]
>[3] [4]
>Overfull \hbox (2.44667pt too wide) in paragraph at lines 260--262
>[]\OT1/cmr/m/n/10 The wrap-per class for multi-precision arith-metic within CPR
>OVER.
>[5] [6] [7]
>Overfull \hbox (12.80382pt too wide) in paragraph at lines 440--448
>[]\OT1/cmr/m/n/10 Provides the \OT1/cmtt/m/n/10 smt2[]dect \OT1/cmr/m/n/10 type
> which func-tions in a sim-i-lar way to \OT1/cmtt/m/n/10 smt1[]dect\OT1/cmr/m/n
>/10 ,
>[8]
>Overfull \hbox (6.13939pt too wide) in paragraph at lines 568--576
>\OT1/cmr/m/n/10 There are a large num-ber of kind of tree struc-tured or tree-l
>ike data in CPROVER.
>[9] [10]
>Overfull \hbox (18.3098pt too wide) in paragraph at lines 653--671
>\OT1/cmr/m/n/10 The com-mon start-ing point for work-ing with goto-programs is 
>the \OT1/cmtt/m/n/10 read[]goto[]binary
>
>Overfull \hbox (27.36626pt too wide) in paragraph at lines 653--671
>\OT1/cmtt/m/n/10 goto[]functions.h \OT1/cmr/m/n/10 and is an in-stan-ti-a-tion 
>of the tem-plate \OT1/cmtt/m/n/10 goto[]functions[]templatet
>
>Overfull \hbox (48.46867pt too wide) in paragraph at lines 691--711
>\OT1/cmr/m/n/10 one step in the func-tion. Each has a type, an in-stance of \OT
>1/cmtt/m/n/10 goto[]program[]instruction[]typet
>[11] [12] (./CBMC-guide.aux) )
>(see the transcript file for additional information)</usr/share/texlive/texmf-d
>ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
>nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
>pe1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
>lic/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
>fonts/cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
>m/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.p
>fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr
>/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy6.pfb></usr/share/
>texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive
>/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf
>-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-dist/
>fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fonts/
>type1/public/amsfonts/cm/cmtt8.pfb>
>Output written on CBMC-guide.pdf (12 pages, 183881 bytes).
>Transcript written on CBMC-guide.log.
>+ popd
>~/rpmbuild/BUILD/cbmc-4.7
>+ exit 0
>Executing(%install): /bin/sh -e /home/root/rpmbuild/tmp/rpm-tmp.GKRNDe
>+ umask 022
>+ cd /home/root/rpmbuild/BUILD
>+ '[' /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le '!=' / ']'
>+ rm -rf /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le
>++ dirname /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le
>+ mkdir -p /home/root/rpmbuild/BUILDROOT
>+ mkdir /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le
>+ cd cbmc-4.7
>+ mkdir -p /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/bin /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/share/man/man1
>+ install -p -m 0755 src/cbmc/cbmc /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/bin
>+ install -p -m 0755 src/goto-cc/goto-cc /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/bin
>+ install -p -m 0755 src/goto-instrument/goto-instrument /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/bin
>+ install -p -m 0644 doc/man/cbmc.1 /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/share/man/man1
>+ /usr/lib/rpm/find-debuginfo.sh --strict-build-id -m --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 50000000 /home/root/rpmbuild/BUILD/cbmc-4.7
>extracting debug info from /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/bin/goto-cc
>extracting debug info from /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/bin/goto-instrument
>extracting debug info from /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/bin/cbmc
>/usr/lib/rpm/sepdebugcrcfix: Updated 3 CRC32s, 0 CRC32s did match.
>cpio: cbmc-4.7/src/xmllang/xml_y.tab.hpp: Cannot stat: No such file or directory
>11750 blocks
>+ /usr/lib/rpm/check-buildroot
>+ /usr/lib/rpm/brp-compress
>+ /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip
>+ /usr/lib/rpm/brp-python-bytecompile /usr/bin/python 1
>+ /usr/lib/rpm/brp-python-hardlink
>+ /usr/lib/rpm/redhat/brp-java-repack-jars
>Executing(%check): /bin/sh -e /home/root/rpmbuild/tmp/rpm-tmp.OUwccG
>+ umask 022
>+ cd /home/root/rpmbuild/BUILD
>+ cd cbmc-4.7
>+ cd regression
>+ make
>make -C ansi-c test;  make -C cbmc test;  make -C cpp test;
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/regression/ansi-c'
>Loading
>  63 tests found
>
>Running tests
>  Running Assignment_to_typecast1  [OK]
>  Running Builtins1  [OK]
>  Running Defines1  [OK]
>  Running Empty_Declaration1  [OK]
>  Running Forward_Declaration1  [OK]
>  Running Forward_Declaration2  [OK]
>  Running Function_parameters1  [OK]
>  Running Incomplete_Type1  [OK]
>  Running Initializer_cast1  [OK]
>  Running KnR1  [OK]
>  Running Lvalue1  [OK]
>  Running MMX1  [OK]
>  Running MMX2  [OK]
>  Running Multiple  [OK]
>  Running Qualifiers1  [OK]
>  Running Recursive_Structure1  [OK]
>  Running Struct_Bitfields1  [OK]
>  Running Struct_Hierarchy1  [OK]
>  Running Struct_Padding2  [OK]
>  Running Struct_Padding3  [OK]
>  Running Struct_Padding4  [OK]
>  Running Struct_Padding5  [OK]
>  Running Struct_Padding6  [OK]
>  Running Transparent_union1  [OK]
>  Running Typecast_to_array_ptr1  [OK]
>  Running Typecast_to_union1  [OK]
>  Running Union_Initialization1  [OK]
>  Running VS_extensions1  [OK]
>  Running Zero_Initialization1  [OK]
>  Running _Alignof1  [OK]
>  Running _Bool1  [OK]
>  Running _Generic1  [OK]
>  Running _Static_assert1  [OK]
>  Running arithmetic_right_shift1  [OK]
>  Running asm1  [OK]
>  Running asm2  [OK]
>  Running character_literals1  [FAILED]
>  Running envp1  [OK]
>  Running extern1  [OK]
>  Running extern2  [OK]
>  Running float_constant1  [OK]
>  Running for_scope1  [OK]
>  Running gcc_attributes1  [SKIPPED]
>  Running gcc_attributes2  [OK]
>  Running gcc_builtin_constant_p1  [OK]
>  Running gcc_types_compatible_p1  [OK]
>  Running integer_constant1  [OK]
>  Running integer_constant2  [OK]
>  Running pragma_pack1  [OK]
>  Running return_void  [OK]
>  Running sizeof1  [OK]
>  Running sizeof2  [OK]
>  Running sizeof3  [OK]
>  Running struct2  [OK]
>  Running struct5  [OK]
>  Running switch1  [OK]
>  Running typedef1  [OK]
>  Running typedef_code  [OK]
>  Running typeof1  [OK]
>  Running windows_h_VS_2005  [OK]
>  Running windows_h_VS_2008  [OK]
>  Running windows_h_VS_2010  [OK]
>  Running windows_h_VS_2012  [OK]
>
>Tests failed
>  1 of 63 tests failed, 1 test skipped
>make[1]: *** [test] Error 1
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/regression/ansi-c'
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/regression/cbmc'
>Loading
>  274 tests found
>
>Running tests
>  Running ASHR1  [OK]
>  Running Address_of1  [FAILED]
>  Running Address_of2  [OK]
>  Running Anonymous_Struct1  [OK]
>  Running Anonymous_Struct2  [OK]
>  Running Anonymous_Struct3  [FAILED]
>  Running Array_Initialization1  [FAILED]
>  Running Array_Initialization2  [OK]
>  Running Array_Initialization3  [FAILED]
>  Running BV_Arithmetic1  [OK]
>  Running BV_Arithmetic2  [OK]
>  Running BV_Arithmetic3  [OK]
>  Running BV_Arithmetic4  [OK]
>  Running BV_Arithmetic5  [OK]
>  Running BV_Arithmetic6  [OK]
>  Running Bitfields1  [OK]
>  Running Bool1  [FAILED]
>  Running Boolean_Guards1  [OK]
>  Running Computed-Goto1  [OK]
>  Running Division1  [FAILED]
>  Running Division2  [OK]
>  Running Double-to-float-no-simp1  [SKIPPED]
>  Running Double-to-float-with-simp1  [FAILED]
>  Running Ellipsis1  [OK]
>  Running Endianness1  [OK]
>  Running Endianness2  [OK]
>  Running Endianness3  [OK]
>  Running Endianness4  [OK]
>  Running Endianness5  [OK]
>  Running Endianness6  [FAILED]
>  Running Error_Label1  [OK]
>  Running Error_Label2  [OK]
>  Running Eval_Order1  [SKIPPED]
>  Running Eval_Order2  [SKIPPED]
>  Running Exceptions1  [OK]
>  Running Failing_Assert1  [OK]
>  Running Fixedbv1  [OK]
>  Running Fixedbv2  [OK]
>  Running Fixedbv3  [OK]
>  Running Fixedbv4  [OK]
>  Running Fixedbv5  [OK]
>  Running Fixedbv6  [OK]
>  Running Fixedbv7  [OK]
>  Running Float-Rounding1  [FAILED]
>  Running Float-div1  [FAILED]
>  Running Float-flags-no-simp1  [FAILED]
>  Running Float-flags-simp1  [FAILED]
>  Running Float-no-simp1  [OK]
>  Running Float-no-simp2  [OK]
>  Running Float-no-simp3  [FAILED]
>  Running Float-no-simp4  [OK]
>  Running Float-no-simp5  [OK]
>  Running Float-no-simp6  [FAILED]
>  Running Float-overflow1  [OK]
>  Running Float-overflow2  [OK]
>  Running Float-to-double1  [FAILED]
>  Running Float-to-double2  [FAILED]
>  Running Float-zero-sum1  [SKIPPED]
>  Running Float1  [OK]
>  Running Float11  [OK]
>  Running Float12  [OK]
>  Running Float13  [FAILED]
>  Running Float14  [OK]
>  Running Float18  [FAILED]
>  Running Float19  [FAILED]
>  Running Float2  [FAILED]
>  Running Float20  [OK]
>  Running Float21  [FAILED]
>  Running Float22  [FAILED]
>  Running Float3  [OK]
>  Running Float4  [OK]
>  Running Float5  [OK]
>  Running Float6  [OK]
>  Running Float7  [OK]
>  Running Float8  [OK]
>  Running Float_lib1  [FAILED]
>  Running Float_lib2  [FAILED]
>  Running Free1  [OK]
>  Running Free2  [OK]
>  Running Free3  [OK]
>  Running Free4  [FAILED]
>  Running Function-KnR1  [FAILED]
>  Running Function1  [OK]
>  Running Function10  [FAILED]
>  Running Function11  [OK]
>  Running Function12  [FAILED]
>  Running Function2  [OK]
>  Running Function3  [OK]
>  Running Function4  [OK]
>  Running Function5  [FAILED]
>  Running Function6  [OK]
>  Running Function7  [OK]
>  Running Function8  [OK]
>  Running Function9  [OK]
>  Running Function_Parameters1  [OK]
>  Running Function_Pointer1  [OK]
>  Running Function_Pointer10  [OK]
>  Running Function_Pointer11  [OK]
>  Running Function_Pointer12  [OK]
>  Running Function_Pointer13  [FAILED]
>  Running Function_Pointer14  [FAILED]
>  Running Function_Pointer15  [FAILED]
>  Running Function_Pointer16  [OK]
>  Running Function_Pointer2  [OK]
>  Running Function_Pointer3  [OK]
>  Running Function_Pointer4  [OK]
>  Running Function_Pointer5  [OK]
>  Running Function_Pointer6  [OK]
>  Running Function_Pointer7  [OK]
>  Running Function_Pointer8  [OK]
>  Running Function_Pointer9  [OK]
>  Running Global_Initialization1  [OK]
>  Running Global_Initialization2  [FAILED]
>  Running Initialization1  [OK]
>  Running Initialization2  [OK]
>  Running Initialization3  [OK]
>  Running Initialization5  [OK]
>  Running Linking1  [OK]
>  Running Linking2  [FAILED]
>  Running Linking3  [OK]
>  Running Linking4  [FAILED]
>  Running Local_out_of_scope1  [OK]
>  Running Malloc12  [SKIPPED]
>  Running Malloc13  [SKIPPED]
>  Running Malloc14  [OK]
>  Running Malloc15  [OK]
>  Running Malloc16  [OK]
>  Running Memmove1  [SKIPPED]
>  Running Memory_leak1  [FAILED]
>  Running Memory_leak2  [FAILED]
>  Running Mod1  [OK]
>  Running Mod2  [FAILED]
>  Running Multi_Dimensional_Array1  [FAILED]
>  Running Multi_Dimensional_Array2  [OK]
>  Running Multi_Dimensional_Array3  [OK]
>  Running Multi_Dimensional_Array4  [OK]
>  Running Multi_Dimensional_Array5  [FAILED]
>  Running Negation1  [OK]
>  Running Overflow_Addition1  [OK]
>  Running Overflow_Multiplication1  [OK]
>  Running Pointer_Arithmetic1  [OK]
>  Running Pointer_Arithmetic10  [OK]
>  Running Pointer_Arithmetic11  [OK]
>  Running Pointer_Arithmetic12  [FAILED]
>  Running Pointer_Arithmetic2  [OK]
>  Running Pointer_Arithmetic3  [OK]
>  Running Pointer_Arithmetic4  [OK]
>  Running Pointer_Arithmetic5  [OK]
>  Running Pointer_Arithmetic6  [OK]
>  Running Pointer_Arithmetic7  [OK]
>  Running Pointer_Arithmetic8  [OK]
>  Running Pointer_Arithmetic9  [OK]
>  Running Pointer_Assume1  [SKIPPED]
>  Running Pointer_array1  [OK]
>  Running Pointer_byte_extract1  [FAILED]
>  Running Pointer_byte_extract2  [OK]
>  Running Pointer_byte_extract3  [OK]
>  Running Pointer_byte_extract4  [FAILED]
>  Running Pointer_byte_extract5  [FAILED]
>  Running Pointer_byte_extract6  [FAILED]
>  Running Pointer_difference1  [OK]
>  Running Promotion1  [FAILED]
>  Running Promotion2  [OK]
>  Running Recursion1  [OK]
>  Running Recursion2  [OK]
>  Running Recursion3  [FAILED]
>  Running Recursion4  [OK]
>  Running Recursion5  [OK]
>  Running Sideeffects1  [OK]
>  Running Sideeffects2  [OK]
>  Running Sideeffects3  [FAILED]
>  Running Sideeffects4  [FAILED]
>  Running Sideeffects5  [OK]
>  Running Sideeffects6  [OK]
>  Running Static2  [OK]
>  Running Static_Functions1  [FAILED]
>  Running String1  [FAILED]
>  Running String2  [OK]
>  Running String3  [SKIPPED]
>  Running String4  [FAILED]
>  Running String5  [OK]
>  Running String6  [FAILED]
>  Running String7  [OK]
>  Running String_Literal1  [FAILED]
>  Running Struct_Bytewise1  [OK]
>  Running Struct_Bytewise2  [FAILED]
>  Running Struct_Initialization1  [OK]
>  Running Struct_Initialization10  [OK]
>  Running Struct_Initialization2  [OK]
>  Running Struct_Initialization3  [OK]
>  Running Struct_Initialization4  [FAILED]
>  Running Struct_Initialization5  [OK]
>  Running Struct_Initialization6  [FAILED]
>  Running Struct_Initialization7  [FAILED]
>  Running Struct_Initialization8  [SKIPPED]
>  Running Struct_Initialization9  [OK]
>  Running Struct_Padding1  [FAILED]
>  Running Typecast1  [OK]
>  Running Undefined_Function1  [OK]
>  Running Unwinding_Assertions_Improved1  [SKIPPED]
>  Running Unwinding_Locality1  [OK]
>  Running Variadic1  [SKIPPED]
>  Running Visual_Studio_Types1  [OK]
>  Running Visual_Studio_Types2  [OK]
>  Running Volatile1  [SKIPPED]
>  Running Zero_Initialization1  [FAILED]
>  Running __func__1  [OK]
>  Running abs1  [OK]
>  Running argv1  [OK]
>  Running atomic_section_seq1  [FAILED]
>  Running character_handling1  [OK]
>  Running comma1  [OK]
>  Running complex1  [FAILED]
>  Running compound_literal1  [FAILED]
>  Running const_ptr1  [OK]
>  Running enum1  [OK]
>  Running enum2  [OK]
>  Running enum3  [OK]
>  Running exit1  [OK]
>  Running extern_initialization1  [FAILED]
>  Running extern_initialization2  [FAILED]
>  Running for-break1  [OK]
>  Running for1  [OK]
>  Running for2  [OK]
>  Running for3  [OK]
>  Running function_option1  [OK]
>  Running gcc_c99-bool-1  [FAILED]
>  Running gcc_conditional_expr1  [OK]
>  Running gcc_local_label1  [FAILED]
>  Running gcc_statement_expression1  [OK]
>  Running gcc_statement_expression2  [FAILED]
>  Running gcc_statement_expression3  [OK]
>  Running gcc_vector1  [FAILED]
>  Running goto1  [OK]
>  Running goto2  [OK]
>  Running goto3  [OK]
>  Running goto4  [OK]
>  Running if1  [OK]
>  Running if2  [OK]
>  Running if3  [OK]
>  Running if4  [OK]
>  Running inline1  [FAILED]
>  Running int-to-float1  [FAILED]
>  Running int-to-float2  [FAILED]
>  Running noop1  [FAILED]
>  Running offsetof1  [FAILED]
>  Running pipe1  [FAILED]
>  Running return1  [OK]
>  Running return3  [OK]
>  Running return4  [OK]
>  Running return5  [OK]
>  Running strtol1  [FAILED]
>  Running strtol2  [FAILED]
>  Running struct1  [OK]
>  Running struct3  [OK]
>  Running struct4  [OK]
>  Running struct6  [OK]
>  Running struct7  [OK]
>  Running struct8  [OK]
>  Running switch1  [OK]
>  Running switch2  [OK]
>  Running switch3  [OK]
>  Running switch4  [OK]
>  Running switch5  [OK]
>  Running switch6  [FAILED]
>  Running union1  [OK]
>  Running union2  [OK]
>  Running union3  [OK]
>  Running union4  [FAILED]
>  Running unsigned_char1  [OK]
>  Running va_list1  [FAILED]
>  Running va_list2  [SKIPPED]
>  Running void_ifthenelse  [OK]
>  Running while1  [OK]
>
>Tests failed
>  80 of 274 tests failed, 14 tests skipped
>make[1]: *** [test] Error 80
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/regression/cbmc'
>make[1]: Entering directory `/home/root/rpmbuild/BUILD/cbmc-4.7/regression/cpp'
>Loading
>  49 tests found
>
>Running tests
>  Running Address_of_Method2  [OK]
>  Running Address_of_Method3  [OK]
>  Running Constant1  [OK]
>  Running Constant2  [OK]
>  Running Constant3  [OK]
>  Running Constant4  [OK]
>  Running Friend2  [OK]
>  Running Function_Bodies1  [OK]
>  Running Function_Overloading1  [OK]
>  Running Function_Overloading2  [OK]
>  Running Method_Scope1  [OK]
>  Running Method_qualifier1  [OK]
>  Running ModeC1  [OK]
>  Running ModeC2  [OK]
>  Running Pointer_Conversion1  [OK]
>  Running Resolver1  [OK]
>  Running Resolver10  [OK]
>  Running Resolver11  [OK]
>  Running Resolver12  [OK]
>  Running Resolver2  [OK]
>  Running Resolver3  [OK]
>  Running Resolver4  [OK]
>  Running Scope1  [OK]
>  Running Templates1  [OK]
>  Running Templates2  [OK]
>  Running Templates7  [OK]
>  Running bitwise_and1  [OK]
>  Running enum1  [OK]
>  Running enum2  [OK]
>  Running enum3  [SKIPPED]
>  Running enum4  [OK]
>  Running enum5  [SKIPPED]
>  Running enum6  [OK]
>  Running lvalue1  [OK]
>  Running namespace4  [OK]
>  Running sizeof1  [OK]
>  Running sizeof2  [OK]
>  Running sizeof3  [OK]
>  Running static_assert1  [OK]
>  Running switch1  [OK]
>  Running typecast_ambiguity1  [OK]
>  Running typecast_ambiguity2  [OK]
>  Running union3  [OK]
>  Running union4  [OK]
>  Running union5  [OK]
>  Running windows_h_VS_2005  [OK]
>  Running windows_h_VS_2008  [OK]
>  Running windows_h_VS_2010  [OK]
>  Running windows_h_VS_2012  [OK]
>
>All tests were successful, 2 tests skipped
>make[1]: Leaving directory `/home/root/rpmbuild/BUILD/cbmc-4.7/regression/cpp'
>+ exit 0
>Processing files: cbmc-4.7-2.fc21.ppc64le
>Executing(%doc): /bin/sh -e /home/root/rpmbuild/tmp/rpm-tmp.yLUn0a
>+ umask 022
>+ cd /home/root/rpmbuild/BUILD
>+ cd cbmc-4.7
>+ DOCDIR=/home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/share/doc/cbmc
>+ export DOCDIR
>+ /usr/bin/mkdir -p /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/share/doc/cbmc
>+ cp -pr CHANGELOG /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/share/doc/cbmc
>+ cp -pr LICENSE /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/share/doc/cbmc
>+ cp -pr doc/guide/CBMC-guide.pdf /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/share/doc/cbmc
>+ cp -pr doc/html-manual /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le/usr/share/doc/cbmc
>+ exit 0
>Provides: cbmc = 4.7-2.fc21 cbmc(ppc-64) = 4.7-2.fc21
>Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
>Requires: libc.so.6()(64bit) libc.so.6(GLIBC_2.17)(64bit) libcudd.so.2()(64bit) libcuddobj.so.2()(64bit) libdddmp.so.2()(64bit) libgcc_s.so.1()(64bit) libgcc_s.so.1(GCC_3.0)(64bit) libm.so.6()(64bit) libm.so.6(GLIBC_2.17)(64bit) libminisat.so.2()(64bit) libstdc++.so.6()(64bit) libstdc++.so.6(CXXABI_1.3)(64bit) libstdc++.so.6(CXXABI_1.3.1)(64bit) libstdc++.so.6(GLIBCXX_3.4)(64bit) libstdc++.so.6(GLIBCXX_3.4.10)(64bit) libstdc++.so.6(GLIBCXX_3.4.11)(64bit) libstdc++.so.6(GLIBCXX_3.4.15)(64bit) libstdc++.so.6(GLIBCXX_3.4.20)(64bit) libstdc++.so.6(GLIBCXX_3.4.9)(64bit) rtld(GNU_HASH)
>Processing files: cbmc-debuginfo-4.7-2.fc21.ppc64le
>Provides: cbmc-debuginfo = 4.7-2.fc21 cbmc-debuginfo(ppc-64) = 4.7-2.fc21
>Requires(rpmlib): rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 rpmlib(CompressedFileNames) <= 3.0.4-1
>Checking for unpackaged file(s): /usr/lib/rpm/check-files /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le
>Wrote: /ppc64le/stage2/SRPMS/cbmc-4.7-2.fc21.src.rpm
>Wrote: /ppc64le/stage2/RPMS/ppc64le/cbmc-4.7-2.fc21.ppc64le.rpm
>Wrote: /ppc64le/stage2/RPMS/ppc64le/cbmc-debuginfo-4.7-2.fc21.ppc64le.rpm
>Executing(%clean): /bin/sh -e /home/root/rpmbuild/tmp/rpm-tmp.zEBkOr
>+ umask 022
>+ cd /home/root/rpmbuild/BUILD
>+ cd cbmc-4.7
>+ /usr/bin/rm -rf /home/root/rpmbuild/BUILDROOT/cbmc-4.7-2.fc21.ppc64le
>+ exit 0

Actions: View

Attachments on bug 1133066: 929685 | 929686