g++ --static -o cbmc \
      bmc.o \
      bv_cbmc.o \
      cbmc_sat.o \
      counterexample_beautification_greedy.o \
      counterexample_beautification_pbs.o \
      cvc.o \
      dimacs.o \
      document_subgoals.o \
      main.o \
      parseoptions.o \
      pretty_names.o \
      symex_bmc.o \
      ../infrules/infrule.o \
      ../intrep/intrep.o \
      ../big-int/bigint.o \
      ../langapi/csp_dummy.o \
      ../langapi/pvs_dummy.o \
      ../langapi/bplang_dummy.o \
      ../langapi/smvlang_dummy.o \
      ../langapi/vhdl_dummy.o \
      ../langapi/promela_dummy.o \
      ../langapi/pascal_dummy.o \
      ../langapi/netlist_dummy.o \
      ../langapi/xmllang_dummy.o \
      ../langapi/verilog_dummy.o \
      ../langapi/cpp_dummy.o \
      ../langapi/specc_dummy.o \
      ../langapi/simplifylang_dummy.o \
      ../langapi/cvclang_dummy.o \
      ../langapi/csharp_dummy.o \
      ../../ctool/src/context.o \
      ../../ctool/src/decl.o \
      ../../ctool/src/express.o \
      ../../ctool/src/gram.o \
      ../../ctool/src/lexer.o \
      ../../ctool/src/location.o \
      ../../ctool/src/parseenv.o \
      ../../ctool/src/project.o \
      ../../ctool/src/stemnt.o \
      ../../ctool/src/symbol.o \
      ../../ctool/src/token.o \
      ../../zChaff/libsat.a \
      ../ansi-c/c_code.o \
      ../ansi-c/c_expr.o \
      ../ansi-c/c_final.o \
      ../ansi-c/c_sequent.o \
      ../ansi-c/ansi_c_language.o \
      ../ansi-c/c_link.o \
      ../ansi-c/codegen.o \
      ../ansi-c/convert-c.o \
      ../ansi-c/c_sizeof.o \
      ../ansi-c/c_typecast.o \
      ../ansi-c/c_typecheck_base.o \
      ../ansi-c/c_typecheck_code.o \
      ../ansi-c/c_typecheck_expr.o \
      ../ansi-c/c_typecheck_initializer.o \
      ../ansi-c/c_typecheck_type.o \
      ../ansi-c/c_typecheck_typecast.o \
      ../ansi-c/c_type.o \
      ../ansi-c/c_types.o \
      ../ansi-c/c_preprocess.o \
      ../ansi-c/expr2c.o \
      ../ansi-c/global_init.o \
      ../ansi-c/trans_unit.o \
      ../symex/nondet_symbols.o \
      ../symex/symex_assign.o \
      ../symex/symex_check.o \
      ../symex/symex_clean_expr.o \
      ../symex/symex_decl.o \
      ../symex/symex_equation.o \
      ../symex/symex_equation_container.o \
      ../symex/symex_function.o \
      ../symex/symex_goto.o \
      ../symex/symex_ifthenelse.o \
      ../symex/symex_label.o \
      ../symex/symex_loops.o \
      ../symex/symex_main.o \
      ../symex/symex_pointer.o \
      ../symex/symex_remove_sideeffects.o \
      ../symex/symex_sideeffect.o \
      ../symex/symex_switch.o \
      ../langapi/api.o \
      ../langapi/language_ui.o \
      ../langapi/languages.o \
      ../langapi/mode.o \
      ../propdec/boolbv.o \
      ../propdec/boolbv_add_sub.o \
      ../propdec/boolbv_bitwise.o \
      ../propdec/boolbv_bv_rel.o \
      ../propdec/boolbv_byte_extract.o \
      ../propdec/boolbv_case.o \
      ../propdec/boolbv_concatenation.o \
      ../propdec/boolbv_cond.o \
      ../propdec/boolbv_constant.o \
      ../propdec/boolbv_div.o \
      ../propdec/boolbv_equality.o \
      ../propdec/boolbv_extractbit.o \
      ../propdec/boolbv_extractbits.o \
      ../propdec/boolbv_get.o \
      ../propdec/boolbv_if.o \
      ../propdec/boolbv_index.o \
      ../propdec/boolbv_member.o \
      ../propdec/boolbv_mod.o \
      ../propdec/boolbv_mult.o \
      ../propdec/boolbv_overflow.o \
      ../propdec/boolbv_reduction.o \
      ../propdec/boolbv_replication.o \
      ../propdec/boolbv_shift.o \
      ../propdec/boolbv_typecast.o \
      ../propdec/boolbv_width.o \
      ../propdec/boolbv_with.o \
      ../propdec/bv_pointers.o \
      ../propdec/bv_utils.o \
      ../propdec/cnf.o \
      ../propdec/congruence_closure.o \
      ../propdec/cvc_conv.o \
      ../propdec/cvc_prop.o \
      ../propdec/dimacs_cnf.o \
      ../propdec/equality.o \
      ../propdec/functions.o \
      ../propdec/pbs_dimacs_cnf.o \
      ../propdec/prop_conv.o \
      ../propdec/prop.o \
      ../propdec/satcheck_zchaff.o \
      ../propdec/satcheck_limmat.o \
      ../../limmat/liblimmat.a \
      ../util/actuals.o \
      ../util/arith_tools.o \
      ../util/array_name.o \
      ../util/base_type.o \
      ../util/bitvector.o \
      ../util/c_misc.o \
      ../util/cmdline.o \
      ../util/cnf_simplify.o \
      ../util/code_utils.o \
      ../util/config.o \
      ../util/context.o \
      ../util/err_stream.o \
      ../util/expr.o \
      ../util/expr_util.o \
      ../util/find_symbols.o \
      ../util/get_module.o \
      ../util/guard.o \
      ../util/h_sequent.o \
      ../util/i2string.o \
      ../util/identifier.o \
      ../util/irep.o \
      ../util/language_file.o \
      ../util/language.o \
      ../util/lispexpr.o \
      ../util/lispirep.o \
      ../util/location.o \
      ../util/map_util.o \
      ../util/message.o \
      ../util/mp_arith.o \
      ../util/namespace.o \
      ../util/options.o \
      ../util/parseoptions.o \
      ../util/parser.o \
      ../util/rename.o \
      ../util/replace_expr.o \
      ../util/replace_symbol.o \
      ../util/sequent.o \
      ../util/simplify.o \
      ../util/simplify_expr.o \
      ../util/simplify_utils.o \
      ../util/str_getline.o \
      ../util/string2array.o \
      ../util/stringdb.o \
      ../util/string_hash.o \
      ../util/strstream2string.o \
      ../util/symbol.o \
      ../util/threeval.o \
      ../util/time_stopping.o \
      ../util/typecheck.o \
      ../util/type.o \
      ../util/type_eq.o \
      ../util/ui_message.o
