Compiling Enumerative solver returns errors

After "make distclean" and "make eopt" commands, this is the full console output:

`[DEP:esolver] Z3TheoremProver.cpp [DEP:esolver] Z3Objects.cpp [DEP:esolver] ValueManager.cpp [DEP:esolver] UserExpression.cpp [DEP:esolver] UIDGenerator.cpp [DEP:esolver] TypeManager.cpp [DEP:esolver] TimeValue.cpp [DEP:esolver] TheoremProver.cpp [DEP:esolver] SynthLib2Solver.cpp [DEP:esolver] SymPartitionGenerator.cpp [DEP:esolver] SpookyHash.cpp [DEP:esolver] SpecRewriter.cpp [DEP:esolver] Signature.cpp [DEP:esolver] ScopeManager.cpp [DEP:esolver] ResourceLimitManager.cpp [DEP:esolver] PartitionGenerator.cpp [DEP:esolver] Operators.cpp [DEP:esolver] MemStats.cpp [DEP:esolver] Logger.cpp [DEP:esolver] LIALogic.cpp [DEP:esolver] Indent.cpp [DEP:esolver] GrammarNodes.cpp [DEP:esolver] Grammar.cpp [DEP:esolver] GenExpression.cpp [DEP:esolver] Gatherers.cpp [DEP:esolver] GNCostPair.cpp [DEP:esolver] FunctorBase.cpp [DEP:esolver] ExpressionVisitorBase.cpp [DEP:esolver] ExprManager.cpp [DEP:esolver] ExpCheckers.cpp [DEP:esolver] EvalRule.cpp [DEP:esolver] EnumeratorBase.cpp [DEP:esolver] ESolverScope.cpp [DEP:esolver] ESolverLogic.cpp [DEP:esolver] ESolver.cpp [DEP:esolver] ESType.cpp [DEP:esolver] ESException.cpp [DEP:esolver] CrossProductGenerator.cpp [DEP:esolver] ConstManager.cpp [DEP:esolver] ConcreteValueBase.cpp [DEP:esolver] ConcreteEvaluator.cpp [DEP:esolver] CFGEnumerator.cpp [DEP:esolver] CEGSolver.cpp [DEP:esolver] Builtins.cpp [DEP:esolver] BVLogic.cpp [CXX:esolver] BVLogic.cpp --> BVLogic.o [CXX:esolver] Builtins.cpp --> Builtins.o [CXX:esolver] CEGSolver.cpp --> CEGSolver.o [CXX:esolver] CFGEnumerator.cpp --> CFGEnumerator.o [CXX:esolver] ConcreteEvaluator.cpp --> ConcreteEvaluator.o [CXX:esolver] ConcreteValueBase.cpp --> ConcreteValueBase.o [CXX:esolver] ConstManager.cpp --> ConstManager.o [CXX:esolver] CrossProductGenerator.cpp --> CrossProductGenerator.o [CXX:esolver] ESException.cpp --> ESException.o [CXX:esolver] ESType.cpp --> ESType.o [CXX:esolver] ESolver.cpp --> ESolver.o [CXX:esolver] ESolverLogic.cpp --> ESolverLogic.o [CXX:esolver] ESolverScope.cpp --> ESolverScope.o [CXX:esolver] EnumeratorBase.cpp --> EnumeratorBase.o [CXX:esolver] EvalRule.cpp --> EvalRule.o [CXX:esolver] ExpCheckers.cpp --> ExpCheckers.o [CXX:esolver] ExprManager.cpp --> ExprManager.o [CXX:esolver] ExpressionVisitorBase.cpp --> ExpressionVisitorBase.o [CXX:esolver] FunctorBase.cpp --> FunctorBase.o [CXX:esolver] GNCostPair.cpp --> GNCostPair.o [CXX:esolver] Gatherers.cpp --> Gatherers.o [CXX:esolver] GenExpression.cpp --> GenExpression.o [CXX:esolver] Grammar.cpp --> Grammar.o [CXX:esolver] GrammarNodes.cpp --> GrammarNodes.o [CXX:esolver] Indent.cpp --> Indent.o [CXX:esolver] LIALogic.cpp --> LIALogic.o [CXX:esolver] Logger.cpp --> Logger.o [CXX:esolver] MemStats.cpp --> MemStats.o [CXX:esolver] Operators.cpp --> Operators.o [CXX:esolver] PartitionGenerator.cpp --> PartitionGenerator.o [CXX:esolver] ResourceLimitManager.cpp --> ResourceLimitManager.o [CXX:esolver] ScopeManager.cpp --> ScopeManager.o [CXX:esolver] Signature.cpp --> Signature.o [CXX:esolver] SpecRewriter.cpp --> SpecRewriter.o [CXX:esolver] SpookyHash.cpp --> SpookyHash.o [CXX:esolver] SymPartitionGenerator.cpp --> SymPartitionGenerator.o [CXX:esolver] SynthLib2Solver.cpp --> SynthLib2Solver.o [CXX:esolver] TheoremProver.cpp --> TheoremProver.o [CXX:esolver] TimeValue.cpp --> TimeValue.o [CXX:esolver] TypeManager.cpp --> TypeManager.o [CXX:esolver] UIDGenerator.cpp --> UIDGenerator.o [CXX:esolver] UserExpression.cpp --> UserExpression.o [CXX:esolver] ValueManager.cpp --> ValueManager.o [CXX:esolver] Z3Objects.cpp --> Z3Objects.o [CXX:esolver] Z3TheoremProver.cpp --> Z3TheoremProver.o [AR:esolver] libesolver.a [LD:esolver] libesolver.so make eopt -C /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/synthlib2parser make[1]: Entering directory '/home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/synthlib2parser' [DEP:synthlib2parser] PrintVisitor.cpp [DEP:synthlib2parser] SynthLib2ParserExceptions.cpp [DEP:synthlib2parser] SynthLib2ParserAST.cpp [bison:synthlib2parser] SynthLib2Parser.y --> SynthLib2Parser.tab.cpp [CXX:synthlib2parser] SynthLib2Parser.tab.cpp --> SynthLib2Parser.tab.o src/SynthLib2Parser.tab.cpp: In function ‘int yyparse()’: src/SynthLib2Parser.tab.cpp:2161:35: warning: ISO C++ forbids converting a string constant to ‘char’ [-Wpedantic] yyerror (YY_("syntax error")); ^ src/SynthLib2Parser.tab.cpp:2305:35: warning: ISO C++ forbids converting a string constant to ‘char’ [-Wpedantic] yyerror (YY_("memory exhausted")); ^ [flex:synthlib2parser] SynthLib2Lexer.l --> SynthLib2Lexer.cpp [CXX:synthlib2parser] SynthLib2Lexer.cpp --> SynthLib2Lexer.o src/SynthLib2Lexer.cpp: In function ‘int yy_get_next_buffer()’: src/SynthLib2Lexer.cpp:1360:44: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] if ((int) ((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_s ^ [CXX:synthlib2parser] SynthLib2ParserAST.cpp --> SynthLib2ParserAST.o [CXX:synthlib2parser] SynthLib2ParserExceptions.cpp --> SynthLib2ParserExceptions.o [CXX:synthlib2parser] PrintVisitor.cpp --> PrintVisitor.o [AR:synthlib2parser] libsynthlib2parser.a [LD:synthlib2parser] libsynthlib2parser.so make[1]: Leaving directory '/home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/synthlib2parser' cp /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/synthlib2parser/lib/opt/libsynthlib2parser.so \ /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/synthlib2parser/lib/opt/libsynthlib2parser.a \ /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/lib/opt touch /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/lib/opt/slparserlib.ph [DEP:esolver] ESolverSynthLib.cpp [CXX:esolver] ESolverSynthLib.cpp --> ESolverSynthLib.o cd /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/z3-4.3.1; \ autoconf; \ ./configure; \ python scripts/mk_make.py; \ cd build; \ make; \ touch /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/z3-4.3.1/build/z3build.ph checking for g++... g++ checking whether we are using the GNU C++ compiler... no checking whether g++ accepts -g... no checking for gcc... gcc checking whether we are using the GNU C compiler... no checking whether gcc accepts -g... no checking for gcc option to accept ISO C89... unsupported checking whether make sets $(MAKE)... yes checking for grep that handles long lines and -e... /bin/grep checking for a sed that does not truncate output... /bin/sed checking size of int *... 8 configure: creating ./config.status config.status: creating scripts/config-debug.mk config.status: creating scripts/config-release.mk Z3 was configured with success. Host platform: linux Compiler: g++ Arithmetic: internal Python: python Prefix: /usr 64-bit: yes

To build and install Z3, execute: python scripts/mk_make.py cd build make sudo make install Fixing end of line... New component: 'util' New component: 'polynomial' New component: 'sat' New component: 'nlsat' New component: 'interval' New component: 'subpaving' New component: 'ast' New component: 'rewriter' New component: 'model' New component: 'tactic' New component: 'substitution' New component: 'parser_util' New component: 'grobner' New component: 'euclid' New component: 'front_end_params' New component: 'simplifier' New component: 'normal_forms' New component: 'core_tactics' New component: 'sat_tactic' New component: 'arith_tactics' New component: 'nlsat_tactic' New component: 'subpaving_tactic' New component: 'aig_tactic' New component: 'solver' New component: 'cmd_context' New component: 'extra_cmds' New component: 'smt2parser' New component: 'pattern' New component: 'macros' New component: 'proof_checker' New component: 'bit_blaster' New component: 'proto_model' New component: 'smt' New component: 'user_plugin' New component: 'bv_tactics' New component: 'fuzzing' New component: 'fpa' New component: 'smt_tactic' New component: 'sls_tactic' New component: 'muz_qe' New component: 'smtlogic_tactics' New component: 'ufbv_tactic' New component: 'portfolio' New component: 'smtparser' New component: 'api' New component: 'shell' New component: 'test' New component: 'api_dll' New component: 'api_static_lib' New component: 'dotnet' New component: 'cpp' Python bindinds directory was detected. New component: 'cpp_example' New component: 'c_example' New component: 'maxsat' New component: 'dotnet_example' New component: 'py_example' Generated 'src/util/version.h' Updated 'src/api/dotnet/Properties/AssemblyInfo.cs' Generated 'src/ast/pattern/database.h' Generated 'src/shell/install_tactic.cpp' Generated 'src/test/install_tactic.cpp' Generated 'src/api/dll/install_tactic.cpp' Generated 'src/api/staticlib/install_tactic.cpp' Generated 'src/api/python/z3consts.py' Generated 'src/api/dotnet/Enumerations.cs' Generated 'src/api/api_log_macros.h' Generated 'src/api/api_log_macros.cpp' Generated 'src/api/api_commands.cpp' Generated 'src/api/python/z3core.py' Generated 'src/api/dotnet/Native.cs' Listing src/api/python ... Compiling src/api/python/z3.py ... Compiling src/api/python/z3consts.py ... Compiling src/api/python/z3core.py ... Compiling src/api/python/z3printer.py ... Compiling src/api/python/z3test.py ... Compiling src/api/python/z3types.py ... Generated 'z3consts.pyc' Generated 'z3types.pyc' Generated 'z3test.pyc' Generated 'z3printer.pyc' Generated 'z3core.pyc' Generated 'z3.pyc' Writing build/Makefile Copied Z3Py example 'example.py' to 'build' Makefile was successfully generated. python packages dir: /usr/lib/python2.7/dist-packages compilation mode: Release Type 'cd build; make' to build Z3 make[1]: Entering directory '/home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/z3-4.3.1/build' src/shell/datalog_frontend.cpp --> shell/datalog_frontend-lto.o src/shell/z3_log_frontend.cpp --> shell/z3_log_frontend-lto.o src/shell/main.cpp --> shell/main-lto.o src/shell/install_tactic.cpp --> shell/install_tactic-lto.o src/shell/dimacs_frontend.cpp --> shell/dimacs_frontend-lto.o src/shell/smtlib_frontend.cpp --> shell/smtlib_frontend-lto.o src/api/api_datalog.cpp --> api/api_datalog-lto.o src/api/api_tactic.cpp --> api/api_tactic-lto.o src/api/api_goal.cpp --> api/api_goal-lto.o src/api/api_ast.cpp --> api/api_ast-lto.o src/api/api_bv.cpp --> api/api_bv-lto.o src/api/api_commands.cpp --> api/api_commands-lto.o src/api/api_ast_map.cpp --> api/api_ast_map-lto.o src/api/api_ast_vector.cpp --> api/api_ast_vector-lto.o src/api/api_context.cpp --> api/api_context-lto.o src/api/api_solver.cpp --> api/api_solver-lto.o src/api/api_log_macros.cpp --> api/api_log_macros-lto.o src/api/api_config_params.cpp --> api/api_config_params-lto.o src/api/api_quant.cpp --> api/api_quant-lto.o src/api/api_user_theory.cpp --> api/api_user_theory-lto.o src/api/api_parsers.cpp --> api/api_parsers-lto.o src/api/api_arith.cpp --> api/api_arith-lto.o src/api/api_numeral.cpp --> api/api_numeral-lto.o src/api/api_stats.cpp --> api/api_stats-lto.o src/api/api_datatype.cpp --> api/api_datatype-lto.o src/api/z3_replayer.cpp --> api/z3_replayer-lto.o src/api/api_params.cpp --> api/api_params-lto.o src/api/api_solver_old.cpp --> api/api_solver_old-lto.o src/api/api_log.cpp --> api/api_log-lto.o src/api/api_model.cpp --> api/api_model-lto.o src/api/api_array.cpp --> api/api_array-lto.o api/api-lto.a ar: api/api_datalog-lto.o: plugin needed to handle lto object ar: api/api_tactic-lto.o: plugin needed to handle lto object ar: api/api_goal-lto.o: plugin needed to handle lto object ar: api/api_ast-lto.o: plugin needed to handle lto object ar: api/api_bv-lto.o: plugin needed to handle lto object ar: api/api_commands-lto.o: plugin needed to handle lto object ar: api/api_ast_map-lto.o: plugin needed to handle lto object ar: api/api_ast_vector-lto.o: plugin needed to handle lto object ar: api/api_context-lto.o: plugin needed to handle lto object ar: api/api_solver-lto.o: plugin needed to handle lto object ar: api/api_log_macros-lto.o: plugin needed to handle lto object ar: api/api_config_params-lto.o: plugin needed to handle lto object ar: api/api_quant-lto.o: plugin needed to handle lto object ar: api/api_user_theory-lto.o: plugin needed to handle lto object ar: api/api_parsers-lto.o: plugin needed to handle lto object ar: api/api_arith-lto.o: plugin needed to handle lto object ar: api/api_numeral-lto.o: plugin needed to handle lto object ar: api/api_stats-lto.o: plugin needed to handle lto object ar: api/api_datatype-lto.o: plugin needed to handle lto object ar: api/z3_replayer-lto.o: plugin needed to handle lto object ar: api/api_params-lto.o: plugin needed to handle lto object ar: api/api_solver_old-lto.o: plugin needed to handle lto object ar: api/api_log-lto.o: plugin needed to handle lto object ar: api/api_model-lto.o: plugin needed to handle lto object ar: api/api_array-lto.o: plugin needed to handle lto object src/parsers/smt/smtlib_solver.cpp --> parsers/smt/smtlib_solver-lto.o src/parsers/smt/smtlib.cpp --> parsers/smt/smtlib-lto.o src/parsers/smt/smtparser.cpp --> parsers/smt/smtparser-lto.o parsers/smt/smtparser-lto.a ar: parsers/smt/smtlib_solver-lto.o: plugin needed to handle lto object ar: parsers/smt/smtlib-lto.o: plugin needed to handle lto object ar: parsers/smt/smtparser-lto.o: plugin needed to handle lto object src/tactic/portfolio/default_tactic.cpp --> tactic/portfolio/default_tactic-lto.o src/tactic/portfolio/smt_strategic_solver.cpp --> tactic/portfolio/smt_strategic_solver-lto.o tactic/portfolio/portfolio-lto.a ar: tactic/portfolio/default_tactic-lto.o: plugin needed to handle lto object ar: tactic/portfolio/smt_strategic_solver-lto.o: plugin needed to handle lto object src/tactic/ufbv/ufbv_rewriter_tactic.cpp --> tactic/ufbv/ufbv_rewriter_tactic-lto.o src/tactic/ufbv/ufbv_rewriter.cpp --> tactic/ufbv/ufbv_rewriter-lto.o src/tactic/ufbv/ufbv_tactic.cpp --> tactic/ufbv/ufbv_tactic-lto.o src/tactic/ufbv/quasi_macros_tactic.cpp --> tactic/ufbv/quasi_macros_tactic-lto.o src/tactic/ufbv/macro_finder_tactic.cpp --> tactic/ufbv/macro_finder_tactic-lto.o tactic/ufbv/ufbv_tactic-lto.a ar: tactic/ufbv/ufbv_rewriter_tactic-lto.o: plugin needed to handle lto object ar: tactic/ufbv/ufbv_rewriter-lto.o: plugin needed to handle lto object ar: tactic/ufbv/ufbv_tactic-lto.o: plugin needed to handle lto object ar: tactic/ufbv/quasi_macros_tactic-lto.o: plugin needed to handle lto object ar: tactic/ufbv/macro_finder_tactic-lto.o: plugin needed to handle lto object src/tactic/smtlogics/qfauflia_tactic.cpp --> tactic/smtlogics/qfauflia_tactic-lto.o src/tactic/smtlogics/quant_tactics.cpp --> tactic/smtlogics/quant_tactics-lto.o src/tactic/smtlogics/qfbv_tactic.cpp --> tactic/smtlogics/qfbv_tactic-lto.o src/tactic/smtlogics/qflia_tactic.cpp --> tactic/smtlogics/qflia_tactic-lto.o src/tactic/smtlogics/qfnia_tactic.cpp --> tactic/smtlogics/qfnia_tactic-lto.o src/tactic/smtlogics/qflra_tactic.cpp --> tactic/smtlogics/qflra_tactic-lto.o src/tactic/smtlogics/qfufbv_tactic.cpp --> tactic/smtlogics/qfufbv_tactic-lto.o src/tactic/smtlogics/qfaufbv_tactic.cpp --> tactic/smtlogics/qfaufbv_tactic-lto.o src/tactic/smtlogics/nra_tactic.cpp --> tactic/smtlogics/nra_tactic-lto.o src/tactic/smtlogics/qfidl_tactic.cpp --> tactic/smtlogics/qfidl_tactic-lto.o src/tactic/smtlogics/qfuf_tactic.cpp --> tactic/smtlogics/qfuf_tactic-lto.o src/tactic/smtlogics/qfnra_tactic.cpp --> tactic/smtlogics/qfnra_tactic-lto.o tactic/smtlogics/smtlogic_tactics-lto.a ar: tactic/smtlogics/qfauflia_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/quant_tactics-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfbv_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qflia_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfnia_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qflra_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfufbv_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfaufbv_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/nra_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfidl_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfuf_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfnra_tactic-lto.o: plugin needed to handle lto object src/muz_qe/dl_skip_table.cpp --> muz_qe/dl_skip_table-lto.o src/muz_qe/qe_sat_tactic.cpp --> muz_qe/qe_sat_tactic-lto.o src/muz_qe/dl_rule.cpp --> muz_qe/dl_rule-lto.o src/muz_qe/dl_costs.cpp --> muz_qe/dl_costs-lto.o src/muz_qe/dl_cmds.cpp --> muz_qe/dl_cmds-lto.o src/muz_qe/imdd.cpp --> muz_qe/imdd-lto.o src/muz_qe/dl_mk_simple_joins.cpp --> muz_qe/dl_mk_simple_joins-lto.o src/muz_qe/vsubst_tactic.cpp --> muz_qe/vsubst_tactic-lto.o src/muz_qe/dl_interval_relation.cpp --> muz_qe/dl_interval_relation-lto.o src/muz_qe/dl_mk_unbound_compressor.cpp --> muz_qe/dl_mk_unbound_compressor-lto.o src/muz_qe/qe_dl_plugin.cpp --> muz_qe/qe_dl_plugin-lto.o src/muz_qe/dl_mk_coalesce.cpp --> muz_qe/dl_mk_coalesce-lto.o src/muz_qe/proof_utils.cpp --> muz_qe/proof_utils-lto.o src/muz_qe/qe_bv_plugin.cpp --> muz_qe/qe_bv_plugin-lto.o src/muz_qe/dl_util.cpp --> muz_qe/dl_util-lto.o src/muz_qe/dl_mk_explanations.cpp --> muz_qe/dl_mk_explanations-lto.o src/muz_qe/dl_mk_rule_inliner.cpp --> muz_qe/dl_mk_rule_inliner-lto.o src/muz_qe/dl_rule_transformer.cpp --> muz_qe/dl_rule_transformer-lto.o src/muz_qe/dl_mk_magic_sets.cpp --> muz_qe/dl_mk_magic_sets-lto.o src/muz_qe/model2expr.cpp --> muz_qe/model2expr-lto.o src/muz_qe/arith_bounds_tactic.cpp --> muz_qe/arith_bounds_tactic-lto.o src/muz_qe/dl_mk_partial_equiv.cpp --> muz_qe/dl_mk_partial_equiv-lto.o src/muz_qe/qe.cpp --> muz_qe/qe-lto.o src/muz_qe/dl_mk_unfold.cpp --> muz_qe/dl_mk_unfold-lto.o src/muz_qe/dl_mk_bit_blast.cpp --> muz_qe/dl_mk_bit_blast-lto.o src/muz_qe/dl_sieve_relation.cpp --> muz_qe/dl_sieve_relation-lto.o src/muz_qe/qe_bool_plugin.cpp --> muz_qe/qe_bool_plugin-lto.o src/muz_qe/datalog_parser.cpp --> muz_qe/datalog_parser-lto.o src/muz_qe/dl_rule_set.cpp --> muz_qe/dl_rule_set-lto.o src/muz_qe/dl_mk_subsumption_checker.cpp --> muz_qe/dl_mk_subsumption_checker-lto.o src/muz_qe/dl_bound_relation.cpp --> muz_qe/dl_bound_relation-lto.o src/muz_qe/pdr_prop_solver.cpp --> muz_qe/pdr_prop_solver-lto.o src/muz_qe/nlarith_util.cpp --> muz_qe/nlarith_util-lto.o src/muz_qe/replace_proof_converter.cpp --> muz_qe/replace_proof_converter-lto.o src/muz_qe/dl_instruction.cpp --> muz_qe/dl_instruction-lto.o src/muz_qe/dl_base.cpp --> muz_qe/dl_base-lto.o src/muz_qe/dl_table.cpp --> muz_qe/dl_table-lto.o src/muz_qe/dl_bmc_engine.cpp --> muz_qe/dl_bmc_engine-lto.o src/muz_qe/qe_datatype_plugin.cpp --> muz_qe/qe_datatype_plugin-lto.o src/muz_qe/dl_mk_filter_rules.cpp --> muz_qe/dl_mk_filter_rules-lto.o src/muz_qe/dl_table_relation.cpp --> muz_qe/dl_table_relation-lto.o src/muz_qe/dl_relation_manager.cpp --> muz_qe/dl_relation_manager-lto.o src/muz_qe/qe_lite.cpp --> muz_qe/qe_lite-lto.o src/muz_qe/dl_mk_slice.cpp --> muz_qe/dl_mk_slice-lto.o src/muz_qe/horn_subsume_model_converter.cpp --> muz_qe/horn_subsume_model_converter-lto.o src/muz_qe/qe_arith_plugin.cpp --> muz_qe/qe_arith_plugin-lto.o src/muz_qe/dl_mk_coi_filter.cpp --> muz_qe/dl_mk_coi_filter-lto.o src/muz_qe/dl_finite_product_relation.cpp --> muz_qe/dl_finite_product_relation-lto.o src/muz_qe/pdr_quantifiers.cpp --> muz_qe/pdr_quantifiers-lto.o src/muz_qe/dl_context.cpp --> muz_qe/dl_context-lto.o src/muz_qe/dl_compiler.cpp --> muz_qe/dl_compiler-lto.o src/muz_qe/pdr_dl_interface.cpp --> muz_qe/pdr_dl_interface-lto.o src/muz_qe/dl_smt_relation.cpp --> muz_qe/dl_smt_relation-lto.o src/muz_qe/pdr_reachable_cache.cpp --> muz_qe/pdr_reachable_cache-lto.o src/muz_qe/dl_rule_subsumption_index.cpp --> muz_qe/dl_rule_subsumption_index-lto.o src/muz_qe/pdr_context.cpp --> muz_qe/pdr_context-lto.o src/muz_qe/qe_cmd.cpp --> muz_qe/qe_cmd-lto.o src/muz_qe/dl_external_relation.cpp --> muz_qe/dl_external_relation-lto.o src/muz_qe/dl_product_relation.cpp --> muz_qe/dl_product_relation-lto.o src/muz_qe/dl_check_table.cpp --> muz_qe/dl_check_table-lto.o src/muz_qe/pdr_sym_mux.cpp --> muz_qe/pdr_sym_mux-lto.o src/muz_qe/qe_array_plugin.cpp --> muz_qe/qe_array_plugin-lto.o src/muz_qe/dl_mk_similarity_compressor.cpp --> muz_qe/dl_mk_similarity_compressor-lto.o src/muz_qe/pdr_smt_context_manager.cpp --> muz_qe/pdr_smt_context_manager-lto.o src/muz_qe/dl_mk_interp_tail_simplifier.cpp --> muz_qe/dl_mk_interp_tail_simplifier-lto.o src/muz_qe/pdr_util.cpp --> muz_qe/pdr_util-lto.o src/muz_qe/pdr_generalizers.cpp --> muz_qe/pdr_generalizers-lto.o src/muz_qe/unit_subsumption_tactic.cpp --> muz_qe/unit_subsumption_tactic-lto.o src/muz_qe/pdr_farkas_learner.cpp --> muz_qe/pdr_farkas_learner-lto.o src/muz_qe/pdr_interpolant_provider.cpp --> muz_qe/pdr_interpolant_provider-lto.o src/muz_qe/qe_tactic.cpp --> muz_qe/qe_tactic-lto.o src/muz_qe/pdr_manager.cpp --> muz_qe/pdr_manager-lto.o src/muz_qe/dl_sparse_table.cpp --> muz_qe/dl_sparse_table-lto.o muz_qe/muz_qe-lto.a ar: muz_qe/dl_skip_table-lto.o: plugin needed to handle lto object ar: muz_qe/qe_sat_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/dl_rule-lto.o: plugin needed to handle lto object ar: muz_qe/dl_costs-lto.o: plugin needed to handle lto object ar: muz_qe/dl_cmds-lto.o: plugin needed to handle lto object ar: muz_qe/imdd-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_simple_joins-lto.o: plugin needed to handle lto object ar: muz_qe/vsubst_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/dl_interval_relation-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_unbound_compressor-lto.o: plugin needed to handle lto object ar: muz_qe/qe_dl_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_coalesce-lto.o: plugin needed to handle lto object ar: muz_qe/proof_utils-lto.o: plugin needed to handle lto object ar: muz_qe/qe_bv_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_util-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_explanations-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_rule_inliner-lto.o: plugin needed to handle lto object ar: muz_qe/dl_rule_transformer-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_magic_sets-lto.o: plugin needed to handle lto object ar: muz_qe/model2expr-lto.o: plugin needed to handle lto object ar: muz_qe/arith_bounds_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_partial_equiv-lto.o: plugin needed to handle lto object ar: muz_qe/qe-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_unfold-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_bit_blast-lto.o: plugin needed to handle lto object ar: muz_qe/dl_sieve_relation-lto.o: plugin needed to handle lto object ar: muz_qe/qe_bool_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/datalog_parser-lto.o: plugin needed to handle lto object ar: muz_qe/dl_rule_set-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_subsumption_checker-lto.o: plugin needed to handle lto object ar: muz_qe/dl_bound_relation-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_prop_solver-lto.o: plugin needed to handle lto object ar: muz_qe/nlarith_util-lto.o: plugin needed to handle lto object ar: muz_qe/replace_proof_converter-lto.o: plugin needed to handle lto object ar: muz_qe/dl_instruction-lto.o: plugin needed to handle lto object ar: muz_qe/dl_base-lto.o: plugin needed to handle lto object ar: muz_qe/dl_table-lto.o: plugin needed to handle lto object ar: muz_qe/dl_bmc_engine-lto.o: plugin needed to handle lto object ar: muz_qe/qe_datatype_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_filter_rules-lto.o: plugin needed to handle lto object ar: muz_qe/dl_table_relation-lto.o: plugin needed to handle lto object ar: muz_qe/dl_relation_manager-lto.o: plugin needed to handle lto object ar: muz_qe/qe_lite-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_slice-lto.o: plugin needed to handle lto object ar: muz_qe/horn_subsume_model_converter-lto.o: plugin needed to handle lto object ar: muz_qe/qe_arith_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_coi_filter-lto.o: plugin needed to handle lto object ar: muz_qe/dl_finite_product_relation-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_quantifiers-lto.o: plugin needed to handle lto object ar: muz_qe/dl_context-lto.o: plugin needed to handle lto object ar: muz_qe/dl_compiler-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_dl_interface-lto.o: plugin needed to handle lto object ar: muz_qe/dl_smt_relation-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_reachable_cache-lto.o: plugin needed to handle lto object ar: muz_qe/dl_rule_subsumption_index-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_context-lto.o: plugin needed to handle lto object ar: muz_qe/qe_cmd-lto.o: plugin needed to handle lto object ar: muz_qe/dl_external_relation-lto.o: plugin needed to handle lto object ar: muz_qe/dl_product_relation-lto.o: plugin needed to handle lto object ar: muz_qe/dl_check_table-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_sym_mux-lto.o: plugin needed to handle lto object ar: muz_qe/qe_array_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_similarity_compressor-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_smt_context_manager-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_interp_tail_simplifier-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_util-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_generalizers-lto.o: plugin needed to handle lto object ar: muz_qe/unit_subsumption_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_farkas_learner-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_interpolant_provider-lto.o: plugin needed to handle lto object ar: muz_qe/qe_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_manager-lto.o: plugin needed to handle lto object ar: muz_qe/dl_sparse_table-lto.o: plugin needed to handle lto object src/tactic/sls/sls_tactic.cpp --> tactic/sls/sls_tactic-lto.o tactic/sls/sls_tactic-lto.a ar: tactic/sls/sls_tactic-lto.o: plugin needed to handle lto object src/smt/tactic/smt_tactic.cpp --> smt/tactic/smt_tactic-lto.o src/smt/tactic/ctx_solver_simplify_tactic.cpp --> smt/tactic/ctx_solver_simplify_tactic-lto.o smt/tactic/smt_tactic-lto.a ar: smt/tactic/smt_tactic-lto.o: plugin needed to handle lto object ar: smt/tactic/ctx_solver_simplify_tactic-lto.o: plugin needed to handle lto object src/tactic/fpa/fpa2bv_converter.cpp --> tactic/fpa/fpa2bv_converter-lto.o src/tactic/fpa/fpa2bv_tactic.cpp --> tactic/fpa/fpa2bv_tactic-lto.o src/tactic/fpa/qffpa_tactic.cpp --> tactic/fpa/qffpa_tactic-lto.o tactic/fpa/fpa-lto.a ar: tactic/fpa/fpa2bv_converter-lto.o: plugin needed to handle lto object ar: tactic/fpa/fpa2bv_tactic-lto.o: plugin needed to handle lto object ar: tactic/fpa/qffpa_tactic-lto.o: plugin needed to handle lto object src/tactic/bv/bv_size_reduction_tactic.cpp --> tactic/bv/bv_size_reduction_tactic-lto.o src/tactic/bv/bv1_blaster_tactic.cpp --> tactic/bv/bv1_blaster_tactic-lto.o src/tactic/bv/bit_blaster_model_converter.cpp --> tactic/bv/bit_blaster_model_converter-lto.o src/tactic/bv/max_bv_sharing_tactic.cpp --> tactic/bv/max_bv_sharing_tactic-lto.o src/tactic/bv/bit_blaster_tactic.cpp --> tactic/bv/bit_blaster_tactic-lto.o tactic/bv/bv_tactics-lto.a ar: tactic/bv/bv_size_reduction_tactic-lto.o: plugin needed to handle lto object ar: tactic/bv/bv1_blaster_tactic-lto.o: plugin needed to handle lto object ar: tactic/bv/bit_blaster_model_converter-lto.o: plugin needed to handle lto object ar: tactic/bv/max_bv_sharing_tactic-lto.o: plugin needed to handle lto object ar: tactic/bv/bit_blaster_tactic-lto.o: plugin needed to handle lto object src/smt/user_plugin/user_decl_plugin.cpp --> smt/user_plugin/user_decl_plugin-lto.o src/smt/user_plugin/user_smt_theory.cpp --> smt/user_plugin/user_smt_theory-lto.o src/smt/user_plugin/user_simplifier_plugin.cpp --> smt/user_plugin/user_simplifier_plugin-lto.o smt/user_plugin/user_plugin-lto.a ar: smt/user_plugin/user_decl_plugin-lto.o: plugin needed to handle lto object ar: smt/user_plugin/user_smt_theory-lto.o: plugin needed to handle lto object ar: smt/user_plugin/user_simplifier_plugin-lto.o: plugin needed to handle lto object src/smt/theory_diff_logic.cpp --> smt/theory_diff_logic-lto.o src/smt/smt_almost_cg_table.cpp --> smt/smt_almost_cg_table-lto.o src/smt/smt_quantifier_stat.cpp --> smt/smt_quantifier_stat-lto.o src/smt/smt_context_stat.cpp --> smt/smt_context_stat-lto.o src/smt/smt_setup.cpp --> smt/smt_setup-lto.o src/smt/smt_cg_table.cpp --> smt/smt_cg_table-lto.o src/smt/smt_conflict_resolution.cpp --> smt/smt_conflict_resolution-lto.o src/smt/smt_case_split_queue.cpp --> smt/smt_case_split_queue-lto.o src/smt/smt_solver.cpp --> smt/smt_solver-lto.o src/smt/mam.cpp --> smt/mam-lto.o src/smt/smt_context_inv.cpp --> smt/smt_context_inv-lto.o src/smt/expr_context_simplifier.cpp --> smt/expr_context_simplifier-lto.o src/smt/theory_datatype.cpp --> smt/theory_datatype-lto.o src/smt/smt_kernel.cpp --> smt/smt_kernel-lto.o src/smt/arith_eq_adapter.cpp --> smt/arith_eq_adapter-lto.o src/smt/smt_model_generator.cpp --> smt/smt_model_generator-lto.o src/smt/smt_statistics.cpp --> smt/smt_statistics-lto.o src/smt/cached_var_subst.cpp --> smt/cached_var_subst-lto.o src/smt/smt_literal.cpp --> smt/smt_literal-lto.o src/smt/smt_checker.cpp --> smt/smt_checker-lto.o src/smt/smt_implied_equalities.cpp --> smt/smt_implied_equalities-lto.o src/smt/smt_enode.cpp --> smt/smt_enode-lto.o src/smt/theory_instgen.cpp --> smt/theory_instgen-lto.o src/smt/smt_model_checker.cpp --> smt/smt_model_checker-lto.o src/smt/smt_quantifier.cpp --> smt/smt_quantifier-lto.o src/smt/theory_arith.cpp --> smt/theory_arith-lto.o src/smt/theory_dl.cpp --> smt/theory_dl-lto.o src/smt/theory_bv.cpp --> smt/theory_bv-lto.o src/smt/qi_queue.cpp --> smt/qi_queue-lto.o src/smt/theory_dummy.cpp --> smt/theory_dummy-lto.o src/smt/watch_list.cpp --> smt/watch_list-lto.o src/smt/smt_relevancy.cpp --> smt/smt_relevancy-lto.o src/smt/smt_internalizer.cpp --> smt/smt_internalizer-lto.o src/smt/cost_evaluator.cpp --> smt/cost_evaluator-lto.o src/smt/dyn_ack.cpp --> smt/dyn_ack-lto.o src/smt/smt_clause.cpp --> smt/smt_clause-lto.o src/smt/theory_array.cpp --> smt/theory_array-lto.o src/smt/smt_context_pp.cpp --> smt/smt_context_pp-lto.o src/smt/old_interval.cpp --> smt/old_interval-lto.o src/smt/theory_array_full.cpp --> smt/theory_array_full-lto.o src/smt/uses_theory.cpp --> smt/uses_theory-lto.o src/smt/smt_for_each_relevant_expr.cpp --> smt/smt_for_each_relevant_expr-lto.o src/smt/smt_justification.cpp --> smt/smt_justification-lto.o src/smt/smt_context.cpp --> smt/smt_context-lto.o src/smt/smt_model_finder.cpp --> smt/smt_model_finder-lto.o src/smt/arith_solver_plugin.cpp --> smt/arith_solver_plugin-lto.o src/smt/theory_array_base.cpp --> smt/theory_array_base-lto.o src/smt/smt_quick_checker.cpp --> smt/smt_quick_checker-lto.o src/smt/smt_theory.cpp --> smt/smt_theory-lto.o src/smt/fingerprints.cpp --> smt/fingerprints-lto.o src/smt/theory_dense_diff_logic.cpp --> smt/theory_dense_diff_logic-lto.o src/smt/asserted_formulas.cpp --> smt/asserted_formulas-lto.o src/smt/arith_eq_solver.cpp --> smt/arith_eq_solver-lto.o smt/smt-lto.a ar: smt/theory_diff_logic-lto.o: plugin needed to handle lto object ar: smt/smt_almost_cg_table-lto.o: plugin needed to handle lto object ar: smt/smt_quantifier_stat-lto.o: plugin needed to handle lto object ar: smt/smt_context_stat-lto.o: plugin needed to handle lto object ar: smt/smt_setup-lto.o: plugin needed to handle lto object ar: smt/smt_cg_table-lto.o: plugin needed to handle lto object ar: smt/smt_conflict_resolution-lto.o: plugin needed to handle lto object ar: smt/smt_case_split_queue-lto.o: plugin needed to handle lto object ar: smt/smt_solver-lto.o: plugin needed to handle lto object ar: smt/mam-lto.o: plugin needed to handle lto object ar: smt/smt_context_inv-lto.o: plugin needed to handle lto object ar: smt/expr_context_simplifier-lto.o: plugin needed to handle lto object ar: smt/theory_datatype-lto.o: plugin needed to handle lto object ar: smt/smt_kernel-lto.o: plugin needed to handle lto object ar: smt/arith_eq_adapter-lto.o: plugin needed to handle lto object ar: smt/smt_model_generator-lto.o: plugin needed to handle lto object ar: smt/smt_statistics-lto.o: plugin needed to handle lto object ar: smt/cached_var_subst-lto.o: plugin needed to handle lto object ar: smt/smt_literal-lto.o: plugin needed to handle lto object ar: smt/smt_checker-lto.o: plugin needed to handle lto object ar: smt/smt_implied_equalities-lto.o: plugin needed to handle lto object ar: smt/smt_enode-lto.o: plugin needed to handle lto object ar: smt/theory_instgen-lto.o: plugin needed to handle lto object ar: smt/smt_model_checker-lto.o: plugin needed to handle lto object ar: smt/smt_quantifier-lto.o: plugin needed to handle lto object ar: smt/theory_arith-lto.o: plugin needed to handle lto object ar: smt/theory_dl-lto.o: plugin needed to handle lto object ar: smt/theory_bv-lto.o: plugin needed to handle lto object ar: smt/qi_queue-lto.o: plugin needed to handle lto object ar: smt/theory_dummy-lto.o: plugin needed to handle lto object ar: smt/watch_list-lto.o: plugin needed to handle lto object ar: smt/smt_relevancy-lto.o: plugin needed to handle lto object ar: smt/smt_internalizer-lto.o: plugin needed to handle lto object ar: smt/cost_evaluator-lto.o: plugin needed to handle lto object ar: smt/dyn_ack-lto.o: plugin needed to handle lto object ar: smt/smt_clause-lto.o: plugin needed to handle lto object ar: smt/theory_array-lto.o: plugin needed to handle lto object ar: smt/smt_context_pp-lto.o: plugin needed to handle lto object ar: smt/old_interval-lto.o: plugin needed to handle lto object ar: smt/theory_array_full-lto.o: plugin needed to handle lto object ar: smt/uses_theory-lto.o: plugin needed to handle lto object ar: smt/smt_for_each_relevant_expr-lto.o: plugin needed to handle lto object ar: smt/smt_justification-lto.o: plugin needed to handle lto object ar: smt/smt_context-lto.o: plugin needed to handle lto object ar: smt/smt_model_finder-lto.o: plugin needed to handle lto object ar: smt/arith_solver_plugin-lto.o: plugin needed to handle lto object ar: smt/theory_array_base-lto.o: plugin needed to handle lto object ar: smt/smt_quick_checker-lto.o: plugin needed to handle lto object ar: smt/smt_theory-lto.o: plugin needed to handle lto object ar: smt/fingerprints-lto.o: plugin needed to handle lto object ar: smt/theory_dense_diff_logic-lto.o: plugin needed to handle lto object ar: smt/asserted_formulas-lto.o: plugin needed to handle lto object ar: smt/arith_eq_solver-lto.o: plugin needed to handle lto object src/smt/proto_model/array_factory.cpp --> smt/proto_model/array_factory-lto.o src/smt/proto_model/proto_model.cpp --> smt/proto_model/proto_model-lto.o src/smt/proto_model/value_factory.cpp --> smt/proto_model/value_factory-lto.o src/smt/proto_model/numeral_factory.cpp --> smt/proto_model/numeral_factory-lto.o src/smt/proto_model/struct_factory.cpp --> smt/proto_model/struct_factory-lto.o src/smt/proto_model/datatype_factory.cpp --> smt/proto_model/datatype_factory-lto.o smt/proto_model/proto_model-lto.a ar: smt/proto_model/array_factory-lto.o: plugin needed to handle lto object ar: smt/proto_model/proto_model-lto.o: plugin needed to handle lto object ar: smt/proto_model/value_factory-lto.o: plugin needed to handle lto object ar: smt/proto_model/numeral_factory-lto.o: plugin needed to handle lto object ar: smt/proto_model/struct_factory-lto.o: plugin needed to handle lto object ar: smt/proto_model/datatype_factory-lto.o: plugin needed to handle lto object src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp --> ast/rewriter/bit_blaster/bit_blaster_rewriter-lto.o src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp --> ast/rewriter/bit_blaster/eager_bit_blaster-lto.o src/ast/rewriter/bit_blaster/bit_blaster.cpp --> ast/rewriter/bit_blaster/bit_blaster-lto.o ast/rewriter/bit_blaster/bit_blaster-lto.a ar: ast/rewriter/bit_blaster/bit_blaster_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/bit_blaster/eager_bit_blaster-lto.o: plugin needed to handle lto object ar: ast/rewriter/bit_blaster/bit_blaster-lto.o: plugin needed to handle lto object src/ast/proof_checker/proof_checker.cpp --> ast/proof_checker/proof_checker-lto.o ast/proof_checker/proof_checker-lto.a ar: ast/proof_checker/proof_checker-lto.o: plugin needed to handle lto object src/ast/macros/quasi_macros.cpp --> ast/macros/quasi_macros-lto.o src/ast/macros/macro_manager.cpp --> ast/macros/macro_manager-lto.o src/ast/macros/macro_finder.cpp --> ast/macros/macro_finder-lto.o src/ast/macros/macro_util.cpp --> ast/macros/macro_util-lto.o ast/macros/macros-lto.a ar: ast/macros/quasi_macros-lto.o: plugin needed to handle lto object ar: ast/macros/macro_manager-lto.o: plugin needed to handle lto object ar: ast/macros/macro_finder-lto.o: plugin needed to handle lto object ar: ast/macros/macro_util-lto.o: plugin needed to handle lto object src/ast/pattern/expr_pattern_match.cpp --> ast/pattern/expr_pattern_match-lto.o src/ast/pattern/pattern_inference.cpp --> ast/pattern/pattern_inference-lto.o ast/pattern/pattern-lto.a ar: ast/pattern/expr_pattern_match-lto.o: plugin needed to handle lto object ar: ast/pattern/pattern_inference-lto.o: plugin needed to handle lto object src/parsers/smt2/smt2scanner.cpp --> parsers/smt2/smt2scanner-lto.o src/parsers/smt2/smt2parser.cpp --> parsers/smt2/smt2parser-lto.o parsers/smt2/smt2parser-lto.a ar: parsers/smt2/smt2scanner-lto.o: plugin needed to handle lto object ar: parsers/smt2/smt2parser-lto.o: plugin needed to handle lto object src/cmd_context/extra_cmds/dbg_cmds.cpp --> cmd_context/extra_cmds/dbg_cmds-lto.o src/cmd_context/extra_cmds/polynomial_cmds.cpp --> cmd_context/extra_cmds/polynomial_cmds-lto.o src/cmd_context/extra_cmds/subpaving_cmds.cpp --> cmd_context/extra_cmds/subpaving_cmds-lto.o cmd_context/extra_cmds/extra_cmds-lto.a ar: cmd_context/extra_cmds/dbg_cmds-lto.o: plugin needed to handle lto object ar: cmd_context/extra_cmds/polynomial_cmds-lto.o: plugin needed to handle lto object ar: cmd_context/extra_cmds/subpaving_cmds-lto.o: plugin needed to handle lto object src/cmd_context/simplify_cmd.cpp --> cmd_context/simplify_cmd-lto.o src/cmd_context/tactic_cmds.cpp --> cmd_context/tactic_cmds-lto.o src/cmd_context/cmd_context.cpp --> cmd_context/cmd_context-lto.o src/cmd_context/pdecl.cpp --> cmd_context/pdecl-lto.o src/cmd_context/echo_tactic.cpp --> cmd_context/echo_tactic-lto.o src/cmd_context/cmd_util.cpp --> cmd_context/cmd_util-lto.o src/cmd_context/tactic_manager.cpp --> cmd_context/tactic_manager-lto.o src/cmd_context/basic_cmds.cpp --> cmd_context/basic_cmds-lto.o src/cmd_context/cmd_context_to_goal.cpp --> cmd_context/cmd_context_to_goal-lto.o src/cmd_context/eval_cmd.cpp --> cmd_context/eval_cmd-lto.o src/cmd_context/parametric_cmd.cpp --> cmd_context/parametric_cmd-lto.o src/cmd_context/check_logic.cpp --> cmd_context/check_logic-lto.o cmd_context/cmd_context-lto.a ar: cmd_context/simplify_cmd-lto.o: plugin needed to handle lto object ar: cmd_context/tactic_cmds-lto.o: plugin needed to handle lto object ar: cmd_context/cmd_context-lto.o: plugin needed to handle lto object ar: cmd_context/pdecl-lto.o: plugin needed to handle lto object ar: cmd_context/echo_tactic-lto.o: plugin needed to handle lto object ar: cmd_context/cmd_util-lto.o: plugin needed to handle lto object ar: cmd_context/tactic_manager-lto.o: plugin needed to handle lto object ar: cmd_context/basic_cmds-lto.o: plugin needed to handle lto object ar: cmd_context/cmd_context_to_goal-lto.o: plugin needed to handle lto object ar: cmd_context/eval_cmd-lto.o: plugin needed to handle lto object ar: cmd_context/parametric_cmd-lto.o: plugin needed to handle lto object ar: cmd_context/check_logic-lto.o: plugin needed to handle lto object src/solver/solver.cpp --> solver/solver-lto.o src/solver/strategic_solver.cpp --> solver/strategic_solver-lto.o src/solver/solver_na2as.cpp --> solver/solver_na2as-lto.o src/solver/tactic2solver.cpp --> solver/tactic2solver-lto.o src/solver/check_sat_result.cpp --> solver/check_sat_result-lto.o solver/solver-lto.a ar: solver/solver-lto.o: plugin needed to handle lto object ar: solver/strategic_solver-lto.o: plugin needed to handle lto object ar: solver/solver_na2as-lto.o: plugin needed to handle lto object ar: solver/tactic2solver-lto.o: plugin needed to handle lto object ar: solver/check_sat_result-lto.o: plugin needed to handle lto object src/tactic/aig/aig_tactic.cpp --> tactic/aig/aig_tactic-lto.o src/tactic/aig/aig.cpp --> tactic/aig/aig-lto.o tactic/aig/aig_tactic-lto.a ar: tactic/aig/aig_tactic-lto.o: plugin needed to handle lto object ar: tactic/aig/aig-lto.o: plugin needed to handle lto object src/math/subpaving/tactic/subpaving_tactic.cpp --> math/subpaving/tactic/subpaving_tactic-lto.o src/math/subpaving/tactic/expr2subpaving.cpp --> math/subpaving/tactic/expr2subpaving-lto.o math/subpaving/tactic/subpaving_tactic-lto.a ar: math/subpaving/tactic/subpaving_tactic-lto.o: plugin needed to handle lto object ar: math/subpaving/tactic/expr2subpaving-lto.o: plugin needed to handle lto object src/nlsat/tactic/goal2nlsat.cpp --> nlsat/tactic/goal2nlsat-lto.o src/nlsat/tactic/qfnra_nlsat_tactic.cpp --> nlsat/tactic/qfnra_nlsat_tactic-lto.o src/nlsat/tactic/nlsat_tactic.cpp --> nlsat/tactic/nlsat_tactic-lto.o nlsat/tactic/nlsat_tactic-lto.a ar: nlsat/tactic/goal2nlsat-lto.o: plugin needed to handle lto object ar: nlsat/tactic/qfnra_nlsat_tactic-lto.o: plugin needed to handle lto object ar: nlsat/tactic/nlsat_tactic-lto.o: plugin needed to handle lto object src/tactic/arith/probe_arith.cpp --> tactic/arith/probe_arith-lto.o src/tactic/arith/nla2bv_tactic.cpp --> tactic/arith/nla2bv_tactic-lto.o src/tactic/arith/pb2bv_model_converter.cpp --> tactic/arith/pb2bv_model_converter-lto.o src/tactic/arith/bv2real_rewriter.cpp --> tactic/arith/bv2real_rewriter-lto.o src/tactic/arith/pb2bv_tactic.cpp --> tactic/arith/pb2bv_tactic-lto.o src/tactic/arith/fm_tactic.cpp --> tactic/arith/fm_tactic-lto.o src/tactic/arith/bv2int_rewriter.cpp --> tactic/arith/bv2int_rewriter-lto.o src/tactic/arith/recover_01_tactic.cpp --> tactic/arith/recover_01_tactic-lto.o src/tactic/arith/lia2pb_tactic.cpp --> tactic/arith/lia2pb_tactic-lto.o src/tactic/arith/normalize_bounds_tactic.cpp --> tactic/arith/normalize_bounds_tactic-lto.o src/tactic/arith/diff_neq_tactic.cpp --> tactic/arith/diff_neq_tactic-lto.o src/tactic/arith/bound_manager.cpp --> tactic/arith/bound_manager-lto.o src/tactic/arith/propagate_ineqs_tactic.cpp --> tactic/arith/propagate_ineqs_tactic-lto.o src/tactic/arith/add_bounds_tactic.cpp --> tactic/arith/add_bounds_tactic-lto.o src/tactic/arith/degree_shift_tactic.cpp --> tactic/arith/degree_shift_tactic-lto.o src/tactic/arith/factor_tactic.cpp --> tactic/arith/factor_tactic-lto.o src/tactic/arith/fix_dl_var_tactic.cpp --> tactic/arith/fix_dl_var_tactic-lto.o src/tactic/arith/bound_propagator.cpp --> tactic/arith/bound_propagator-lto.o src/tactic/arith/purify_arith_tactic.cpp --> tactic/arith/purify_arith_tactic-lto.o src/tactic/arith/linear_equation.cpp --> tactic/arith/linear_equation-lto.o tactic/arith/arith_tactics-lto.a ar: tactic/arith/probe_arith-lto.o: plugin needed to handle lto object ar: tactic/arith/nla2bv_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/pb2bv_model_converter-lto.o: plugin needed to handle lto object ar: tactic/arith/bv2real_rewriter-lto.o: plugin needed to handle lto object ar: tactic/arith/pb2bv_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/fm_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/bv2int_rewriter-lto.o: plugin needed to handle lto object ar: tactic/arith/recover_01_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/lia2pb_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/normalize_bounds_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/diff_neq_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/bound_manager-lto.o: plugin needed to handle lto object ar: tactic/arith/propagate_ineqs_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/add_bounds_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/degree_shift_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/factor_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/fix_dl_var_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/bound_propagator-lto.o: plugin needed to handle lto object ar: tactic/arith/purify_arith_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/linear_equation-lto.o: plugin needed to handle lto object src/sat/tactic/atom2bool_var.cpp --> sat/tactic/atom2bool_var-lto.o src/sat/tactic/sat_tactic.cpp --> sat/tactic/sat_tactic-lto.o src/sat/tactic/goal2sat.cpp --> sat/tactic/goal2sat-lto.o sat/tactic/sat_tactic-lto.a ar: sat/tactic/atom2bool_var-lto.o: plugin needed to handle lto object ar: sat/tactic/sat_tactic-lto.o: plugin needed to handle lto object ar: sat/tactic/goal2sat-lto.o: plugin needed to handle lto object src/tactic/core/ctx_simplify_tactic.cpp --> tactic/core/ctx_simplify_tactic-lto.o src/tactic/core/elim_term_ite_tactic.cpp --> tactic/core/elim_term_ite_tactic-lto.o src/tactic/core/propagate_values_tactic.cpp --> tactic/core/propagate_values_tactic-lto.o src/tactic/core/distribute_forall_tactic.cpp --> tactic/core/distribute_forall_tactic-lto.o src/tactic/core/der_tactic.cpp --> tactic/core/der_tactic-lto.o src/tactic/core/simplify_tactic.cpp --> tactic/core/simplify_tactic-lto.o src/tactic/core/occf_tactic.cpp --> tactic/core/occf_tactic-lto.o src/tactic/core/cofactor_term_ite_tactic.cpp --> tactic/core/cofactor_term_ite_tactic-lto.o src/tactic/core/cofactor_elim_term_ite.cpp --> tactic/core/cofactor_elim_term_ite-lto.o src/tactic/core/tseitin_cnf_tactic.cpp --> tactic/core/tseitin_cnf_tactic-lto.o src/tactic/core/split_clause_tactic.cpp --> tactic/core/split_clause_tactic-lto.o src/tactic/core/reduce_args_tactic.cpp --> tactic/core/reduce_args_tactic-lto.o src/tactic/core/symmetry_reduce_tactic.cpp --> tactic/core/symmetry_reduce_tactic-lto.o src/tactic/core/elim_uncnstr_tactic.cpp --> tactic/core/elim_uncnstr_tactic-lto.o src/tactic/core/nnf_tactic.cpp --> tactic/core/nnf_tactic-lto.o src/tactic/core/solve_eqs_tactic.cpp --> tactic/core/solve_eqs_tactic-lto.o tactic/core/core_tactics-lto.a ar: tactic/core/ctx_simplify_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/elim_term_ite_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/propagate_values_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/distribute_forall_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/der_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/simplify_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/occf_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/cofactor_term_ite_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/cofactor_elim_term_ite-lto.o: plugin needed to handle lto object ar: tactic/core/tseitin_cnf_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/split_clause_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/reduce_args_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/symmetry_reduce_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/elim_uncnstr_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/nnf_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/solve_eqs_tactic-lto.o: plugin needed to handle lto object src/ast/normal_forms/name_exprs.cpp --> ast/normal_forms/name_exprs-lto.o src/ast/normal_forms/nnf.cpp --> ast/normal_forms/nnf-lto.o src/ast/normal_forms/pull_quant.cpp --> ast/normal_forms/pull_quant-lto.o src/ast/normal_forms/defined_names.cpp --> ast/normal_forms/defined_names-lto.o src/ast/normal_forms/elim_term_ite.cpp --> ast/normal_forms/elim_term_ite-lto.o src/ast/normal_forms/cnf.cpp --> ast/normal_forms/cnf-lto.o ast/normal_forms/normal_forms-lto.a ar: ast/normal_forms/name_exprs-lto.o: plugin needed to handle lto object ar: ast/normal_forms/nnf-lto.o: plugin needed to handle lto object ar: ast/normal_forms/pull_quant-lto.o: plugin needed to handle lto object ar: ast/normal_forms/defined_names-lto.o: plugin needed to handle lto object ar: ast/normal_forms/elim_term_ite-lto.o: plugin needed to handle lto object ar: ast/normal_forms/cnf-lto.o: plugin needed to handle lto object src/ast/simplifier/simplifier.cpp --> ast/simplifier/simplifier-lto.o src/ast/simplifier/bit2int.cpp --> ast/simplifier/bit2int-lto.o src/ast/simplifier/elim_bounds.cpp --> ast/simplifier/elim_bounds-lto.o src/ast/simplifier/distribute_forall.cpp --> ast/simplifier/distribute_forall-lto.o src/ast/simplifier/simplifier_plugin.cpp --> ast/simplifier/simplifier_plugin-lto.o src/ast/simplifier/arith_simplifier_plugin.cpp --> ast/simplifier/arith_simplifier_plugin-lto.o src/ast/simplifier/maximise_ac_sharing.cpp --> ast/simplifier/maximise_ac_sharing-lto.o src/ast/simplifier/array_simplifier_plugin.cpp --> ast/simplifier/array_simplifier_plugin-lto.o src/ast/simplifier/poly_simplifier_plugin.cpp --> ast/simplifier/poly_simplifier_plugin-lto.o src/ast/simplifier/bv_simplifier_plugin.cpp --> ast/simplifier/bv_simplifier_plugin-lto.o src/ast/simplifier/datatype_simplifier_plugin.cpp --> ast/simplifier/datatype_simplifier_plugin-lto.o src/ast/simplifier/inj_axiom.cpp --> ast/simplifier/inj_axiom-lto.o src/ast/simplifier/push_app_ite.cpp --> ast/simplifier/push_app_ite-lto.o src/ast/simplifier/bv_elim.cpp --> ast/simplifier/bv_elim-lto.o src/ast/simplifier/basic_simplifier_plugin.cpp --> ast/simplifier/basic_simplifier_plugin-lto.o src/ast/simplifier/pull_ite_tree.cpp --> ast/simplifier/pull_ite_tree-lto.o ast/simplifier/simplifier-lto.a ar: ast/simplifier/simplifier-lto.o: plugin needed to handle lto object ar: ast/simplifier/bit2int-lto.o: plugin needed to handle lto object ar: ast/simplifier/elim_bounds-lto.o: plugin needed to handle lto object ar: ast/simplifier/distribute_forall-lto.o: plugin needed to handle lto object ar: ast/simplifier/simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/arith_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/maximise_ac_sharing-lto.o: plugin needed to handle lto object ar: ast/simplifier/array_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/poly_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/bv_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/datatype_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/inj_axiom-lto.o: plugin needed to handle lto object ar: ast/simplifier/push_app_ite-lto.o: plugin needed to handle lto object ar: ast/simplifier/bv_elim-lto.o: plugin needed to handle lto object ar: ast/simplifier/basic_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/pull_ite_tree-lto.o: plugin needed to handle lto object src/front_end_params/params2front_end_params.cpp --> front_end_params/params2front_end_params-lto.o src/front_end_params/model_params.cpp --> front_end_params/model_params-lto.o src/front_end_params/dyn_ack_params.cpp --> front_end_params/dyn_ack_params-lto.o src/front_end_params/nnf_params.cpp --> front_end_params/nnf_params-lto.o src/front_end_params/order_params.cpp --> front_end_params/order_params-lto.o src/front_end_params/cnf_params.cpp --> front_end_params/cnf_params-lto.o src/front_end_params/spc_params.cpp --> front_end_params/spc_params-lto.o src/front_end_params/parser_params.cpp --> front_end_params/parser_params-lto.o src/front_end_params/arith_simplifier_params.cpp --> front_end_params/arith_simplifier_params-lto.o src/front_end_params/pattern_inference_params.cpp --> front_end_params/pattern_inference_params-lto.o src/front_end_params/theory_arith_params.cpp --> front_end_params/theory_arith_params-lto.o src/front_end_params/z3_solver_params.cpp --> front_end_params/z3_solver_params-lto.o src/front_end_params/front_end_params.cpp --> front_end_params/front_end_params-lto.o src/front_end_params/smt_params.cpp --> front_end_params/smt_params-lto.o front_end_params/front_end_params-lto.a ar: front_end_params/params2front_end_params-lto.o: plugin needed to handle lto object ar: front_end_params/model_params-lto.o: plugin needed to handle lto object ar: front_end_params/dyn_ack_params-lto.o: plugin needed to handle lto object ar: front_end_params/nnf_params-lto.o: plugin needed to handle lto object ar: front_end_params/order_params-lto.o: plugin needed to handle lto object ar: front_end_params/cnf_params-lto.o: plugin needed to handle lto object ar: front_end_params/spc_params-lto.o: plugin needed to handle lto object ar: front_end_params/parser_params-lto.o: plugin needed to handle lto object ar: front_end_params/arith_simplifier_params-lto.o: plugin needed to handle lto object ar: front_end_params/pattern_inference_params-lto.o: plugin needed to handle lto object ar: front_end_params/theory_arith_params-lto.o: plugin needed to handle lto object ar: front_end_params/z3_solver_params-lto.o: plugin needed to handle lto object ar: front_end_params/front_end_params-lto.o: plugin needed to handle lto object ar: front_end_params/smt_params-lto.o: plugin needed to handle lto object src/math/euclid/euclidean_solver.cpp --> math/euclid/euclidean_solver-lto.o math/euclid/euclid-lto.a ar: math/euclid/euclidean_solver-lto.o: plugin needed to handle lto object src/math/grobner/grobner.cpp --> math/grobner/grobner-lto.o math/grobner/grobner-lto.a ar: math/grobner/grobner-lto.o: plugin needed to handle lto object src/parsers/util/pattern_validation.cpp --> parsers/util/pattern_validation-lto.o src/parsers/util/scanner.cpp --> parsers/util/scanner-lto.o src/parsers/util/cost_parser.cpp --> parsers/util/cost_parser-lto.o src/parsers/util/simple_parser.cpp --> parsers/util/simple_parser-lto.o parsers/util/parser_util-lto.a ar: parsers/util/pattern_validation-lto.o: plugin needed to handle lto object ar: parsers/util/scanner-lto.o: plugin needed to handle lto object ar: parsers/util/cost_parser-lto.o: plugin needed to handle lto object ar: parsers/util/simple_parser-lto.o: plugin needed to handle lto object src/ast/substitution/matcher.cpp --> ast/substitution/matcher-lto.o src/ast/substitution/substitution.cpp --> ast/substitution/substitution-lto.o src/ast/substitution/substitution_tree.cpp --> ast/substitution/substitution_tree-lto.o src/ast/substitution/unifier.cpp --> ast/substitution/unifier-lto.o ast/substitution/substitution-lto.a ar: ast/substitution/matcher-lto.o: plugin needed to handle lto object ar: ast/substitution/substitution-lto.o: plugin needed to handle lto object ar: ast/substitution/substitution_tree-lto.o: plugin needed to handle lto object ar: ast/substitution/unifier-lto.o: plugin needed to handle lto object src/tactic/goal_util.cpp --> tactic/goal_util-lto.o src/tactic/model_converter.cpp --> tactic/model_converter-lto.o src/tactic/num_occurs_goal.cpp --> tactic/num_occurs_goal-lto.o src/tactic/tactic.cpp --> tactic/tactic-lto.o src/tactic/filter_model_converter.cpp --> tactic/filter_model_converter-lto.o src/tactic/extension_model_converter.cpp --> tactic/extension_model_converter-lto.o src/tactic/goal.cpp --> tactic/goal-lto.o src/tactic/probe.cpp --> tactic/probe-lto.o src/tactic/tactical.cpp --> tactic/tactical-lto.o src/tactic/proof_converter.cpp --> tactic/proof_converter-lto.o src/tactic/goal_shared_occs.cpp --> tactic/goal_shared_occs-lto.o tactic/tactic-lto.a ar: tactic/goal_util-lto.o: plugin needed to handle lto object ar: tactic/model_converter-lto.o: plugin needed to handle lto object ar: tactic/num_occurs_goal-lto.o: plugin needed to handle lto object ar: tactic/tactic-lto.o: plugin needed to handle lto object ar: tactic/filter_model_converter-lto.o: plugin needed to handle lto object ar: tactic/extension_model_converter-lto.o: plugin needed to handle lto object ar: tactic/goal-lto.o: plugin needed to handle lto object ar: tactic/probe-lto.o: plugin needed to handle lto object ar: tactic/tactical-lto.o: plugin needed to handle lto object ar: tactic/proof_converter-lto.o: plugin needed to handle lto object ar: tactic/goal_shared_occs-lto.o: plugin needed to handle lto object src/model/model_smt2_pp.cpp --> model/model_smt2_pp-lto.o src/model/func_interp.cpp --> model/func_interp-lto.o src/model/model.cpp --> model/model-lto.o src/model/model_core.cpp --> model/model_core-lto.o src/model/model_v2_pp.cpp --> model/model_v2_pp-lto.o src/model/model_evaluator.cpp --> model/model_evaluator-lto.o src/model/model_pp.cpp --> model/model_pp-lto.o model/model-lto.a ar: model/model_smt2_pp-lto.o: plugin needed to handle lto object ar: model/func_interp-lto.o: plugin needed to handle lto object ar: model/model-lto.o: plugin needed to handle lto object ar: model/model_core-lto.o: plugin needed to handle lto object ar: model/model_v2_pp-lto.o: plugin needed to handle lto object ar: model/model_evaluator-lto.o: plugin needed to handle lto object ar: model/model_pp-lto.o: plugin needed to handle lto object src/ast/rewriter/arith_rewriter.cpp --> ast/rewriter/arith_rewriter-lto.o src/ast/rewriter/th_rewriter.cpp --> ast/rewriter/th_rewriter-lto.o src/ast/rewriter/expr_replacer.cpp --> ast/rewriter/expr_replacer-lto.o src/ast/rewriter/mk_simplified_app.cpp --> ast/rewriter/mk_simplified_app-lto.o src/ast/rewriter/der.cpp --> ast/rewriter/der-lto.o src/ast/rewriter/dl_rewriter.cpp --> ast/rewriter/dl_rewriter-lto.o src/ast/rewriter/float_rewriter.cpp --> ast/rewriter/float_rewriter-lto.o src/ast/rewriter/factor_rewriter.cpp --> ast/rewriter/factor_rewriter-lto.o src/ast/rewriter/array_rewriter.cpp --> ast/rewriter/array_rewriter-lto.o src/ast/rewriter/quant_hoist.cpp --> ast/rewriter/quant_hoist-lto.o src/ast/rewriter/datatype_rewriter.cpp --> ast/rewriter/datatype_rewriter-lto.o src/ast/rewriter/var_subst.cpp --> ast/rewriter/var_subst-lto.o src/ast/rewriter/rewriter.cpp --> ast/rewriter/rewriter-lto.o src/ast/rewriter/bv_rewriter.cpp --> ast/rewriter/bv_rewriter-lto.o src/ast/rewriter/bool_rewriter.cpp --> ast/rewriter/bool_rewriter-lto.o ast/rewriter/rewriter-lto.a ar: ast/rewriter/arith_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/th_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/expr_replacer-lto.o: plugin needed to handle lto object ar: ast/rewriter/mk_simplified_app-lto.o: plugin needed to handle lto object ar: ast/rewriter/der-lto.o: plugin needed to handle lto object ar: ast/rewriter/dl_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/float_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/factor_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/array_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/quant_hoist-lto.o: plugin needed to handle lto object ar: ast/rewriter/datatype_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/var_subst-lto.o: plugin needed to handle lto object ar: ast/rewriter/rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/bv_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/bool_rewriter-lto.o: plugin needed to handle lto object src/ast/has_free_vars.cpp --> ast/has_free_vars-lto.o src/ast/ast_printer.cpp --> ast/ast_printer-lto.o src/ast/ast_util.cpp --> ast/ast_util-lto.o src/ast/pp.cpp --> ast/pp-lto.o src/ast/act_cache.cpp --> ast/act_cache-lto.o src/ast/ast_smt2_pp.cpp --> ast/ast_smt2_pp-lto.o src/ast/num_occurs.cpp --> ast/num_occurs-lto.o src/ast/bv_decl_plugin.cpp --> ast/bv_decl_plugin-lto.o src/ast/expr_functors.cpp --> ast/expr_functors-lto.o src/ast/ast.cpp --> ast/ast-lto.o src/ast/expr_abstract.cpp --> ast/expr_abstract-lto.o src/ast/for_each_ast.cpp --> ast/for_each_ast-lto.o src/ast/ast_translation.cpp --> ast/ast_translation-lto.o src/ast/expr2polynomial.cpp --> ast/expr2polynomial-lto.o src/ast/datatype_decl_plugin.cpp --> ast/datatype_decl_plugin-lto.o src/ast/format.cpp --> ast/format-lto.o src/ast/expr2var.cpp --> ast/expr2var-lto.o src/ast/arith_decl_plugin.cpp --> ast/arith_decl_plugin-lto.o src/ast/expr_map.cpp --> ast/expr_map-lto.o src/ast/for_each_expr.cpp --> ast/for_each_expr-lto.o src/ast/ast_pp.cpp --> ast/ast_pp-lto.o src/ast/shared_occs.cpp --> ast/shared_occs-lto.o src/ast/reg_decl_plugins.cpp --> ast/reg_decl_plugins-lto.o src/ast/well_sorted.cpp --> ast/well_sorted-lto.o src/ast/ast_smt_pp.cpp --> ast/ast_smt_pp-lto.o src/ast/static_features.cpp --> ast/static_features-lto.o src/ast/expr_substitution.cpp --> ast/expr_substitution-lto.o src/ast/pp_params.cpp --> ast/pp_params-lto.o src/ast/array_decl_plugin.cpp --> ast/array_decl_plugin-lto.o src/ast/func_decl_dependencies.cpp --> ast/func_decl_dependencies-lto.o src/ast/decl_collector.cpp --> ast/decl_collector-lto.o src/ast/expr_stat.cpp --> ast/expr_stat-lto.o src/ast/used_vars.cpp --> ast/used_vars-lto.o src/ast/dl_decl_plugin.cpp --> ast/dl_decl_plugin-lto.o src/ast/macro_substitution.cpp --> ast/macro_substitution-lto.o src/ast/float_decl_plugin.cpp --> ast/float_decl_plugin-lto.o src/ast/occurs.cpp --> ast/occurs-lto.o src/ast/ast_ll_pp.cpp --> ast/ast_ll_pp-lto.o src/ast/seq_decl_plugin.cpp --> ast/seq_decl_plugin-lto.o src/ast/ast_lt.cpp --> ast/ast_lt-lto.o ast/ast-lto.a ar: ast/has_free_vars-lto.o: plugin needed to handle lto object ar: ast/ast_printer-lto.o: plugin needed to handle lto object ar: ast/ast_util-lto.o: plugin needed to handle lto object ar: ast/pp-lto.o: plugin needed to handle lto object ar: ast/act_cache-lto.o: plugin needed to handle lto object ar: ast/ast_smt2_pp-lto.o: plugin needed to handle lto object ar: ast/num_occurs-lto.o: plugin needed to handle lto object ar: ast/bv_decl_plugin-lto.o: plugin needed to handle lto object ar: ast/expr_functors-lto.o: plugin needed to handle lto object ar: ast/ast-lto.o: plugin needed to handle lto object ar: ast/expr_abstract-lto.o: plugin needed to handle lto object ar: ast/for_each_ast-lto.o: plugin needed to handle lto object ar: ast/ast_translation-lto.o: plugin needed to handle lto object ar: ast/expr2polynomial-lto.o: plugin needed to handle lto object ar: ast/datatype_decl_plugin-lto.o: plugin needed to handle lto object ar: ast/format-lto.o: plugin needed to handle lto object ar: ast/expr2var-lto.o: plugin needed to handle lto object ar: ast/arith_decl_plugin-lto.o: plugin needed to handle lto object ar: ast/expr_map-lto.o: plugin needed to handle lto object ar: ast/for_each_expr-lto.o: plugin needed to handle lto object ar: ast/ast_pp-lto.o: plugin needed to handle lto object ar: ast/shared_occs-lto.o: plugin needed to handle lto object ar: ast/reg_decl_plugins-lto.o: plugin needed to handle lto object ar: ast/well_sorted-lto.o: plugin needed to handle lto object ar: ast/ast_smt_pp-lto.o: plugin needed to handle lto object ar: ast/static_features-lto.o: plugin needed to handle lto object ar: ast/expr_substitution-lto.o: plugin needed to handle lto object ar: ast/pp_params-lto.o: plugin needed to handle lto object ar: ast/array_decl_plugin-lto.o: plugin needed to handle lto object ar: ast/func_decl_dependencies-lto.o: plugin needed to handle lto object ar: ast/decl_collector-lto.o: plugin needed to handle lto object ar: ast/expr_stat-lto.o: plugin needed to handle lto object ar: ast/used_vars-lto.o: plugin needed to handle lto object ar: ast/dl_decl_plugin-lto.o: plugin needed to handle lto object ar: ast/macro_substitution-lto.o: plugin needed to handle lto object ar: ast/float_decl_plugin-lto.o: plugin needed to handle lto object ar: ast/occurs-lto.o: plugin needed to handle lto object ar: ast/ast_ll_pp-lto.o: plugin needed to handle lto object ar: ast/seq_decl_plugin-lto.o: plugin needed to handle lto object ar: ast/ast_lt-lto.o: plugin needed to handle lto object src/math/subpaving/subpaving_mpf.cpp --> math/subpaving/subpaving_mpf-lto.o src/math/subpaving/subpaving.cpp --> math/subpaving/subpaving-lto.o src/math/subpaving/subpaving_hwf.cpp --> math/subpaving/subpaving_hwf-lto.o src/math/subpaving/subpaving_mpq.cpp --> math/subpaving/subpaving_mpq-lto.o src/math/subpaving/subpaving_mpff.cpp --> math/subpaving/subpaving_mpff-lto.o src/math/subpaving/subpaving_mpfx.cpp --> math/subpaving/subpaving_mpfx-lto.o math/subpaving/subpaving-lto.a ar: math/subpaving/subpaving_mpf-lto.o: plugin needed to handle lto object ar: math/subpaving/subpaving-lto.o: plugin needed to handle lto object ar: math/subpaving/subpaving_hwf-lto.o: plugin needed to handle lto object ar: math/subpaving/subpaving_mpq-lto.o: plugin needed to handle lto object ar: math/subpaving/subpaving_mpff-lto.o: plugin needed to handle lto object ar: math/subpaving/subpaving_mpfx-lto.o: plugin needed to handle lto object src/math/interval/interval_mpq.cpp --> math/interval/interval_mpq-lto.o math/interval/interval-lto.a ar: math/interval/interval_mpq-lto.o: plugin needed to handle lto object src/nlsat/nlsat_evaluator.cpp --> nlsat/nlsat_evaluator-lto.o src/nlsat/nlsat_clause.cpp --> nlsat/nlsat_clause-lto.o src/nlsat/nlsat_explain.cpp --> nlsat/nlsat_explain-lto.o src/nlsat/nlsat_types.cpp --> nlsat/nlsat_types-lto.o src/nlsat/nlsat_interval_set.cpp --> nlsat/nlsat_interval_set-lto.o src/nlsat/nlsat_solver.cpp --> nlsat/nlsat_solver-lto.o nlsat/nlsat-lto.a ar: nlsat/nlsat_evaluator-lto.o: plugin needed to handle lto object ar: nlsat/nlsat_clause-lto.o: plugin needed to handle lto object ar: nlsat/nlsat_explain-lto.o: plugin needed to handle lto object ar: nlsat/nlsat_types-lto.o: plugin needed to handle lto object ar: nlsat/nlsat_interval_set-lto.o: plugin needed to handle lto object ar: nlsat/nlsat_solver-lto.o: plugin needed to handle lto object src/sat/sat_config.cpp --> sat/sat_config-lto.o src/sat/sat_cleaner.cpp --> sat/sat_cleaner-lto.o src/sat/sat_clause_set.cpp --> sat/sat_clause_set-lto.o src/sat/sat_elim_eqs.cpp --> sat/sat_elim_eqs-lto.o src/sat/sat_watched.cpp --> sat/sat_watched-lto.o src/sat/sat_clause.cpp --> sat/sat_clause-lto.o src/sat/sat_iff3_finder.cpp --> sat/sat_iff3_finder-lto.o src/sat/sat_scc.cpp --> sat/sat_scc-lto.o src/sat/sat_model_converter.cpp --> sat/sat_model_converter-lto.o src/sat/sat_solver.cpp --> sat/sat_solver-lto.o src/sat/dimacs.cpp --> sat/dimacs-lto.o src/sat/sat_probing.cpp --> sat/sat_probing-lto.o src/sat/sat_simplifier.cpp --> sat/sat_simplifier-lto.o src/sat/sat_integrity_checker.cpp --> sat/sat_integrity_checker-lto.o src/sat/sat_asymm_branch.cpp --> sat/sat_asymm_branch-lto.o src/sat/sat_clause_use_list.cpp --> sat/sat_clause_use_list-lto.o sat/sat-lto.a ar: sat/sat_config-lto.o: plugin needed to handle lto object ar: sat/sat_cleaner-lto.o: plugin needed to handle lto object ar: sat/sat_clause_set-lto.o: plugin needed to handle lto object ar: sat/sat_elim_eqs-lto.o: plugin needed to handle lto object ar: sat/sat_watched-lto.o: plugin needed to handle lto object ar: sat/sat_clause-lto.o: plugin needed to handle lto object ar: sat/sat_iff3_finder-lto.o: plugin needed to handle lto object ar: sat/sat_scc-lto.o: plugin needed to handle lto object ar: sat/sat_model_converter-lto.o: plugin needed to handle lto object ar: sat/sat_solver-lto.o: plugin needed to handle lto object ar: sat/dimacs-lto.o: plugin needed to handle lto object ar: sat/sat_probing-lto.o: plugin needed to handle lto object ar: sat/sat_simplifier-lto.o: plugin needed to handle lto object ar: sat/sat_integrity_checker-lto.o: plugin needed to handle lto object ar: sat/sat_asymm_branch-lto.o: plugin needed to handle lto object ar: sat/sat_clause_use_list-lto.o: plugin needed to handle lto object src/math/polynomial/polynomial_cache.cpp --> math/polynomial/polynomial_cache-lto.o src/math/polynomial/rpolynomial.cpp --> math/polynomial/rpolynomial-lto.o src/math/polynomial/sexpr2upolynomial.cpp --> math/polynomial/sexpr2upolynomial-lto.o src/math/polynomial/upolynomial.cpp --> math/polynomial/upolynomial-lto.o src/math/polynomial/polynomial_factorization.cpp --> math/polynomial/polynomial_factorization-lto.o src/math/polynomial/upolynomial_factorization.cpp --> math/polynomial/upolynomial_factorization-lto.o src/math/polynomial/algebraic_numbers.cpp --> math/polynomial/algebraic_numbers-lto.o src/math/polynomial/polynomial.cpp --> math/polynomial/polynomial-lto.o math/polynomial/polynomial-lto.a ar: math/polynomial/polynomial_cache-lto.o: plugin needed to handle lto object ar: math/polynomial/rpolynomial-lto.o: plugin needed to handle lto object ar: math/polynomial/sexpr2upolynomial-lto.o: plugin needed to handle lto object ar: math/polynomial/upolynomial-lto.o: plugin needed to handle lto object ar: math/polynomial/polynomial_factorization-lto.o: plugin needed to handle lto object ar: math/polynomial/upolynomial_factorization-lto.o: plugin needed to handle lto object ar: math/polynomial/algebraic_numbers-lto.o: plugin needed to handle lto object ar: math/polynomial/polynomial-lto.o: plugin needed to handle lto object src/util/common_msgs.cpp --> util/common_msgs-lto.o src/util/util.cpp --> util/util-lto.o src/util/mpff.cpp --> util/mpff-lto.o src/util/statistics.cpp --> util/statistics-lto.o src/util/params.cpp --> util/params-lto.o src/util/memory_manager.cpp --> util/memory_manager-lto.o src/util/instruction_count.cpp --> util/instruction_count-lto.o src/util/smt2_util.cpp --> util/smt2_util-lto.o src/util/s_integer.cpp --> util/s_integer-lto.o src/util/inf_int_rational.cpp --> util/inf_int_rational-lto.o src/util/hwf.cpp --> util/hwf-lto.o src/util/trace.cpp --> util/trace-lto.o src/util/scoped_ctrl_c.cpp --> util/scoped_ctrl_c-lto.o src/util/warning.cpp --> util/warning-lto.o src/util/cooperate.cpp --> util/cooperate-lto.o src/util/timer.cpp --> util/timer-lto.o src/util/mpn.cpp --> util/mpn-lto.o src/util/permutation.cpp --> util/permutation-lto.o src/util/symbol.cpp --> util/symbol-lto.o src/util/timeit.cpp --> util/timeit-lto.o src/util/debug.cpp --> util/debug-lto.o src/util/lbool.cpp --> util/lbool-lto.o src/util/sexpr.cpp --> util/sexpr-lto.o src/util/approx_set.cpp --> util/approx_set-lto.o src/util/mem_stat.cpp --> util/mem_stat-lto.o src/util/page.cpp --> util/page-lto.o src/util/stack.cpp --> util/stack-lto.o src/util/luby.cpp --> util/luby-lto.o src/util/mpz.cpp --> util/mpz-lto.o src/util/mpq.cpp --> util/mpq-lto.o src/util/region.cpp --> util/region-lto.o src/util/timeout.cpp --> util/timeout-lto.o src/util/cmd_context_types.cpp --> util/cmd_context_types-lto.o src/util/prime_generator.cpp --> util/prime_generator-lto.o src/util/mpfx.cpp --> util/mpfx-lto.o src/util/hash.cpp --> util/hash-lto.o src/util/approx_nat.cpp --> util/approx_nat-lto.o src/util/small_object_allocator.cpp --> util/small_object_allocator-lto.o src/util/bit_vector.cpp --> util/bit_vector-lto.o src/util/mpbq.cpp --> util/mpbq-lto.o src/util/mpq_inf.cpp --> util/mpq_inf-lto.o src/util/rational.cpp --> util/rational-lto.o src/util/scoped_timer.cpp --> util/scoped_timer-lto.o src/util/bit_util.cpp --> util/bit_util-lto.o src/util/inf_s_integer.cpp --> util/inf_s_integer-lto.o src/util/inf_rational.cpp --> util/inf_rational-lto.o src/util/ini_file.cpp --> util/ini_file-lto.o src/util/z3_exception.cpp --> util/z3_exception-lto.o src/util/mpf.cpp --> util/mpf-lto.o util/util-lto.a ar: util/common_msgs-lto.o: plugin needed to handle lto object ar: util/util-lto.o: plugin needed to handle lto object ar: util/mpff-lto.o: plugin needed to handle lto object ar: util/statistics-lto.o: plugin needed to handle lto object ar: util/params-lto.o: plugin needed to handle lto object ar: util/memory_manager-lto.o: plugin needed to handle lto object ar: util/instruction_count-lto.o: plugin needed to handle lto object ar: util/smt2_util-lto.o: plugin needed to handle lto object ar: util/s_integer-lto.o: plugin needed to handle lto object ar: util/inf_int_rational-lto.o: plugin needed to handle lto object ar: util/hwf-lto.o: plugin needed to handle lto object ar: util/trace-lto.o: plugin needed to handle lto object ar: util/scoped_ctrl_c-lto.o: plugin needed to handle lto object ar: util/warning-lto.o: plugin needed to handle lto object ar: util/cooperate-lto.o: plugin needed to handle lto object ar: util/timer-lto.o: plugin needed to handle lto object ar: util/mpn-lto.o: plugin needed to handle lto object ar: util/permutation-lto.o: plugin needed to handle lto object ar: util/symbol-lto.o: plugin needed to handle lto object ar: util/timeit-lto.o: plugin needed to handle lto object ar: util/debug-lto.o: plugin needed to handle lto object ar: util/lbool-lto.o: plugin needed to handle lto object ar: util/sexpr-lto.o: plugin needed to handle lto object ar: util/approx_set-lto.o: plugin needed to handle lto object ar: util/mem_stat-lto.o: plugin needed to handle lto object ar: util/page-lto.o: plugin needed to handle lto object ar: util/stack-lto.o: plugin needed to handle lto object ar: util/luby-lto.o: plugin needed to handle lto object ar: util/mpz-lto.o: plugin needed to handle lto object ar: util/mpq-lto.o: plugin needed to handle lto object ar: util/region-lto.o: plugin needed to handle lto object ar: util/timeout-lto.o: plugin needed to handle lto object ar: util/cmd_context_types-lto.o: plugin needed to handle lto object ar: util/prime_generator-lto.o: plugin needed to handle lto object ar: util/mpfx-lto.o: plugin needed to handle lto object ar: util/hash-lto.o: plugin needed to handle lto object ar: util/approx_nat-lto.o: plugin needed to handle lto object ar: util/small_object_allocator-lto.o: plugin needed to handle lto object ar: util/bit_vector-lto.o: plugin needed to handle lto object ar: util/mpbq-lto.o: plugin needed to handle lto object ar: util/mpq_inf-lto.o: plugin needed to handle lto object ar: util/rational-lto.o: plugin needed to handle lto object ar: util/scoped_timer-lto.o: plugin needed to handle lto object ar: util/bit_util-lto.o: plugin needed to handle lto object ar: util/inf_s_integer-lto.o: plugin needed to handle lto object ar: util/inf_rational-lto.o: plugin needed to handle lto object ar: util/ini_file-lto.o: plugin needed to handle lto object ar: util/z3_exception-lto.o: plugin needed to handle lto object ar: util/mpf-lto.o: plugin needed to handle lto object g++ -o z3 -flto=jobserver -O3 shell/datalog_frontend-lto.o shell/z3_log_frontend-lto.o shell/main-lto.o shell/install_tactic-lto.o shell/dimacs_frontend-lto.o shell/smtlib_frontend-lto.o api/api-lto.a parsers/smt/smtparser-lto.a tactic/portfolio/portfolio-lto.a tactic/ufbv/ufbv_tactic-lto.a tactic/smtlogics/smtlogic_tactics-lto.a muz_qe/muz_qe-lto.a tactic/sls/sls_tactic-lto.a smt/tactic/smt_tactic-lto.a tactic/fpa/fpa-lto.a tactic/bv/bv_tactics-lto.a smt/user_plugin/user_plugin-lto.a smt/smt-lto.a smt/proto_model/proto_model-lto.a ast/rewriter/bit_blaster/bit_blaster-lto.a ast/proof_checker/proof_checker-lto.a ast/macros/macros-lto.a ast/pattern/pattern-lto.a parsers/smt2/smt2parser-lto.a cmd_context/extra_cmds/extra_cmds-lto.a cmd_context/cmd_context-lto.a solver/solver-lto.a tactic/aig/aig_tactic-lto.a math/subpaving/tactic/subpaving_tactic-lto.a nlsat/tactic/nlsat_tactic-lto.a tactic/arith/arith_tactics-lto.a sat/tactic/sat_tactic-lto.a tactic/core/core_tactics-lto.a ast/normal_forms/normal_forms-lto.a ast/simplifier/simplifier-lto.a front_end_params/front_end_params-lto.a math/euclid/euclid-lto.a math/grobner/grobner-lto.a parsers/util/parser_util-lto.a ast/substitution/substitution-lto.a tactic/tactic-lto.a model/model-lto.a ast/rewriter/rewriter-lto.a ast/ast-lto.a math/subpaving/subpaving-lto.a math/interval/interval-lto.a nlsat/nlsat-lto.a sat/sat-lto.a math/polynomial/polynomial-lto.a util/util-lto.a -lpthread -fopenmp -lrt /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `datalog_params::register_params(ini_params&)':

:(.text+0x145): undefined reference to `ini_params::register_symbol_param(char const*, symbol&, char const*, bool)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `extra_params::register_params(ini_params&)': :(.text+0x195): undefined reference to `ini_params::register_symbol_param(char const*, symbol&, char const*, bool)' :(.text+0x1b2): undefined reference to `ini_params::register_bool_param(char const*, bool&, char const*, bool)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `order_params::~order_params()': :(.text+0x2a7): undefined reference to `memory::deallocate(void*)' :(.text+0x2b9): undefined reference to `memory::deallocate(void*)' :(.text+0x2e8): undefined reference to `memory::deallocate(void*)' :(.text+0x305): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `del_params()': :(.text+0x323): undefined reference to `front_end_params::close_trace_file()' :(.text+0x349): undefined reference to `ini_params::~ini_params()' :(.text+0x386): undefined reference to `param_vector::dec_ref()' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `solve(char const*, std::istream&) [clone .isra.3]': :(.text+0x433): undefined reference to `z3_replayer::z3_replayer(std::istream&)' :(.text+0x43b): undefined reference to `z3_replayer::parse()' :(.text+0x452): undefined reference to `memory::display_max_usage(std::ostream&)' :(.text+0x4af): undefined reference to `z3_replayer::~z3_replayer()' :(.text+0x4de): undefined reference to `z3_replayer::get_line() const' :(.text+0x544): undefined reference to `z3_replayer::~z3_replayer()' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `datalog_params::register_params(ini_params&)': :(.text+0x168): undefined reference to `ini_params::register_bool_param(char const*, bool&, char const*, bool)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `extra_params::register_params(ini_params&)': :(.text+0x1d5): undefined reference to `ini_params::register_bool_param(char const*, bool&, char const*, bool)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `order_params::~order_params()': :(.text+0x2d0): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `datalog::compiler::instruction_observer::notify(datalog::instruction*)': :(.text+0x6b5): undefined reference to `datalog::accounted_object::set_accounting_parent_object(datalog::context&, datalog::rule*)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `read_ini_file(char const*)': :(.text.unlikely+0x36): undefined reference to `ini_params::read_ini_file(std::istream&)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `ref::dec_ref()': :(.text.unlikely+0xbb): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans0.ltrans.o: In function `main': :(.text.startup+0x19): undefined reference to `memory::initialize(unsigned long)' :(.text.startup+0x37): undefined reference to `memory::exit_when_out_of_memory(bool, char const*)' :(.text.startup+0x90): undefined reference to `ini_params::set_param_value(char const*, char const*)' :(.text.startup+0x182): undefined reference to `memory::set_high_watermark(unsigned long)' :(.text.startup+0x198): undefined reference to `memory::set_max_size(unsigned long)' :(.text.startup+0x1a4): undefined reference to `front_end_params::open_trace_file()' :(.text.startup+0x224): undefined reference to `warning_msg(char const*, ...)' :(.text.startup+0x23a): undefined reference to `warning_msg(char const*, ...)' :(.text.startup+0x320): undefined reference to `warning_msg(char const*, ...)' :(.text.startup+0x412): undefined reference to `set_verbosity_level(unsigned int)' :(.text.startup+0x4d5): undefined reference to `z3_bound_num_procs()' :(.text.startup+0xb85): undefined reference to `parser_params::parser_params()' :(.text.startup+0xc07): undefined reference to `memory::allocate(unsigned long)' :(.text.startup+0xc1e): undefined reference to `param_vector::param_vector(void*)' :(.text.startup+0xc2d): undefined reference to `param_vector::inc_ref()' :(.text.startup+0xd3f): undefined reference to `ini_params::ini_params(bool)' :(.text.startup+0xd6d): undefined reference to `symbol::symbol(char const*)' :(.text.startup+0xd99): undefined reference to `register_verbosity_level(ini_params&)' :(.text.startup+0xda5): undefined reference to `register_warning(ini_params&)' :(.text.startup+0xdb1): undefined reference to `register_pp_params(ini_params&)' :(.text.startup+0xdc4): undefined reference to `front_end_params::register_params(ini_params&)' :(.text.startup+0xe27): undefined reference to `memory::finalize()' :(.text.startup+0xe31): undefined reference to `memory::finalize()' :(.text.startup+0xe70): undefined reference to `memory::exit_when_out_of_memory(bool, char const*)' :(.text.startup+0xf4a): undefined reference to `memory::finalize()' :(.text.startup+0xfab): undefined reference to `z3_exception::has_error_code() const' :(.text.startup+0x151f): undefined reference to `warning_msg(char const*, ...)' :(.text.startup+0x168e): undefined reference to `set_timeout(long)' :(.text.startup+0x1740): undefined reference to `param_vector::dec_ref()' :(.text.startup+0x18f9): undefined reference to `enable_warning_messages(bool)' :(.text.startup+0x1993): undefined reference to `ini_params::display_params_documentation(std::ostream&) const' :(.text.startup+0x19ab): undefined reference to `ini_params::display_params(std::ostream&) const' /tmp/ccjrQz3Z.ltrans0.ltrans.o:(.data.DW.ref._ZTI12z3_exception[DW.ref._ZTI12z3_exception]+0x0): undefined reference to `typeinfo for z3_exception' /tmp/ccjrQz3Z.ltrans1.ltrans.o: In function `on_ctrl_c(int) [clone .lto_priv.36]': :(.text+0x81): undefined reference to `ini_params::display_params(std::ostream&) const' :(.text+0xec): undefined reference to `smtlib::solver::display_statistics()' :(.text+0xf4): undefined reference to `memory::display_max_usage(std::ostream&)' :(.text+0x18f): undefined reference to `stream_ref::set(char const*)' :(.text+0x1c2): undefined reference to `cmd_context::display_statistics(bool, double)' /tmp/ccjrQz3Z.ltrans1.ltrans.o: In function `read_datalog(char const*, datalog_params const&, front_end_params&) [clone .constprop.5]': :(.text+0x21b): undefined reference to `get_verbosity_level()' :(.text+0x23e): undefined reference to `ast_manager::ast_manager(proof_gen_mode, std::ostream*, bool)' :(.text+0x257): undefined reference to `register_on_timeout_proc(void (*)())' :(.text+0x292): undefined reference to `symbol::symbol(char const*)' :(.text+0x2ae): undefined reference to `params_ref::set_sym(char const*, symbol const&)' :(.text+0x2c1): undefined reference to `params_ref::set_sym(char const*, symbol const&)' :(.text+0x2d4): undefined reference to `params_ref::set_bool(char const*, bool)' :(.text+0x2e7): undefined reference to `datalog::context::context(ast_manager&, front_end_params&, params_ref const&)' :(.text+0x2fd): undefined reference to `memory::set_high_watermark(unsigned long)' :(.text+0x319): undefined reference to `symbol::symbol(char const*)' :(.text+0x32a): undefined reference to `datalog::relation_manager::get_relation_plugin(symbol const&)' :(.text+0x337): undefined reference to `memory::allocate(unsigned long)' :(.text+0x351): undefined reference to `datalog::finite_product_relation_plugin::finite_product_relation_plugin(datalog::relation_plugin&, datalog::relation_manager&)' :(.text+0x360): undefined reference to `datalog::relation_manager::register_relation_plugin_impl(datalog::relation_plugin*)' :(.text+0x39b): undefined reference to `datalog::is_directory(std::__cxx11::basic_string, std::allocator >)' :(.text+0x3c7): undefined reference to `datalog::wpa_parser::create(datalog::context&, ast_manager&)' :(.text+0x3ed): undefined reference to `datalog::parser::create(datalog::context&, ast_manager&)' :(.text+0x451): undefined reference to `get_verbosity_level()' :(.text+0x45a): undefined reference to `verbose_stream()' :(.text+0x46e): undefined reference to `get_verbosity_level()' :(.text+0x496): undefined reference to `datalog::context::close()' :(.text+0x4a7): undefined reference to `datalog::rule_set::rule_set(datalog::rule_set const&)' :(.text+0x4b1): undefined reference to `memory::allocate(unsigned long)' :(.text+0x578): undefined reference to `datalog::context::collect_predicates(hashtable, ptr_eq >&)' :(.text+0x5c6): undefined reference to `datalog::execution_context::execution_context(datalog::context&)' :(.text+0x5dc): undefined reference to `get_verbosity_level()' :(.text+0x648): undefined reference to `params_ref::get_uint(char const*, unsigned int) const' :(.text+0x6c3): undefined reference to `datalog::context::transform_rules(ref&, ref&)' :(.text+0x6ea): undefined reference to `memory::allocate(unsigned long)' :(.text+0x861): undefined reference to `memory::allocate(unsigned long)' :(.text+0x9c3): undefined reference to `datalog::compiler::do_compilation(datalog::instruction_block&, datalog::instruction_block&)' :(.text+0x9d5): undefined reference to `memory::deallocate(void*)' :(.text+0xa0e): undefined reference to `memory::deallocate(void*)' :(.text+0xa28): undefined reference to `memory::deallocate(void*)' :(.text+0xa3a): undefined reference to `memory::deallocate(void*)' :(.text+0xa45): undefined reference to `datalog::instruction_block::make_annotations(datalog::execution_context&)' :(.text+0xa50): undefined reference to `datalog::execution_context::set_timelimit(unsigned int)' :(.text+0xa5b): undefined reference to `datalog::instruction_block::perform(datalog::execution_context&) const' :(.text+0xa67): undefined reference to `get_verbosity_level()' :(.text+0xa71): undefined reference to `verbose_stream()' :(.text+0xa81): undefined reference to `datalog::execution_context::report_big_relations(unsigned int, std::ostream&)' :(.text+0xa86): undefined reference to `memory::above_high_watermark()' :(.text+0xa96): undefined reference to `datalog::execution_context::reset_timelimit()' :(.text+0xaa2): undefined reference to `datalog::instruction_block::perform(datalog::execution_context&) const' :(.text+0xab8): undefined reference to `get_verbosity_level()' :(.text+0xac1): undefined reference to `verbose_stream()' :(.text+0xaeb): undefined reference to `params_ref::get_uint(char const*, unsigned int) const' :(.text+0xb0c): undefined reference to `datalog::instruction_block::process_all_costs()' :(.text+0xb14): undefined reference to `datalog::instruction_block::reset()' :(.text+0xb1d): undefined reference to `datalog::instruction_block::reset()' :(.text+0xb25): undefined reference to `datalog::execution_context::reset()' :(.text+0xb2d): undefined reference to `datalog::context::reopen()' :(.text+0xb3a): undefined reference to `datalog::context::restrict_predicates(hashtable, ptr_eq > const&)' :(.text+0xb47): undefined reference to `datalog::context::replace_rules(datalog::rule_set&)' :(.text+0xb4f): undefined reference to `datalog::context::close()' :(.text+0xb9a): undefined reference to `params_ref::get_bool(char const*, bool) const' :(.text+0xbb1): undefined reference to `datalog::relation_manager::display_output_tables(std::ostream&) const' :(.text+0xbce): undefined reference to `register_on_timeout_proc(void (*)())' :(.text+0xbd9): undefined reference to `datalog::execution_context::~execution_context()' :(.text+0xbe2): undefined reference to `datalog::instruction_block::~instruction_block()' :(.text+0xbea): undefined reference to `datalog::instruction_block::~instruction_block()' :(.text+0xbfc): undefined reference to `memory::deallocate(void*)' :(.text+0xc06): undefined reference to `datalog::rule_set::~rule_set()' :(.text+0xc0e): undefined reference to `datalog::context::~context()' :(.text+0xc18): undefined reference to `params_ref::~params_ref()' :(.text+0xc22): undefined reference to `ast_manager::~ast_manager()' :(.text+0xc4d): undefined reference to `memory::deallocate(void*)' :(.text+0xc6d): undefined reference to `memory::deallocate(void*)' :(.text+0xcb1): undefined reference to `verbose_stream()' :(.text+0xcf8): undefined reference to `verbose_stream()' :(.text+0xd16): undefined reference to `datalog::rule_set::display_deps(std::ostream&) const' :(.text+0xd20): undefined reference to `verbose_stream()' :(.text+0xe10): undefined reference to `datalog::rule_set::~rule_set()' :(.text+0xe18): undefined reference to `datalog::context::~context()' :(.text+0xe22): undefined reference to `params_ref::~params_ref()' :(.text+0xe2c): undefined reference to `ast_manager::~ast_manager()' :(.text+0xeeb): undefined reference to `datalog::instruction_block::~instruction_block()' :(.text+0xf01): undefined reference to `memory::deallocate(void*)' :(.text+0xf19): undefined reference to `datalog::execution_context::~execution_context()' :(.text+0xf22): undefined reference to `datalog::instruction_block::~instruction_block()' :(.text+0xf7a): undefined reference to `memory::deallocate(void*)' :(.text+0xfa6): undefined reference to `out_of_memory_error::out_of_memory_error()' :(.text+0xfc3): undefined reference to `fatal_error(int)' :(.text+0x1033): undefined reference to `memory::deallocate(void*)' :(.text+0x1052): undefined reference to `memory::deallocate(void*)' :(.text+0x107f): undefined reference to `memory::deallocate(void*)' :(.text+0x1096): undefined reference to `memory::deallocate(void*)' :(.text+0x10a8): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans1.ltrans.o::(.text+0x10e6): more undefined references to `memory::deallocate(void*)' follow /tmp/ccjrQz3Z.ltrans1.ltrans.o: In function `read_smtlib_file(char const*, front_end_params&)': :(.text+0x1128): undefined reference to `register_on_timeout_proc(void (*)())' :(.text+0x1144): undefined reference to `smtlib::solver::solver(front_end_params&)' :(.text+0x1156): undefined reference to `smtlib::solver::solve_smt(char const*)' :(.text+0x11a0): undefined reference to `register_on_timeout_proc(void (*)())' :(.text+0x11ba): undefined reference to `smtlib::solver::~solver()' :(.text+0x11e8): undefined reference to `smtlib::solver::~solver()' /tmp/ccjrQz3Z.ltrans1.ltrans.o: In function `read_smtlib2_commands(char const*, front_end_params&)': :(.text+0x122f): undefined reference to `register_on_timeout_proc(void (*)())' :(.text+0x1247): undefined reference to `symbol::null' :(.text+0x1259): undefined reference to `cmd_context::cmd_context(front_end_params*, bool, ast_manager*, symbol const&)' :(.text+0x1270): undefined reference to `memory::allocate(unsigned long)' :(.text+0x128c): undefined reference to `solver_na2as::solver_na2as()' :(.text+0x1293): undefined reference to `vtable for tactic_factory2solver' :(.text+0x12d1): undefined reference to `memory::allocate(unsigned long)' :(.text+0x12eb): undefined reference to `tactic_factory2solver::set_tactic(tactic_factory*)' :(.text+0x12f6): undefined reference to `cmd_context::set_solver(solver*)' :(.text+0x12fe): undefined reference to `install_dl_cmds(cmd_context&)' :(.text+0x1306): undefined reference to `install_dbg_cmds(cmd_context&)' :(.text+0x130e): undefined reference to `install_polynomial_cmds(cmd_context&)' :(.text+0x1316): undefined reference to `install_subpaving_cmds(cmd_context&)' :(.text+0x1329): undefined reference to `register_on_timeout_proc(void (*)())' :(.text+0x13c9): undefined reference to `parse_smt2_commands(cmd_context&, std::istream&, bool)' :(.text+0x13eb): undefined reference to `cmd_context::~cmd_context()' :(.text+0x1408): undefined reference to `mk_smt_strategic_solver(bool)' :(.text+0x1413): undefined reference to `cmd_context::set_solver(solver*)' :(.text+0x142c): undefined reference to `parse_smt2_commands(cmd_context&, std::istream&, bool)' :(.text+0x1443): undefined reference to `cmd_context::~cmd_context()' /tmp/ccjrQz3Z.ltrans1.ltrans.o: In function `void dealloc(datalog::wpa_parser*) [clone .constprop.15]': :(.text+0x13): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans1.ltrans.o: In function `void dealloc(datalog::parser*) [clone .constprop.14]': :(.text+0x33): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans1.ltrans.o: In function `vector::destroy() [clone .constprop.11]': :(.text.unlikely+0x28): undefined reference to `memory::deallocate(void*)' :(.text.unlikely+0x3f): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans1.ltrans.o:(.data.rel.ro+0x88): undefined reference to `typeinfo for z3_error' /tmp/ccjrQz3Z.ltrans2.ltrans.o: In function `display_statistics(std::ostream&, datalog::context&, datalog::rule_set&, datalog::instruction_block&, datalog::execution_context&, front_end_params&, bool) [clone .constprop.20]': :(.text+0xe4): undefined reference to `datalog::instruction_block::process_all_costs()' :(.text+0xf0): undefined reference to `params_ref::params_ref(params_ref const&)' :(.text+0x104): undefined reference to `params_ref::set_bool(char const*, bool)' :(.text+0x118): undefined reference to `params_ref::set_uint(char const*, unsigned int)' :(.text+0x123): undefined reference to `datalog::context::updt_params(params_ref const&)' :(.text+0x15d): undefined reference to `datalog::rule_set::display(std::ostream&) const' :(.text+0x197): undefined reference to `datalog::rule_set::display(std::ostream&) const' :(.text+0x1ec): undefined reference to `datalog::instruction_block::display_indented(datalog::context&, std::ostream&, std::__cxx11::basic_string, std::allocator >) const' :(.text+0x238): undefined reference to `datalog::execution_context::report_big_relations(unsigned int, std::ostream&)' :(.text+0x240): undefined reference to `params_ref::~params_ref()' :(.text+0x277): undefined reference to `datalog::relation_manager::display_relation_sizes(std::ostream&) const' :(.text+0x2b1): undefined reference to `datalog::rule_set::display(std::ostream&) const' :(.text+0x4d8): undefined reference to `params_ref::~params_ref()' /tmp/ccjrQz3Z.ltrans3.ltrans.o: In function `display_statistics()': :(.text+0xc6): undefined reference to `sat::solver::collect_statistics(statistics&)' :(.text+0xf7): undefined reference to `statistics::update(char const*, double)' :(.text+0x102): undefined reference to `statistics::display_smt2(std::ostream&) const' :(.text+0x115): undefined reference to `memory::deallocate(void*)' :(.text+0x12b): undefined reference to `memory::deallocate(void*)' :(.text+0x158): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans3.ltrans.o: In function `on_ctrl_c(int)': :(.text+0x1ed): undefined reference to `sat::solver::collect_statistics(statistics&)' :(.text+0x21e): undefined reference to `statistics::update(char const*, double)' :(.text+0x229): undefined reference to `statistics::display_smt2(std::ostream&) const' :(.text+0x23c): undefined reference to `memory::deallocate(void*)' :(.text+0x252): undefined reference to `memory::deallocate(void*)' :(.text+0x27f): undefined reference to `memory::deallocate(void*)' /tmp/ccjrQz3Z.ltrans3.ltrans.o: In function `display_statistics() [clone .lto_priv.40]': :(.text+0x2b5): undefined reference to `ini_params::display_params(std::ostream&) const' :(.text+0x307): undefined reference to `smtlib::solver::display_statistics()' :(.text+0x30f): undefined reference to `memory::display_max_usage(std::ostream&)' :(.text+0x396): undefined reference to `stream_ref::set(char const*)' /tmp/ccjrQz3Z.ltrans3.ltrans.o: In function `read_dimacs(char const*, front_end_params&)': :(.text+0x43c): undefined reference to `register_on_timeout_proc(void (*)())' :(.text+0x46c): undefined reference to `params_ref::set_bool(char const*, bool)' :(.text+0x481): undefined reference to `sat::solver::solver(params_ref const&, sat::extension*)' :(.text+0x517): undefined reference to `parse_dimacs(std::istream&, sat::solver&)' :(.text+0x524): undefined reference to `get_verbosity_level()' :(.text+0x531): undefined reference to `sat::solver::check()' :(.text+0x55d): undefined reference to `sat::solver::~solver()' :(.text+0x565): undefined reference to `params_ref::~params_ref()' :(.text+0x57c): undefined reference to `verbose_stream()' :(.text+0x587): undefined reference to `sat::solver::display_status(std::ostream&) const' :(.text+0x660): undefined reference to `parse_dimacs(std::istream&, sat::solver&)' :(.text+0x681): undefined reference to `params_ref::~params_ref()' :(.text+0x6a2): undefined reference to `sat::solver::~solver()' /tmp/ccjrQz3Z.ltrans3.ltrans.o: In function `qfnra_nlsat_fct::operator()(ast_manager&, params_ref const&)': :(.text+0x47): undefined reference to `mk_qfnra_nlsat_tactic(ast_manager&, params_ref const&)' /tmp/ccjrQz3Z.ltrans3.ltrans.o: In function `display_statistics() [clone .lto_priv.40]': :(.text+0x3cf): undefined reference to `cmd_context::display_statistics(bool, double)' /tmp/ccjrQz3Z.ltrans3.ltrans.o: In function `statistics::~statistics()': :(.text.unlikely+0x28): undefined reference to `memory::deallocate(void*)' :(.text.unlikely+0x3e): undefined reference to `memory::deallocate(void*)' :(.text.unlikely+0x1f): undefined reference to `memory::deallocate(void*)' collect2: error: ld returned 1 exit status Makefile:8804: recipe for target 'z3' failed make[1]: *** [z3] Error 1 make[1]: Leaving directory '/home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/z3-4.3.1/build' [LD:esolver] esolver-synthlib /usr/bin/ld: cannot find -lz3 collect2: error: ld returned 1 exit status Makefile:120: recipe for target '/home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/bin/opt/esolver-synthlib' failed make: *** [/home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/bin/opt/esolver-synthlib] Error 1 `

Could you please checkout this branch: fix/remove-lto-builds-from-z3 and see if that works?

On Mon, Apr 16, 2018 at 11:18 AM, alaa-megahed notifications@github.com wrote:

After "make distclean" and "make eopt" commands, this is the full console output:

`[DEP:esolver] Z3TheoremProver.cpp [DEP:esolver] Z3Objects.cpp [DEP:esolver] ValueManager.cpp [DEP:esolver] UserExpression.cpp [DEP:esolver] UIDGenerator.cpp [DEP:esolver] TypeManager.cpp [DEP:esolver] TimeValue.cpp [DEP:esolver] TheoremProver.cpp [DEP:esolver] SynthLib2Solver.cpp [DEP:esolver] SymPartitionGenerator.cpp [DEP:esolver] SpookyHash.cpp [DEP:esolver] SpecRewriter.cpp [DEP:esolver] Signature.cpp [DEP:esolver] ScopeManager.cpp [DEP:esolver] ResourceLimitManager.cpp [DEP:esolver] PartitionGenerator.cpp [DEP:esolver] Operators.cpp [DEP:esolver] MemStats.cpp [DEP:esolver] Logger.cpp [DEP:esolver] LIALogic.cpp [DEP:esolver] Indent.cpp [DEP:esolver] GrammarNodes.cpp [DEP:esolver] Grammar.cpp [DEP:esolver] GenExpression.cpp [DEP:esolver] Gatherers.cpp [DEP:esolver] GNCostPair.cpp [DEP:esolver] FunctorBase.cpp [DEP:esolver] ExpressionVisitorBase.cpp [DEP:esolver] ExprManager.cpp [DEP:esolver] ExpCheckers.cpp [DEP:esolver] EvalRule.cpp [DEP:esolver] EnumeratorBase.cpp [DEP:esolver] ESolverScope.cpp [DEP:esolver] ESolverLogic.cpp [DEP:esolver] ESolver.cpp [DEP:esolver] ESType.cpp [DEP:esolver] ESException.cpp [DEP:esolver] CrossProductGenerator.cpp [DEP:esolver] ConstManager.cpp [DEP:esolver] ConcreteValueBase.cpp [DEP:esolver] ConcreteEvaluator.cpp [DEP:esolver] CFGEnumerator.cpp [DEP:esolver] CEGSolver.cpp [DEP:esolver] Builtins.cpp [DEP:esolver] BVLogic.cpp [CXX:esolver] BVLogic.cpp --> BVLogic.o [CXX:esolver] Builtins.cpp --> Builtins.o [CXX:esolver] CEGSolver.cpp --> CEGSolver.o [CXX:esolver] CFGEnumerator.cpp --> CFGEnumerator.o [CXX:esolver] ConcreteEvaluator.cpp --> ConcreteEvaluator.o [CXX:esolver] ConcreteValueBase.cpp --> ConcreteValueBase.o [CXX:esolver] ConstManager.cpp --> ConstManager.o [CXX:esolver] CrossProductGenerator.cpp --> CrossProductGenerator.o [CXX:esolver] ESException.cpp --> ESException.o [CXX:esolver] ESType.cpp --> ESType.o [CXX:esolver] ESolver.cpp --> ESolver.o [CXX:esolver] ESolverLogic.cpp --> ESolverLogic.o [CXX:esolver] ESolverScope.cpp --> ESolverScope.o [CXX:esolver] EnumeratorBase.cpp --> EnumeratorBase.o [CXX:esolver] EvalRule.cpp --> EvalRule.o [CXX:esolver] ExpCheckers.cpp --> ExpCheckers.o [CXX:esolver] ExprManager.cpp --> ExprManager.o [CXX:esolver] ExpressionVisitorBase.cpp --> ExpressionVisitorBase.o [CXX:esolver] FunctorBase.cpp --> FunctorBase.o [CXX:esolver] GNCostPair.cpp --> GNCostPair.o [CXX:esolver] Gatherers.cpp --> Gatherers.o [CXX:esolver] GenExpression.cpp --> GenExpression.o [CXX:esolver] Grammar.cpp --> Grammar.o [CXX:esolver] GrammarNodes.cpp --> GrammarNodes.o [CXX:esolver] Indent.cpp --> Indent.o [CXX:esolver] LIALogic.cpp --> LIALogic.o [CXX:esolver] Logger.cpp --> Logger.o [CXX:esolver] MemStats.cpp --> MemStats.o [CXX:esolver] Operators.cpp --> Operators.o [CXX:esolver] PartitionGenerator.cpp --> PartitionGenerator.o [CXX:esolver] ResourceLimitManager.cpp --> ResourceLimitManager.o [CXX:esolver] ScopeManager.cpp --> ScopeManager.o [CXX:esolver] Signature.cpp --> Signature.o [CXX:esolver] SpecRewriter.cpp --> SpecRewriter.o [CXX:esolver] SpookyHash.cpp --> SpookyHash.o [CXX:esolver] SymPartitionGenerator.cpp --> SymPartitionGenerator.o [CXX:esolver] SynthLib2Solver.cpp --> SynthLib2Solver.o [CXX:esolver] TheoremProver.cpp --> TheoremProver.o [CXX:esolver] TimeValue.cpp --> TimeValue.o [CXX:esolver] TypeManager.cpp --> TypeManager.o [CXX:esolver] UIDGenerator.cpp --> UIDGenerator.o [CXX:esolver] UserExpression.cpp --> UserExpression.o [CXX:esolver] ValueManager.cpp --> ValueManager.o [CXX:esolver] Z3Objects.cpp --> Z3Objects.o [CXX:esolver] Z3TheoremProver.cpp --> Z3TheoremProver.o [AR:esolver] libesolver.a [LD:esolver] libesolver.so make eopt -C /home/alaa/sygus-comp14/solvers/enumerative/esolver- synth-lib/src/synthlib2parser make[1]: Entering directory '/home/alaa/sygus-comp14/ solvers/enumerative/esolver-synth-lib/src/synthlib2parser' [DEP:synthlib2parser] PrintVisitor.cpp [DEP:synthlib2parser] SynthLib2ParserExceptions.cpp [DEP:synthlib2parser] SynthLib2ParserAST.cpp [bison:synthlib2parser] SynthLib2Parser.y --> SynthLib2Parser.tab.cpp [CXX:synthlib2parser] SynthLib2Parser.tab.cpp --> SynthLib2Parser.tab.o src/SynthLib2Parser.tab.cpp: In function ‘int yyparse()’: src/SynthLib2Parser.tab.cpp:2161:35: warning: ISO C++ forbids converting a string constant to ‘char’ [-Wpedantic] yyerror (YY_("syntax error")); ^ src/SynthLib2Parser.tab.cpp:2305:35: warning: ISO C++ forbids converting a string constant to ‘char’ [-Wpedantic] yyerror (YY_("memory exhausted")); ^ [flex:synthlib2parser] SynthLib2Lexer.l --> SynthLib2Lexer.cpp [CXX:synthlib2parser] SynthLib2Lexer.cpp --> SynthLib2Lexer.o src/SynthLib2Lexer.cpp: In function ‘int yy_get_next_buffer()’: src/SynthLib2Lexer.cpp:1360:44: warning: comparison between signed and unsigned integer expressions [-Wsign-compare] if ((int) ((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFERLVALUE->yy buf_s ^ [CXX:synthlib2parser] SynthLib2ParserAST.cpp --> SynthLib2ParserAST.o [CXX:synthlib2parser] SynthLib2ParserExceptions.cpp --> SynthLib2ParserExceptions.o [CXX:synthlib2parser] PrintVisitor.cpp --> PrintVisitor.o [AR:synthlib2parser] libsynthlib2parser.a [LD:synthlib2parser] libsynthlib2parser.so make[1]: Leaving directory '/home/alaa/sygus-comp14/ solvers/enumerative/esolver-synth-lib/src/synthlib2parser' cp /home/alaa/sygus-comp14/solvers/enumerative/esolver- synth-lib/src/synthlib2parser/lib/opt/libsynthlib2parser.so /home/alaa/sygus-comp14/solvers/enumerative/esolver- synth-lib/src/synthlib2parser/lib/opt/libsynthlib2parser.a /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/lib/opt touch /home/alaa/sygus-comp14/solvers/enumerative/esolver- synth-lib/lib/opt/slparserlib.ph [DEP:esolver] ESolverSynthLib.cpp [CXX:esolver] ESolverSynthLib.cpp --> ESolverSynthLib.o cd /home/alaa/sygus-comp14/solvers/enumerative/esolver-synth-lib/src/z3-4.3.1;

autoconf; ./configure; python scripts/mk_make.py; cd build; make; touch /home/alaa/sygus-comp14/solvers/enumerative/esolver- synth-lib/src/z3-4.3.1/build/z3build.ph checking for g++... g++ checking whether we are using the GNU C++ compiler... no checking whether g++ accepts -g... no checking for gcc... gcc checking whether we are using the GNU C compiler... no checking whether gcc accepts -g... no checking for gcc option to accept ISO C89... unsupported checking whether make sets $(MAKE)... yes checking for grep that handles long lines and -e... /bin/grep checking for a sed that does not truncate output... /bin/sed checking size of int *... 8 configure: creating ./config.status config.status: creating scripts/config-debug.mk config.status: creating scripts/config-release.mk Z3 was configured with success. Host platform: linux Compiler: g++ Arithmetic: internal Python: python Prefix: /usr 64-bit: yes

To build and install Z3, execute: python scripts/mk_make.py cd build make sudo make install Fixing end of line... New component: 'util' New component: 'polynomial' New component: 'sat' New component: 'nlsat' New component: 'interval' New component: 'subpaving' New component: 'ast' New component: 'rewriter' New component: 'model' New component: 'tactic' New component: 'substitution' New component: 'parser_util' New component: 'grobner' New component: 'euclid' New component: 'front_end_params' New component: 'simplifier' New component: 'normal_forms' New component: 'core_tactics' New component: 'sat_tactic' New component: 'arith_tactics' New component: 'nlsat_tactic' New component: 'subpaving_tactic' New component: 'aig_tactic' New component: 'solver' New component: 'cmd_context' New component: 'extra_cmds' New component: 'smt2parser' New component: 'pattern' New component: 'macros' New component: 'proof_checker' New component: 'bit_blaster' New component: 'proto_model' New component: 'smt' New component: 'user_plugin' New component: 'bv_tactics' New component: 'fuzzing' New component: 'fpa' New component: 'smt_tactic' New component: 'sls_tactic' New component: 'muz_qe' New component: 'smtlogic_tactics' New component: 'ufbv_tactic' New component: 'portfolio' New component: 'smtparser' New component: 'api' New component: 'shell' New component: 'test' New component: 'api_dll' New component: 'api_static_lib' New component: 'dotnet' New component: 'cpp' Python bindinds directory was detected. New component: 'cpp_example' New component: 'c_example' New component: 'maxsat' New component: 'dotnet_example' New component: 'py_example' Generated 'src/util/version.h' Updated 'src/api/dotnet/Properties/AssemblyInfo.cs' Generated 'src/ast/pattern/database.h' Generated 'src/shell/install_tactic.cpp' Generated 'src/test/install_tactic.cpp' Generated 'src/api/dll/install_tactic.cpp' Generated 'src/api/staticlib/install_tactic.cpp' Generated 'src/api/python/z3consts.py' Generated 'src/api/dotnet/Enumerations.cs' Generated 'src/api/api_log_macros.h' Generated 'src/api/api_log_macros.cpp' Generated 'src/api/api_commands.cpp' Generated 'src/api/python/z3core.py' Generated 'src/api/dotnet/Native.cs' Listing src/api/python ... Compiling src/api/python/z3.py ... Compiling src/api/python/z3consts.py ... Compiling src/api/python/z3core.py ... Compiling src/api/python/z3printer.py ... Compiling src/api/python/z3test.py ... Compiling src/api/python/z3types.py ... Generated 'z3consts.pyc' Generated 'z3types.pyc' Generated 'z3test.pyc' Generated 'z3printer.pyc' Generated 'z3core.pyc' Generated 'z3.pyc' Writing build/Makefile Copied Z3Py example 'example.py' to 'build' Makefile was successfully generated. python packages dir: /usr/lib/python2.7/dist-packages compilation mode: Release Type 'cd build; make' to build Z3 make[1]: Entering directory '/home/alaa/sygus-comp14/ solvers/enumerative/esolver-synth-lib/src/z3-4.3.1/build' src/shell/datalog_frontend.cpp --> shell/datalog_frontend-lto.o src/shell/z3_log_frontend.cpp --> shell/z3_log_frontend-lto.o src/shell/main.cpp --> shell/main-lto.o src/shell/install_tactic.cpp --> shell/install_tactic-lto.o src/shell/dimacs_frontend.cpp --> shell/dimacs_frontend-lto.o src/shell/smtlib_frontend.cpp --> shell/smtlib_frontend-lto.o src/api/api_datalog.cpp --> api/api_datalog-lto.o src/api/api_tactic.cpp --> api/api_tactic-lto.o src/api/api_goal.cpp --> api/api_goal-lto.o src/api/api_ast.cpp --> api/api_ast-lto.o src/api/api_bv.cpp --> api/api_bv-lto.o src/api/api_commands.cpp --> api/api_commands-lto.o src/api/api_ast_map.cpp --> api/api_ast_map-lto.o src/api/api_ast_vector.cpp --> api/api_ast_vector-lto.o src/api/api_context.cpp --> api/api_context-lto.o src/api/api_solver.cpp --> api/api_solver-lto.o src/api/api_log_macros.cpp --> api/api_log_macros-lto.o src/api/api_config_params.cpp --> api/api_config_params-lto.o src/api/api_quant.cpp --> api/api_quant-lto.o src/api/api_user_theory.cpp --> api/api_user_theory-lto.o src/api/api_parsers.cpp --> api/api_parsers-lto.o src/api/api_arith.cpp --> api/api_arith-lto.o src/api/api_numeral.cpp --> api/api_numeral-lto.o src/api/api_stats.cpp --> api/api_stats-lto.o src/api/api_datatype.cpp --> api/api_datatype-lto.o src/api/z3_replayer.cpp --> api/z3_replayer-lto.o src/api/api_params.cpp --> api/api_params-lto.o src/api/api_solver_old.cpp --> api/api_solver_old-lto.o src/api/api_log.cpp --> api/api_log-lto.o src/api/api_model.cpp --> api/api_model-lto.o src/api/api_array.cpp --> api/api_array-lto.o api/api-lto.a ar: api/api_datalog-lto.o: plugin needed to handle lto object ar: api/api_tactic-lto.o: plugin needed to handle lto object ar: api/api_goal-lto.o: plugin needed to handle lto object ar: api/api_ast-lto.o: plugin needed to handle lto object ar: api/api_bv-lto.o: plugin needed to handle lto object ar: api/api_commands-lto.o: plugin needed to handle lto object ar: api/api_ast_map-lto.o: plugin needed to handle lto object ar: api/api_ast_vector-lto.o: plugin needed to handle lto object ar: api/api_context-lto.o: plugin needed to handle lto object ar: api/api_solver-lto.o: plugin needed to handle lto object ar: api/api_log_macros-lto.o: plugin needed to handle lto object ar: api/api_config_params-lto.o: plugin needed to handle lto object ar: api/api_quant-lto.o: plugin needed to handle lto object ar: api/api_user_theory-lto.o: plugin needed to handle lto object ar: api/api_parsers-lto.o: plugin needed to handle lto object ar: api/api_arith-lto.o: plugin needed to handle lto object ar: api/api_numeral-lto.o: plugin needed to handle lto object ar: api/api_stats-lto.o: plugin needed to handle lto object ar: api/api_datatype-lto.o: plugin needed to handle lto object ar: api/z3_replayer-lto.o: plugin needed to handle lto object ar: api/api_params-lto.o: plugin needed to handle lto object ar: api/api_solver_old-lto.o: plugin needed to handle lto object ar: api/api_log-lto.o: plugin needed to handle lto object ar: api/api_model-lto.o: plugin needed to handle lto object ar: api/api_array-lto.o: plugin needed to handle lto object src/parsers/smt/smtlib_solver.cpp --> parsers/smt/smtlib_solver-lto.o src/parsers/smt/smtlib.cpp --> parsers/smt/smtlib-lto.o src/parsers/smt/smtparser.cpp --> parsers/smt/smtparser-lto.o parsers/smt/smtparser-lto.a ar: parsers/smt/smtlib_solver-lto.o: plugin needed to handle lto object ar: parsers/smt/smtlib-lto.o: plugin needed to handle lto object ar: parsers/smt/smtparser-lto.o: plugin needed to handle lto object src/tactic/portfolio/defaulttactic.cpp --> tactic/portfolio/default tactic-lto.o src/tactic/portfolio/smt_strategicsolver.cpp --> tactic/portfolio/smt strategic_solver-lto.o tactic/portfolio/portfolio-lto.a ar: tactic/portfolio/default_tactic-lto.o: plugin needed to handle lto object ar: tactic/portfolio/smt_strategic_solver-lto.o: plugin needed to handle lto object src/tactic/ufbv/ufbv_rewriter_tactic.cpp --> tactic/ufbv/ufbvrewriter tactic-lto.o src/tactic/ufbv/ufbv_rewriter.cpp --> tactic/ufbv/ufbv_rewriter-lto.o src/tactic/ufbv/ufbv_tactic.cpp --> tactic/ufbv/ufbv_tactic-lto.o src/tactic/ufbv/quasi_macros_tactic.cpp --> tactic/ufbv/quasimacros tactic-lto.o src/tactic/ufbv/macro_finder_tactic.cpp --> tactic/ufbv/macrofinder tactic-lto.o tactic/ufbv/ufbv_tactic-lto.a ar: tactic/ufbv/ufbv_rewriter_tactic-lto.o: plugin needed to handle lto object ar: tactic/ufbv/ufbv_rewriter-lto.o: plugin needed to handle lto object ar: tactic/ufbv/ufbv_tactic-lto.o: plugin needed to handle lto object ar: tactic/ufbv/quasi_macros_tactic-lto.o: plugin needed to handle lto object ar: tactic/ufbv/macro_finder_tactic-lto.o: plugin needed to handle lto object src/tactic/smtlogics/qfaufliatactic.cpp --> tactic/smtlogics/qfauflia tactic-lto.o src/tactic/smtlogics/quanttactics.cpp --> tactic/smtlogics/quant tactics-lto.o src/tactic/smtlogics/qfbv_tactic.cpp --> tactic/smtlogics/qfbv_tactic- lto.o src/tactic/smtlogics/qflia_tactic.cpp --> tactic/smtlogics/qflia_tactic- lto.o src/tactic/smtlogics/qfnia_tactic.cpp --> tactic/smtlogics/qfnia_tactic- lto.o src/tactic/smtlogics/qflra_tactic.cpp --> tactic/smtlogics/qflra_tactic- lto.o src/tactic/smtlogics/qfufbvtactic.cpp --> tactic/smtlogics/qfufbv tactic-lto.o src/tactic/smtlogics/qfaufbvtactic.cpp --> tactic/smtlogics/qfaufbv tactic-lto.o src/tactic/smtlogics/nra_tactic.cpp --> tactic/smtlogics/nra_tactic-lto.o src/tactic/smtlogics/qfidl_tactic.cpp --> tactic/smtlogics/qfidl_tactic- lto.o src/tactic/smtlogics/qfuf_tactic.cpp --> tactic/smtlogics/qfuf_tactic- lto.o src/tactic/smtlogics/qfnra_tactic.cpp --> tactic/smtlogics/qfnra_tactic- lto.o tactic/smtlogics/smtlogic_tactics-lto.a ar: tactic/smtlogics/qfauflia_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/quant_tactics-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfbv_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qflia_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfnia_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qflra_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfufbv_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfaufbv_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/nra_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfidl_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfuf_tactic-lto.o: plugin needed to handle lto object ar: tactic/smtlogics/qfnra_tactic-lto.o: plugin needed to handle lto object src/muz_qe/dl_skip_table.cpp --> muz_qe/dl_skip_table-lto.o src/muz_qe/qe_sat_tactic.cpp --> muz_qe/qe_sat_tactic-lto.o src/muz_qe/dl_rule.cpp --> muz_qe/dl_rule-lto.o src/muz_qe/dl_costs.cpp --> muz_qe/dl_costs-lto.o src/muz_qe/dl_cmds.cpp --> muz_qe/dl_cmds-lto.o src/muz_qe/imdd.cpp --> muz_qe/imdd-lto.o src/muz_qe/dl_mk_simple_joins.cpp --> muz_qe/dl_mk_simple_joins-lto.o src/muz_qe/vsubst_tactic.cpp --> muz_qe/vsubst_tactic-lto.o src/muz_qe/dl_interval_relation.cpp --> muz_qe/dl_interval_relation-lto.o src/muz_qe/dl_mk_unbound_compressor.cpp --> muz_qe/dl_mkunbound compressor-lto.o src/muz_qe/qe_dl_plugin.cpp --> muz_qe/qe_dl_plugin-lto.o src/muz_qe/dl_mk_coalesce.cpp --> muz_qe/dl_mk_coalesce-lto.o src/muz_qe/proof_utils.cpp --> muz_qe/proof_utils-lto.o src/muz_qe/qe_bv_plugin.cpp --> muz_qe/qe_bv_plugin-lto.o src/muz_qe/dl_util.cpp --> muz_qe/dl_util-lto.o src/muz_qe/dl_mk_explanations.cpp --> muz_qe/dl_mk_explanations-lto.o src/muz_qe/dl_mk_rule_inliner.cpp --> muz_qe/dl_mk_rule_inliner-lto.o src/muz_qe/dl_rule_transformer.cpp --> muz_qe/dl_rule_transformer-lto.o src/muz_qe/dl_mk_magic_sets.cpp --> muz_qe/dl_mk_magic_sets-lto.o src/muz_qe/model2expr.cpp --> muz_qe/model2expr-lto.o src/muz_qe/arith_bounds_tactic.cpp --> muz_qe/arith_bounds_tactic-lto.o src/muz_qe/dl_mk_partial_equiv.cpp --> muz_qe/dl_mk_partial_equiv-lto.o src/muz_qe/qe.cpp --> muz_qe/qe-lto.o src/muz_qe/dl_mk_unfold.cpp --> muz_qe/dl_mk_unfold-lto.o src/muz_qe/dl_mk_bit_blast.cpp --> muz_qe/dl_mk_bit_blast-lto.o src/muz_qe/dl_sieve_relation.cpp --> muz_qe/dl_sieve_relation-lto.o src/muz_qe/qe_bool_plugin.cpp --> muz_qe/qe_bool_plugin-lto.o src/muz_qe/datalog_parser.cpp --> muz_qe/datalog_parser-lto.o src/muz_qe/dl_rule_set.cpp --> muz_qe/dl_rule_set-lto.o src/muz_qe/dl_mk_subsumption_checker.cpp --> muz_qe/dl_mksubsumption checker-lto.o src/muz_qe/dl_bound_relation.cpp --> muz_qe/dl_bound_relation-lto.o src/muz_qe/pdr_prop_solver.cpp --> muz_qe/pdr_prop_solver-lto.o src/muz_qe/nlarith_util.cpp --> muz_qe/nlarith_util-lto.o src/muz_qe/replace_proof_converter.cpp --> muz_qe/replaceproof converter-lto.o src/muz_qe/dl_instruction.cpp --> muz_qe/dl_instruction-lto.o src/muz_qe/dl_base.cpp --> muz_qe/dl_base-lto.o src/muz_qe/dl_table.cpp --> muz_qe/dl_table-lto.o src/muz_qe/dl_bmc_engine.cpp --> muz_qe/dl_bmc_engine-lto.o src/muz_qe/qe_datatype_plugin.cpp --> muz_qe/qe_datatype_plugin-lto.o src/muz_qe/dl_mk_filter_rules.cpp --> muz_qe/dl_mk_filter_rules-lto.o src/muz_qe/dl_table_relation.cpp --> muz_qe/dl_table_relation-lto.o src/muz_qe/dl_relation_manager.cpp --> muz_qe/dl_relation_manager-lto.o src/muz_qe/qe_lite.cpp --> muz_qe/qe_lite-lto.o src/muz_qe/dl_mk_slice.cpp --> muz_qe/dl_mk_slice-lto.o src/muz_qe/horn_subsume_model_converter.cpp --> muz_qe/horn_subsumemodel converter-lto.o src/muz_qe/qe_arith_plugin.cpp --> muz_qe/qe_arith_plugin-lto.o src/muz_qe/dl_mk_coi_filter.cpp --> muz_qe/dl_mk_coi_filter-lto.o src/muz_qe/dl_finite_product_relation.cpp --> muz_qe/dl_finiteproduct relation-lto.o src/muz_qe/pdr_quantifiers.cpp --> muz_qe/pdr_quantifiers-lto.o src/muz_qe/dl_context.cpp --> muz_qe/dl_context-lto.o src/muz_qe/dl_compiler.cpp --> muz_qe/dl_compiler-lto.o src/muz_qe/pdr_dl_interface.cpp --> muz_qe/pdr_dl_interface-lto.o src/muz_qe/dl_smt_relation.cpp --> muz_qe/dl_smt_relation-lto.o src/muz_qe/pdr_reachable_cache.cpp --> muz_qe/pdr_reachable_cache-lto.o src/muz_qe/dl_rule_subsumption_index.cpp --> muz_qe/dl_rulesubsumption index-lto.o src/muz_qe/pdr_context.cpp --> muz_qe/pdr_context-lto.o src/muz_qe/qe_cmd.cpp --> muz_qe/qe_cmd-lto.o src/muz_qe/dl_external_relation.cpp --> muz_qe/dl_external_relation-lto.o src/muz_qe/dl_product_relation.cpp --> muz_qe/dl_product_relation-lto.o src/muz_qe/dl_check_table.cpp --> muz_qe/dl_check_table-lto.o src/muz_qe/pdr_sym_mux.cpp --> muz_qe/pdr_sym_mux-lto.o src/muz_qe/qe_array_plugin.cpp --> muz_qe/qe_array_plugin-lto.o src/muz_qe/dl_mk_similarity_compressor.cpp --> muz_qe/dl_mksimilarity compressor-lto.o src/muz_qe/pdr_smt_context_manager.cpp --> muz_qe/pdr_smtcontext manager-lto.o src/muz_qe/dl_mk_interp_tail_simplifier.cpp --> muz_qe/dl_mk_interptail simplifier-lto.o src/muz_qe/pdr_util.cpp --> muz_qe/pdr_util-lto.o src/muz_qe/pdr_generalizers.cpp --> muz_qe/pdr_generalizers-lto.o src/muz_qe/unit_subsumption_tactic.cpp --> muz_qe/unitsubsumption tactic-lto.o src/muz_qe/pdr_farkas_learner.cpp --> muz_qe/pdr_farkas_learner-lto.o src/muz_qe/pdr_interpolant_provider.cpp --> muz_qe/pdrinterpolant provider-lto.o src/muz_qe/qe_tactic.cpp --> muz_qe/qe_tactic-lto.o src/muz_qe/pdr_manager.cpp --> muz_qe/pdr_manager-lto.o src/muz_qe/dl_sparse_table.cpp --> muz_qe/dl_sparse_table-lto.o muz_qe/muz_qe-lto.a ar: muz_qe/dl_skip_table-lto.o: plugin needed to handle lto object ar: muz_qe/qe_sat_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/dl_rule-lto.o: plugin needed to handle lto object ar: muz_qe/dl_costs-lto.o: plugin needed to handle lto object ar: muz_qe/dl_cmds-lto.o: plugin needed to handle lto object ar: muz_qe/imdd-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_simple_joins-lto.o: plugin needed to handle lto object ar: muz_qe/vsubst_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/dl_interval_relation-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_unbound_compressor-lto.o: plugin needed to handle lto object ar: muz_qe/qe_dl_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_coalesce-lto.o: plugin needed to handle lto object ar: muz_qe/proof_utils-lto.o: plugin needed to handle lto object ar: muz_qe/qe_bv_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_util-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_explanations-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_rule_inliner-lto.o: plugin needed to handle lto object ar: muz_qe/dl_rule_transformer-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_magic_sets-lto.o: plugin needed to handle lto object ar: muz_qe/model2expr-lto.o: plugin needed to handle lto object ar: muz_qe/arith_bounds_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_partial_equiv-lto.o: plugin needed to handle lto object ar: muz_qe/qe-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_unfold-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_bit_blast-lto.o: plugin needed to handle lto object ar: muz_qe/dl_sieve_relation-lto.o: plugin needed to handle lto object ar: muz_qe/qe_bool_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/datalog_parser-lto.o: plugin needed to handle lto object ar: muz_qe/dl_rule_set-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_subsumption_checker-lto.o: plugin needed to handle lto object ar: muz_qe/dl_bound_relation-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_prop_solver-lto.o: plugin needed to handle lto object ar: muz_qe/nlarith_util-lto.o: plugin needed to handle lto object ar: muz_qe/replace_proof_converter-lto.o: plugin needed to handle lto object ar: muz_qe/dl_instruction-lto.o: plugin needed to handle lto object ar: muz_qe/dl_base-lto.o: plugin needed to handle lto object ar: muz_qe/dl_table-lto.o: plugin needed to handle lto object ar: muz_qe/dl_bmc_engine-lto.o: plugin needed to handle lto object ar: muz_qe/qe_datatype_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_filter_rules-lto.o: plugin needed to handle lto object ar: muz_qe/dl_table_relation-lto.o: plugin needed to handle lto object ar: muz_qe/dl_relation_manager-lto.o: plugin needed to handle lto object ar: muz_qe/qe_lite-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_slice-lto.o: plugin needed to handle lto object ar: muz_qe/horn_subsume_model_converter-lto.o: plugin needed to handle lto object ar: muz_qe/qe_arith_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_coi_filter-lto.o: plugin needed to handle lto object ar: muz_qe/dl_finite_product_relation-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_quantifiers-lto.o: plugin needed to handle lto object ar: muz_qe/dl_context-lto.o: plugin needed to handle lto object ar: muz_qe/dl_compiler-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_dl_interface-lto.o: plugin needed to handle lto object ar: muz_qe/dl_smt_relation-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_reachable_cache-lto.o: plugin needed to handle lto object ar: muz_qe/dl_rule_subsumption_index-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_context-lto.o: plugin needed to handle lto object ar: muz_qe/qe_cmd-lto.o: plugin needed to handle lto object ar: muz_qe/dl_external_relation-lto.o: plugin needed to handle lto object ar: muz_qe/dl_product_relation-lto.o: plugin needed to handle lto object ar: muz_qe/dl_check_table-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_sym_mux-lto.o: plugin needed to handle lto object ar: muz_qe/qe_array_plugin-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_similarity_compressor-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_smt_context_manager-lto.o: plugin needed to handle lto object ar: muz_qe/dl_mk_interp_tail_simplifier-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_util-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_generalizers-lto.o: plugin needed to handle lto object ar: muz_qe/unit_subsumption_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_farkas_learner-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_interpolant_provider-lto.o: plugin needed to handle lto object ar: muz_qe/qe_tactic-lto.o: plugin needed to handle lto object ar: muz_qe/pdr_manager-lto.o: plugin needed to handle lto object ar: muz_qe/dl_sparse_table-lto.o: plugin needed to handle lto object src/tactic/sls/sls_tactic.cpp --> tactic/sls/sls_tactic-lto.o tactic/sls/sls_tactic-lto.a ar: tactic/sls/sls_tactic-lto.o: plugin needed to handle lto object src/smt/tactic/smt_tactic.cpp --> smt/tactic/smt_tactic-lto.o src/smt/tactic/ctx_solver_simplify_tactic.cpp --> smt/tactic/ctxsolver simplify_tactic-lto.o smt/tactic/smt_tactic-lto.a ar: smt/tactic/smt_tactic-lto.o: plugin needed to handle lto object ar: smt/tactic/ctx_solver_simplify_tactic-lto.o: plugin needed to handle lto object src/tactic/fpa/fpa2bv_converter.cpp --> tactic/fpa/fpa2bv_converter-lto.o src/tactic/fpa/fpa2bv_tactic.cpp --> tactic/fpa/fpa2bv_tactic-lto.o src/tactic/fpa/qffpa_tactic.cpp --> tactic/fpa/qffpa_tactic-lto.o tactic/fpa/fpa-lto.a ar: tactic/fpa/fpa2bv_converter-lto.o: plugin needed to handle lto object ar: tactic/fpa/fpa2bv_tactic-lto.o: plugin needed to handle lto object ar: tactic/fpa/qffpa_tactic-lto.o: plugin needed to handle lto object src/tactic/bv/bv_size_reduction_tactic.cpp --> tactic/bv/bv_size_reduction_tactic-lto.o src/tactic/bv/bv1_blaster_tactic.cpp --> tactic/bv/bv1_blaster_tactic- lto.o src/tactic/bv/bit_blaster_model_converter.cpp --> tactic/bv/bit_blaster_model_converter-lto.o src/tactic/bv/max_bv_sharing_tactic.cpp --> tactic/bv/max_bvsharing tactic-lto.o src/tactic/bv/bit_blaster_tactic.cpp --> tactic/bv/bit_blaster_tactic- lto.o tactic/bv/bv_tactics-lto.a ar: tactic/bv/bv_size_reduction_tactic-lto.o: plugin needed to handle lto object ar: tactic/bv/bv1_blaster_tactic-lto.o: plugin needed to handle lto object ar: tactic/bv/bit_blaster_model_converter-lto.o: plugin needed to handle lto object ar: tactic/bv/max_bv_sharing_tactic-lto.o: plugin needed to handle lto object ar: tactic/bv/bit_blaster_tactic-lto.o: plugin needed to handle lto object src/smt/user_plugin/user_decl_plugin.cpp --> smt/user_plugin/userdecl plugin-lto.o src/smt/user_plugin/user_smt_theory.cpp --> smt/user_plugin/usersmt theory-lto.o src/smt/user_plugin/user_simplifier_plugin.cpp --> smt/userplugin/user simplifier_plugin-lto.o smt/user_plugin/user_plugin-lto.a ar: smt/user_plugin/user_decl_plugin-lto.o: plugin needed to handle lto object ar: smt/user_plugin/user_smt_theory-lto.o: plugin needed to handle lto object ar: smt/user_plugin/user_simplifier_plugin-lto.o: plugin needed to handle lto object src/smt/theory_diff_logic.cpp --> smt/theory_diff_logic-lto.o src/smt/smt_almost_cg_table.cpp --> smt/smt_almost_cg_table-lto.o src/smt/smt_quantifier_stat.cpp --> smt/smt_quantifier_stat-lto.o src/smt/smt_context_stat.cpp --> smt/smt_context_stat-lto.o src/smt/smt_setup.cpp --> smt/smt_setup-lto.o src/smt/smt_cg_table.cpp --> smt/smt_cg_table-lto.o src/smt/smt_conflict_resolution.cpp --> smt/smt_conflict_resolution-lto.o src/smt/smt_case_split_queue.cpp --> smt/smt_case_split_queue-lto.o src/smt/smt_solver.cpp --> smt/smt_solver-lto.o src/smt/mam.cpp --> smt/mam-lto.o src/smt/smt_context_inv.cpp --> smt/smt_context_inv-lto.o src/smt/expr_context_simplifier.cpp --> smt/expr_context_simplifier-lto.o src/smt/theory_datatype.cpp --> smt/theory_datatype-lto.o src/smt/smt_kernel.cpp --> smt/smt_kernel-lto.o src/smt/arith_eq_adapter.cpp --> smt/arith_eq_adapter-lto.o src/smt/smt_model_generator.cpp --> smt/smt_model_generator-lto.o src/smt/smt_statistics.cpp --> smt/smt_statistics-lto.o src/smt/cached_var_subst.cpp --> smt/cached_var_subst-lto.o src/smt/smt_literal.cpp --> smt/smt_literal-lto.o src/smt/smt_checker.cpp --> smt/smt_checker-lto.o src/smt/smt_implied_equalities.cpp --> smt/smt_implied_equalities-lto.o src/smt/smt_enode.cpp --> smt/smt_enode-lto.o src/smt/theory_instgen.cpp --> smt/theory_instgen-lto.o src/smt/smt_model_checker.cpp --> smt/smt_model_checker-lto.o src/smt/smt_quantifier.cpp --> smt/smt_quantifier-lto.o src/smt/theory_arith.cpp --> smt/theory_arith-lto.o src/smt/theory_dl.cpp --> smt/theory_dl-lto.o src/smt/theory_bv.cpp --> smt/theory_bv-lto.o src/smt/qi_queue.cpp --> smt/qi_queue-lto.o src/smt/theory_dummy.cpp --> smt/theory_dummy-lto.o src/smt/watch_list.cpp --> smt/watch_list-lto.o src/smt/smt_relevancy.cpp --> smt/smt_relevancy-lto.o src/smt/smt_internalizer.cpp --> smt/smt_internalizer-lto.o src/smt/cost_evaluator.cpp --> smt/cost_evaluator-lto.o src/smt/dyn_ack.cpp --> smt/dyn_ack-lto.o src/smt/smt_clause.cpp --> smt/smt_clause-lto.o src/smt/theory_array.cpp --> smt/theory_array-lto.o src/smt/smt_context_pp.cpp --> smt/smt_context_pp-lto.o src/smt/old_interval.cpp --> smt/old_interval-lto.o src/smt/theory_array_full.cpp --> smt/theory_array_full-lto.o src/smt/uses_theory.cpp --> smt/uses_theory-lto.o src/smt/smt_for_each_relevant_expr.cpp --> smt/smt_for_eachrelevant expr-lto.o src/smt/smt_justification.cpp --> smt/smt_justification-lto.o src/smt/smt_context.cpp --> smt/smt_context-lto.o src/smt/smt_model_finder.cpp --> smt/smt_model_finder-lto.o src/smt/arith_solver_plugin.cpp --> smt/arith_solver_plugin-lto.o src/smt/theory_array_base.cpp --> smt/theory_array_base-lto.o src/smt/smt_quick_checker.cpp --> smt/smt_quick_checker-lto.o src/smt/smt_theory.cpp --> smt/smt_theory-lto.o src/smt/fingerprints.cpp --> smt/fingerprints-lto.o src/smt/theory_dense_diff_logic.cpp --> smt/theory_dense_diff_logic-lto.o src/smt/asserted_formulas.cpp --> smt/asserted_formulas-lto.o src/smt/arith_eq_solver.cpp --> smt/arith_eq_solver-lto.o smt/smt-lto.a ar: smt/theory_diff_logic-lto.o: plugin needed to handle lto object ar: smt/smt_almost_cg_table-lto.o: plugin needed to handle lto object ar: smt/smt_quantifier_stat-lto.o: plugin needed to handle lto object ar: smt/smt_context_stat-lto.o: plugin needed to handle lto object ar: smt/smt_setup-lto.o: plugin needed to handle lto object ar: smt/smt_cg_table-lto.o: plugin needed to handle lto object ar: smt/smt_conflict_resolution-lto.o: plugin needed to handle lto object ar: smt/smt_case_split_queue-lto.o: plugin needed to handle lto object ar: smt/smt_solver-lto.o: plugin needed to handle lto object ar: smt/mam-lto.o: plugin needed to handle lto object ar: smt/smt_context_inv-lto.o: plugin needed to handle lto object ar: smt/expr_context_simplifier-lto.o: plugin needed to handle lto object ar: smt/theory_datatype-lto.o: plugin needed to handle lto object ar: smt/smt_kernel-lto.o: plugin needed to handle lto object ar: smt/arith_eq_adapter-lto.o: plugin needed to handle lto object ar: smt/smt_model_generator-lto.o: plugin needed to handle lto object ar: smt/smt_statistics-lto.o: plugin needed to handle lto object ar: smt/cached_var_subst-lto.o: plugin needed to handle lto object ar: smt/smt_literal-lto.o: plugin needed to handle lto object ar: smt/smt_checker-lto.o: plugin needed to handle lto object ar: smt/smt_implied_equalities-lto.o: plugin needed to handle lto object ar: smt/smt_enode-lto.o: plugin needed to handle lto object ar: smt/theory_instgen-lto.o: plugin needed to handle lto object ar: smt/smt_model_checker-lto.o: plugin needed to handle lto object ar: smt/smt_quantifier-lto.o: plugin needed to handle lto object ar: smt/theory_arith-lto.o: plugin needed to handle lto object ar: smt/theory_dl-lto.o: plugin needed to handle lto object ar: smt/theory_bv-lto.o: plugin needed to handle lto object ar: smt/qi_queue-lto.o: plugin needed to handle lto object ar: smt/theory_dummy-lto.o: plugin needed to handle lto object ar: smt/watch_list-lto.o: plugin needed to handle lto object ar: smt/smt_relevancy-lto.o: plugin needed to handle lto object ar: smt/smt_internalizer-lto.o: plugin needed to handle lto object ar: smt/cost_evaluator-lto.o: plugin needed to handle lto object ar: smt/dyn_ack-lto.o: plugin needed to handle lto object ar: smt/smt_clause-lto.o: plugin needed to handle lto object ar: smt/theory_array-lto.o: plugin needed to handle lto object ar: smt/smt_context_pp-lto.o: plugin needed to handle lto object ar: smt/old_interval-lto.o: plugin needed to handle lto object ar: smt/theory_array_full-lto.o: plugin needed to handle lto object ar: smt/uses_theory-lto.o: plugin needed to handle lto object ar: smt/smt_for_each_relevant_expr-lto.o: plugin needed to handle lto object ar: smt/smt_justification-lto.o: plugin needed to handle lto object ar: smt/smt_context-lto.o: plugin needed to handle lto object ar: smt/smt_model_finder-lto.o: plugin needed to handle lto object ar: smt/arith_solver_plugin-lto.o: plugin needed to handle lto object ar: smt/theory_array_base-lto.o: plugin needed to handle lto object ar: smt/smt_quick_checker-lto.o: plugin needed to handle lto object ar: smt/smt_theory-lto.o: plugin needed to handle lto object ar: smt/fingerprints-lto.o: plugin needed to handle lto object ar: smt/theory_dense_diff_logic-lto.o: plugin needed to handle lto object ar: smt/asserted_formulas-lto.o: plugin needed to handle lto object ar: smt/arith_eq_solver-lto.o: plugin needed to handle lto object src/smt/proto_model/array_factory.cpp --> smt/proto_model/array_factory- lto.o src/smt/proto_model/proto_model.cpp --> smt/proto_model/proto_model-lto.o src/smt/proto_model/value_factory.cpp --> smt/proto_model/value_factory- lto.o src/smt/proto_model/numeral_factory.cpp --> smt/protomodel/numeral factory-lto.o src/smt/proto_model/struct_factory.cpp --> smt/protomodel/struct factory-lto.o src/smt/proto_model/datatype_factory.cpp --> smt/protomodel/datatype factory-lto.o smt/proto_model/proto_model-lto.a ar: smt/proto_model/array_factory-lto.o: plugin needed to handle lto object ar: smt/proto_model/proto_model-lto.o: plugin needed to handle lto object ar: smt/proto_model/value_factory-lto.o: plugin needed to handle lto object ar: smt/proto_model/numeral_factory-lto.o: plugin needed to handle lto object ar: smt/proto_model/struct_factory-lto.o: plugin needed to handle lto object ar: smt/proto_model/datatype_factory-lto.o: plugin needed to handle lto object src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp --> ast/rewriter/bit_blaster/bit_blaster_rewriter-lto.o src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp --> ast/rewriter/bit_blaster/eager_bit_blaster-lto.o src/ast/rewriter/bit_blaster/bit_blaster.cpp --> ast/rewriter/bit_blaster/bit_blaster-lto.o ast/rewriter/bit_blaster/bit_blaster-lto.a ar: ast/rewriter/bit_blaster/bit_blaster_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/bit_blaster/eager_bit_blaster-lto.o: plugin needed to handle lto object ar: ast/rewriter/bit_blaster/bit_blaster-lto.o: plugin needed to handle lto object src/ast/proof_checker/proof_checker.cpp --> ast/proofchecker/proof checker-lto.o ast/proof_checker/proof_checker-lto.a ar: ast/proof_checker/proof_checker-lto.o: plugin needed to handle lto object src/ast/macros/quasi_macros.cpp --> ast/macros/quasi_macros-lto.o src/ast/macros/macro_manager.cpp --> ast/macros/macro_manager-lto.o src/ast/macros/macro_finder.cpp --> ast/macros/macro_finder-lto.o src/ast/macros/macro_util.cpp --> ast/macros/macro_util-lto.o ast/macros/macros-lto.a ar: ast/macros/quasi_macros-lto.o: plugin needed to handle lto object ar: ast/macros/macro_manager-lto.o: plugin needed to handle lto object ar: ast/macros/macro_finder-lto.o: plugin needed to handle lto object ar: ast/macros/macro_util-lto.o: plugin needed to handle lto object src/ast/pattern/expr_pattern_match.cpp --> ast/pattern/exprpattern match-lto.o src/ast/pattern/pattern_inference.cpp --> ast/pattern/pattern_inference- lto.o ast/pattern/pattern-lto.a ar: ast/pattern/expr_pattern_match-lto.o: plugin needed to handle lto object ar: ast/pattern/pattern_inference-lto.o: plugin needed to handle lto object src/parsers/smt2/smt2scanner.cpp --> parsers/smt2/smt2scanner-lto.o src/parsers/smt2/smt2parser.cpp --> parsers/smt2/smt2parser-lto.o parsers/smt2/smt2parser-lto.a ar: parsers/smt2/smt2scanner-lto.o: plugin needed to handle lto object ar: parsers/smt2/smt2parser-lto.o: plugin needed to handle lto object src/cmd_context/extra_cmds/dbg_cmds.cpp --> cmd_context/extracmds/dbg cmds-lto.o src/cmd_context/extra_cmds/polynomial_cmds.cpp --> cmd_context/extra_cmds/ polynomial_cmds-lto.o src/cmd_context/extra_cmds/subpaving_cmds.cpp --> cmd_context/extra_cmds/ subpaving_cmds-lto.o cmd_context/extra_cmds/extra_cmds-lto.a ar: cmd_context/extra_cmds/dbg_cmds-lto.o: plugin needed to handle lto object ar: cmd_context/extra_cmds/polynomial_cmds-lto.o: plugin needed to handle lto object ar: cmd_context/extra_cmds/subpaving_cmds-lto.o: plugin needed to handle lto object src/cmd_context/simplify_cmd.cpp --> cmd_context/simplify_cmd-lto.o src/cmd_context/tactic_cmds.cpp --> cmd_context/tactic_cmds-lto.o src/cmd_context/cmd_context.cpp --> cmd_context/cmd_context-lto.o src/cmd_context/pdecl.cpp --> cmd_context/pdecl-lto.o src/cmd_context/echo_tactic.cpp --> cmd_context/echo_tactic-lto.o src/cmd_context/cmd_util.cpp --> cmd_context/cmd_util-lto.o src/cmd_context/tactic_manager.cpp --> cmd_context/tactic_manager-lto.o src/cmd_context/basic_cmds.cpp --> cmd_context/basic_cmds-lto.o src/cmd_context/cmd_context_to_goal.cpp --> cmd_context/cmd_contextto goal-lto.o src/cmd_context/eval_cmd.cpp --> cmd_context/eval_cmd-lto.o src/cmd_context/parametric_cmd.cpp --> cmd_context/parametric_cmd-lto.o src/cmd_context/check_logic.cpp --> cmd_context/check_logic-lto.o cmd_context/cmd_context-lto.a ar: cmd_context/simplify_cmd-lto.o: plugin needed to handle lto object ar: cmd_context/tactic_cmds-lto.o: plugin needed to handle lto object ar: cmd_context/cmd_context-lto.o: plugin needed to handle lto object ar: cmd_context/pdecl-lto.o: plugin needed to handle lto object ar: cmd_context/echo_tactic-lto.o: plugin needed to handle lto object ar: cmd_context/cmd_util-lto.o: plugin needed to handle lto object ar: cmd_context/tactic_manager-lto.o: plugin needed to handle lto object ar: cmd_context/basic_cmds-lto.o: plugin needed to handle lto object ar: cmd_context/cmd_context_to_goal-lto.o: plugin needed to handle lto object ar: cmd_context/eval_cmd-lto.o: plugin needed to handle lto object ar: cmd_context/parametric_cmd-lto.o: plugin needed to handle lto object ar: cmd_context/check_logic-lto.o: plugin needed to handle lto object src/solver/solver.cpp --> solver/solver-lto.o src/solver/strategic_solver.cpp --> solver/strategic_solver-lto.o src/solver/solver_na2as.cpp --> solver/solver_na2as-lto.o src/solver/tactic2solver.cpp --> solver/tactic2solver-lto.o src/solver/check_sat_result.cpp --> solver/check_sat_result-lto.o solver/solver-lto.a ar: solver/solver-lto.o: plugin needed to handle lto object ar: solver/strategic_solver-lto.o: plugin needed to handle lto object ar: solver/solver_na2as-lto.o: plugin needed to handle lto object ar: solver/tactic2solver-lto.o: plugin needed to handle lto object ar: solver/check_sat_result-lto.o: plugin needed to handle lto object src/tactic/aig/aig_tactic.cpp --> tactic/aig/aig_tactic-lto.o src/tactic/aig/aig.cpp --> tactic/aig/aig-lto.o tactic/aig/aig_tactic-lto.a ar: tactic/aig/aig_tactic-lto.o: plugin needed to handle lto object ar: tactic/aig/aig-lto.o: plugin needed to handle lto object src/math/subpaving/tactic/subpaving_tactic.cpp --> math/subpaving/tactic/ subpaving_tactic-lto.o src/math/subpaving/tactic/expr2subpaving.cpp --> math/subpaving/tactic/ expr2subpaving-lto.o math/subpaving/tactic/subpaving_tactic-lto.a ar: math/subpaving/tactic/subpaving_tactic-lto.o: plugin needed to handle lto object ar: math/subpaving/tactic/expr2subpaving-lto.o: plugin needed to handle lto object src/nlsat/tactic/goal2nlsat.cpp --> nlsat/tactic/goal2nlsat-lto.o src/nlsat/tactic/qfnra_nlsat_tactic.cpp --> nlsat/tactic/qfnranlsat tactic-lto.o src/nlsat/tactic/nlsat_tactic.cpp --> nlsat/tactic/nlsat_tactic-lto.o nlsat/tactic/nlsat_tactic-lto.a ar: nlsat/tactic/goal2nlsat-lto.o: plugin needed to handle lto object ar: nlsat/tactic/qfnra_nlsat_tactic-lto.o: plugin needed to handle lto object ar: nlsat/tactic/nlsat_tactic-lto.o: plugin needed to handle lto object src/tactic/arith/probe_arith.cpp --> tactic/arith/probe_arith-lto.o src/tactic/arith/nla2bv_tactic.cpp --> tactic/arith/nla2bv_tactic-lto.o src/tactic/arith/pb2bv_model_converter.cpp --> tactic/arith/pb2bvmodel converter-lto.o src/tactic/arith/bv2real_rewriter.cpp --> tactic/arith/bv2real_rewriter- lto.o src/tactic/arith/pb2bv_tactic.cpp --> tactic/arith/pb2bv_tactic-lto.o src/tactic/arith/fm_tactic.cpp --> tactic/arith/fm_tactic-lto.o src/tactic/arith/bv2int_rewriter.cpp --> tactic/arith/bv2int_rewriter- lto.o src/tactic/arith/recover_01_tactic.cpp --> tactic/arith/recover01 tactic-lto.o src/tactic/arith/lia2pb_tactic.cpp --> tactic/arith/lia2pb_tactic-lto.o src/tactic/arith/normalize_bounds_tactic.cpp --> tactic/arith/normalize_bounds_tactic-lto.o src/tactic/arith/diff_neq_tactic.cpp --> tactic/arith/diff_neq_tactic- lto.o src/tactic/arith/bound_manager.cpp --> tactic/arith/bound_manager-lto.o src/tactic/arith/propagate_ineqs_tactic.cpp --> tactic/arith/propagate_ineqs_tactic-lto.o src/tactic/arith/add_bounds_tactic.cpp --> tactic/arith/addbounds tactic-lto.o src/tactic/arith/degree_shift_tactic.cpp --> tactic/arith/degreeshift tactic-lto.o src/tactic/arith/factor_tactic.cpp --> tactic/arith/factor_tactic-lto.o src/tactic/arith/fix_dl_var_tactic.cpp --> tactic/arith/fix_dlvar tactic-lto.o src/tactic/arith/bound_propagator.cpp --> tactic/arith/bound_propagator- lto.o src/tactic/arith/purify_arith_tactic.cpp --> tactic/arith/purifyarith tactic-lto.o src/tactic/arith/linear_equation.cpp --> tactic/arith/linear_equation- lto.o tactic/arith/arith_tactics-lto.a ar: tactic/arith/probe_arith-lto.o: plugin needed to handle lto object ar: tactic/arith/nla2bv_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/pb2bv_model_converter-lto.o: plugin needed to handle lto object ar: tactic/arith/bv2real_rewriter-lto.o: plugin needed to handle lto object ar: tactic/arith/pb2bv_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/fm_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/bv2int_rewriter-lto.o: plugin needed to handle lto object ar: tactic/arith/recover_01_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/lia2pb_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/normalize_bounds_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/diff_neq_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/bound_manager-lto.o: plugin needed to handle lto object ar: tactic/arith/propagate_ineqs_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/add_bounds_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/degree_shift_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/factor_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/fix_dl_var_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/bound_propagator-lto.o: plugin needed to handle lto object ar: tactic/arith/purify_arith_tactic-lto.o: plugin needed to handle lto object ar: tactic/arith/linear_equation-lto.o: plugin needed to handle lto object src/sat/tactic/atom2bool_var.cpp --> sat/tactic/atom2bool_var-lto.o src/sat/tactic/sat_tactic.cpp --> sat/tactic/sat_tactic-lto.o src/sat/tactic/goal2sat.cpp --> sat/tactic/goal2sat-lto.o sat/tactic/sat_tactic-lto.a ar: sat/tactic/atom2bool_var-lto.o: plugin needed to handle lto object ar: sat/tactic/sat_tactic-lto.o: plugin needed to handle lto object ar: sat/tactic/goal2sat-lto.o: plugin needed to handle lto object src/tactic/core/ctx_simplify_tactic.cpp --> tactic/core/ctxsimplify tactic-lto.o src/tactic/core/elim_term_ite_tactic.cpp --> tactic/core/elim_termite tactic-lto.o src/tactic/core/propagate_values_tactic.cpp --> tactic/core/propagate_values_tactic-lto.o src/tactic/core/distribute_forall_tactic.cpp --> tactic/core/distribute_forall_tactic-lto.o src/tactic/core/der_tactic.cpp --> tactic/core/der_tactic-lto.o src/tactic/core/simplify_tactic.cpp --> tactic/core/simplify_tactic-lto.o src/tactic/core/occf_tactic.cpp --> tactic/core/occf_tactic-lto.o src/tactic/core/cofactor_term_ite_tactic.cpp --> tactic/core/cofactor_term_ite_tactic-lto.o src/tactic/core/cofactor_elim_term_ite.cpp --> tactic/core/cofactorelim term_ite-lto.o src/tactic/core/tseitin_cnf_tactic.cpp --> tactic/core/tseitincnf tactic-lto.o src/tactic/core/split_clause_tactic.cpp --> tactic/core/splitclause tactic-lto.o src/tactic/core/reduce_args_tactic.cpp --> tactic/core/reduceargs tactic-lto.o src/tactic/core/symmetry_reduce_tactic.cpp --> tactic/core/symmetry_reduce_tactic-lto.o src/tactic/core/elim_uncnstr_tactic.cpp --> tactic/core/elimuncnstr tactic-lto.o src/tactic/core/nnf_tactic.cpp --> tactic/core/nnf_tactic-lto.o src/tactic/core/solve_eqs_tactic.cpp --> tactic/core/solve_eqs_tactic- lto.o tactic/core/core_tactics-lto.a ar: tactic/core/ctx_simplify_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/elim_term_ite_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/propagate_values_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/distribute_forall_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/der_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/simplify_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/occf_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/cofactor_term_ite_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/cofactor_elim_term_ite-lto.o: plugin needed to handle lto object ar: tactic/core/tseitin_cnf_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/split_clause_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/reduce_args_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/symmetry_reduce_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/elim_uncnstr_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/nnf_tactic-lto.o: plugin needed to handle lto object ar: tactic/core/solve_eqs_tactic-lto.o: plugin needed to handle lto object src/ast/normal_forms/name_exprs.cpp --> ast/normal_forms/name_exprs-lto.o src/ast/normal_forms/nnf.cpp --> ast/normal_forms/nnf-lto.o src/ast/normal_forms/pull_quant.cpp --> ast/normal_forms/pull_quant-lto.o src/ast/normal_forms/defined_names.cpp --> ast/normalforms/defined names-lto.o src/ast/normal_forms/elim_term_ite.cpp --> ast/normal_forms/elimterm ite-lto.o src/ast/normal_forms/cnf.cpp --> ast/normal_forms/cnf-lto.o ast/normal_forms/normal_forms-lto.a ar: ast/normal_forms/name_exprs-lto.o: plugin needed to handle lto object ar: ast/normal_forms/nnf-lto.o: plugin needed to handle lto object ar: ast/normal_forms/pull_quant-lto.o: plugin needed to handle lto object ar: ast/normal_forms/defined_names-lto.o: plugin needed to handle lto object ar: ast/normal_forms/elim_term_ite-lto.o: plugin needed to handle lto object ar: ast/normal_forms/cnf-lto.o: plugin needed to handle lto object src/ast/simplifier/simplifier.cpp --> ast/simplifier/simplifier-lto.o src/ast/simplifier/bit2int.cpp --> ast/simplifier/bit2int-lto.o src/ast/simplifier/elim_bounds.cpp --> ast/simplifier/elim_bounds-lto.o src/ast/simplifier/distributeforall.cpp --> ast/simplifier/distribute forall-lto.o src/ast/simplifier/simplifierplugin.cpp --> ast/simplifier/simplifier plugin-lto.o src/ast/simplifier/arith_simplifierplugin.cpp --> ast/simplifier/arith simplifier_plugin-lto.o src/ast/simplifier/maximise_ac_sharing.cpp --> ast/simplifier/maximiseac sharing-lto.o src/ast/simplifier/array_simplifierplugin.cpp --> ast/simplifier/array simplifier_plugin-lto.o src/ast/simplifier/poly_simplifierplugin.cpp --> ast/simplifier/poly simplifier_plugin-lto.o src/ast/simplifier/bv_simplifier_plugin.cpp --> ast/simplifier/bv_simplifier_plugin-lto.o src/ast/simplifier/datatype_simplifier_plugin.cpp --> ast/simplifier/datatype_simplifier_plugin-lto.o src/ast/simplifier/inj_axiom.cpp --> ast/simplifier/inj_axiom-lto.o src/ast/simplifier/push_app_ite.cpp --> ast/simplifier/push_app_ite-lto.o src/ast/simplifier/bv_elim.cpp --> ast/simplifier/bv_elim-lto.o src/ast/simplifier/basic_simplifierplugin.cpp --> ast/simplifier/basic simplifier_plugin-lto.o src/ast/simplifier/pull_ite_tree.cpp --> ast/simplifier/pull_ite_tree- lto.o ast/simplifier/simplifier-lto.a ar: ast/simplifier/simplifier-lto.o: plugin needed to handle lto object ar: ast/simplifier/bit2int-lto.o: plugin needed to handle lto object ar: ast/simplifier/elim_bounds-lto.o: plugin needed to handle lto object ar: ast/simplifier/distribute_forall-lto.o: plugin needed to handle lto object ar: ast/simplifier/simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/arith_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/maximise_ac_sharing-lto.o: plugin needed to handle lto object ar: ast/simplifier/array_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/poly_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/bv_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/datatype_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/inj_axiom-lto.o: plugin needed to handle lto object ar: ast/simplifier/push_app_ite-lto.o: plugin needed to handle lto object ar: ast/simplifier/bv_elim-lto.o: plugin needed to handle lto object ar: ast/simplifier/basic_simplifier_plugin-lto.o: plugin needed to handle lto object ar: ast/simplifier/pull_ite_tree-lto.o: plugin needed to handle lto object src/front_end_params/params2front_end_params.cpp --> front_end_params/params2front_end_params-lto.o src/front_end_params/model_params.cpp --> front_end_params/model_params- lto.o src/front_end_params/dyn_ack_params.cpp --> front_end_params/dynack params-lto.o src/front_end_params/nnf_params.cpp --> front_end_params/nnf_params-lto.o src/front_end_params/order_params.cpp --> front_end_params/order_params- lto.o src/front_end_params/cnf_params.cpp --> front_end_params/cnf_params-lto.o src/front_end_params/spc_params.cpp --> front_end_params/spc_params-lto.o src/front_end_params/parser_params.cpp --> front_endparams/parser params-lto.o src/front_end_params/arith_simplifier_params.cpp --> front_end_params/arith_simplifier_params-lto.o src/front_end_params/pattern_inference_params.cpp --> front_end_params/pattern_inference_params-lto.o src/front_end_params/theory_arith_params.cpp --> front_end_params/theory_arith_params-lto.o src/front_end_params/z3_solver_params.cpp --> front_end_params/z3solver params-lto.o src/front_end_params/front_end_params.cpp --> front_end_params/frontend params-lto.o src/front_end_params/smt_params.cpp --> front_end_params/smt_params-lto.o front_end_params/front_end_params-lto.a ar: front_end_params/params2front_end_params-lto.o: plugin needed to handle lto object ar: front_end_params/model_params-lto.o: plugin needed to handle lto object ar: front_end_params/dyn_ack_params-lto.o: plugin needed to handle lto object ar: front_end_params/nnf_params-lto.o: plugin needed to handle lto object ar: front_end_params/order_params-lto.o: plugin needed to handle lto object ar: front_end_params/cnf_params-lto.o: plugin needed to handle lto object ar: front_end_params/spc_params-lto.o: plugin needed to handle lto object ar: front_end_params/parser_params-lto.o: plugin needed to handle lto object ar: front_end_params/arith_simplifier_params-lto.o: plugin needed to handle lto object ar: front_end_params/pattern_inference_params-lto.o: plugin needed to handle lto object ar: front_end_params/theory_arith_params-lto.o: plugin needed to handle lto object ar: front_end_params/z3_solver_params-lto.o: plugin needed to handle lto object ar: front_end_params/front_end_params-lto.o: plugin needed to handle lto object ar: front_end_params/smt_params-lto.o: plugin needed to handle lto object src/math/euclid/euclidean_solver.cpp --> math/euclid/euclidean_solver- lto.o math/euclid/euclid-lto.a ar: math/euclid/euclidean_solver-lto.o: plugin needed to handle lto object src/math/grobner/grobner.cpp --> math/grobner/grobner-lto.o math/grobner/grobner-lto.a ar: math/grobner/grobner-lto.o: plugin needed to handle lto object src/parsers/util/patternvalidation.cpp --> parsers/util/pattern validation-lto.o src/parsers/util/scanner.cpp --> parsers/util/scanner-lto.o src/parsers/util/cost_parser.cpp --> parsers/util/cost_parser-lto.o src/parsers/util/simple_parser.cpp --> parsers/util/simple_parser-lto.o parsers/util/parser_util-lto.a ar: parsers/util/pattern_validation-lto.o: plugin needed to handle lto object ar: parsers/util/scanner-lto.o: plugin needed to handle lto object ar: parsers/util/cost_parser-lto.o: plugin needed to handle lto object ar: parsers/util/simple_parser-lto.o: plugin needed to handle lto object src/ast/substitution/matcher.cpp --> ast/substitution/matcher-lto.o src/ast/substitution/substitution.cpp --> ast/substitution/substitution- lto.o src/ast/substitution/substitution_tree.cpp --> ast/substitution/substitution_tree-lto.o src/ast/substitution/unifier.cpp --> ast/substitution/unifier-lto.o ast/substitution/substitution-lto.a ar: ast/substitution/matcher-lto.o: plugin needed to handle lto object ar: ast/substitution/substitution-lto.o: plugin needed to handle lto object ar: ast/substitution/substitution_tree-lto.o: plugin needed to handle lto object ar: ast/substitution/unifier-lto.o: plugin needed to handle lto object src/tactic/goal_util.cpp --> tactic/goal_util-lto.o src/tactic/model_converter.cpp --> tactic/model_converter-lto.o src/tactic/num_occurs_goal.cpp --> tactic/num_occurs_goal-lto.o src/tactic/tactic.cpp --> tactic/tactic-lto.o src/tactic/filter_model_converter.cpp --> tactic/filter_model_converter- lto.o src/tactic/extension_model_converter.cpp --> tactic/extensionmodel converter-lto.o src/tactic/goal.cpp --> tactic/goal-lto.o src/tactic/probe.cpp --> tactic/probe-lto.o src/tactic/tactical.cpp --> tactic/tactical-lto.o src/tactic/proof_converter.cpp --> tactic/proof_converter-lto.o src/tactic/goal_shared_occs.cpp --> tactic/goal_shared_occs-lto.o tactic/tactic-lto.a ar: tactic/goal_util-lto.o: plugin needed to handle lto object ar: tactic/model_converter-lto.o: plugin needed to handle lto object ar: tactic/num_occurs_goal-lto.o: plugin needed to handle lto object ar: tactic/tactic-lto.o: plugin needed to handle lto object ar: tactic/filter_model_converter-lto.o: plugin needed to handle lto object ar: tactic/extension_model_converter-lto.o: plugin needed to handle lto object ar: tactic/goal-lto.o: plugin needed to handle lto object ar: tactic/probe-lto.o: plugin needed to handle lto object ar: tactic/tactical-lto.o: plugin needed to handle lto object ar: tactic/proof_converter-lto.o: plugin needed to handle lto object ar: tactic/goal_shared_occs-lto.o: plugin needed to handle lto object src/model/model_smt2_pp.cpp --> model/model_smt2_pp-lto.o src/model/func_interp.cpp --> model/func_interp-lto.o src/model/model.cpp --> model/model-lto.o src/model/model_core.cpp --> model/model_core-lto.o src/model/model_v2_pp.cpp --> model/model_v2_pp-lto.o src/model/model_evaluator.cpp --> model/model_evaluator-lto.o src/model/model_pp.cpp --> model/model_pp-lto.o model/model-lto.a ar: model/model_smt2_pp-lto.o: plugin needed to handle lto object ar: model/func_interp-lto.o: plugin needed to handle lto object ar: model/model-lto.o: plugin needed to handle lto object ar: model/model_core-lto.o: plugin needed to handle lto object ar: model/model_v2_pp-lto.o: plugin needed to handle lto object ar: model/model_evaluator-lto.o: plugin needed to handle lto object ar: model/model_pp-lto.o: plugin needed to handle lto object src/ast/rewriter/arith_rewriter.cpp --> ast/rewriter/arith_rewriter-lto.o src/ast/rewriter/th_rewriter.cpp --> ast/rewriter/th_rewriter-lto.o src/ast/rewriter/expr_replacer.cpp --> ast/rewriter/expr_replacer-lto.o src/ast/rewriter/mk_simplified_app.cpp --> ast/rewriter/mksimplified app-lto.o src/ast/rewriter/der.cpp --> ast/rewriter/der-lto.o src/ast/rewriter/dl_rewriter.cpp --> ast/rewriter/dl_rewriter-lto.o src/ast/rewriter/float_rewriter.cpp --> ast/rewriter/float_rewriter-lto.o src/ast/rewriter/factor_rewriter.cpp --> ast/rewriter/factor_rewriter- lto.o src/ast/rewriter/array_rewriter.cpp --> ast/rewriter/array_rewriter-lto.o src/ast/rewriter/quant_hoist.cpp --> ast/rewriter/quant_hoist-lto.o src/ast/rewriter/datatyperewriter.cpp --> ast/rewriter/datatype rewriter-lto.o src/ast/rewriter/var_subst.cpp --> ast/rewriter/var_subst-lto.o src/ast/rewriter/rewriter.cpp --> ast/rewriter/rewriter-lto.o src/ast/rewriter/bv_rewriter.cpp --> ast/rewriter/bv_rewriter-lto.o src/ast/rewriter/bool_rewriter.cpp --> ast/rewriter/bool_rewriter-lto.o ast/rewriter/rewriter-lto.a ar: ast/rewriter/arith_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/th_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/expr_replacer-lto.o: plugin needed to handle lto object ar: ast/rewriter/mk_simplified_app-lto.o: plugin needed to handle lto object ar: ast/rewriter/der-lto.o: plugin needed to handle lto object ar: ast/rewriter/dl_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/float_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/factor_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/array_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/quant_hoist-lto.o: plugin needed to handle lto object ar: ast/rewriter/datatype_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/var_subst-lto.o: plugin needed to handle lto object ar: ast/rewriter/rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/bv_rewriter-lto.o: plugin needed to handle lto object ar: ast/rewriter/bool_rewriter-lto.o: plugin needed to handle lto object src/ast/has_free_vars.cpp --> ast/has_free_vars-lto.o src/ast/ast_printer.cpp --> ast/ast_printer-lto.o src/ast/ast_util.cpp --> ast/ast_util-lto.o src/ast/pp.cpp --> ast/pp-lto.o src/ast/act_cache.cpp --> ast/act_cache-lto.o src/ast/ast_smt2_pp.cpp --> ast/ast_smt2_pp-lto.o src/ast/num_occurs.cpp --> ast/num_occurs-lto.o src/ast/bv_decl_plugin.cpp --> ast/bv_decl_plugin-lto.o src/ast/expr_functors.cpp --> ast/expr_functors-lto.o src/ast/ast.cpp --> ast/ast-lto.o src/ast/expr_abstract.cpp --> ast/expr_abstract-lto.o src/ast/for_each_ast.cpp --> ast/for_each_ast-lto.o src/ast/ast_translation.cpp --> ast/ast_translation-lto.o src/ast/expr2polynomial.cpp --> ast/expr2polynomial-lto.o src/ast/datatype_decl_plugin.cpp --> ast/datatype_decl_plugin-lto.o src/ast/format.cpp --> ast/format-lto.o src/ast/expr2var.cpp --> ast/expr2var-lto.o src/ast/arith_decl_plugin.cpp --> ast/arith_decl_plugin-lto.o src/ast/expr_map.cpp --> ast/expr_map-lto.o src/ast/for_each_expr.cpp --> ast/for_each_expr-lto.o src/ast/ast_pp.cpp --> ast/ast_pp-lto.o src/ast/shared_occs.cpp --> ast/shared_occs-lto.o src/ast/reg_decl_plugins.cpp --> ast/reg_decl_plugins-lto.o src/ast/well_sorted.cpp --> ast/well_sorted-lto.o src/ast/ast_smt_pp.cpp --> ast/ast_smt_pp-lto.o src/ast/static_features.cpp --> ast/static_features-lto.o src/ast/expr_substitution.cpp --> ast/expr_substitution-lto.o src/ast/pp_params.cpp --> ast/pp_params-lto.o src/ast/array_decl_plugin.cpp --> ast/array_decl_plugin-lto.o src/ast/func_decl_dependencies.cpp --> ast/func_decl_dependencies-lto.o src/ast/decl_collector.cpp --> ast/decl_collector-lto.o src/ast/expr_stat.cpp --> ast/expr_stat-lto.o src/ast/used_vars.cpp --> ast/used_vars-lto.o src/ast/dl_decl_plugin.cpp --> ast/dl_decl_plugin-lto.o src/ast/macro_substitution.cpp --> ast/macro_substitution-lto.o src/ast/float_decl_plugin.cpp --> ast/float_decl_plugin-lto.o src/ast/occurs.cpp --> ast/occurs-lto.o src/ast/ast_ll_pp.cpp --> ast/ast_ll_pp-lto.o src/ast/seq_decl_plugin.cpp --> ast/seq_decl_plugin-lto.o src/ast/ast_lt.cpp --> ast/ast_lt-lto.o ast/ast-lto.a ar: ast/has_free_vars-lto.o: plugin needed to handle lto object ar: ast/ast_printer-lto.o: plugin needed to handle lto object ar: ast/ast_util-lto.o: plugin needed to handle lto object ar: ast/pp-lto.o: plugin needed to handle lto object ar: ast/act_cache-lto.o: plugin needed to handle lto object ar: ast/ast_smt2_pp-lto.o: plugin needed to handle lto object ar: ast/num_occurs-lto.o: plugin needed to handle lto object ar: ast/bv_decl_plugin-lto.o: plugin needed to handle lto object ar: ast/expr_functors-lto.o: plugin needed to handle lto object ar: ast/ast-lto.o: plugin needed to handle lto object ar: ast/expr_abstract-lto.o: plugin needed to handle lto object ar: ast/for_each_ast-lto.o: plugin needed to handle lto object ar: ast/ast_translation-lto.o: plugin needed to hand

rishabhs / sygus-comp14

Compiling Enumerative solver returns errors #9