Your message dated Sat, 29 Oct 2022 20:36:34 +0000 with message-id <e1ooszg-00gkqn...@fasolo.debian.org> and subject line Bug#1020010: fixed in cvc4 1.8-3 has caused the Debian Bug report #1020010, regarding cvc4 FTBFS with bash 5.2 to be marked as done.
This means that you claim that the problem has been dealt with. If this is not the case it is now your responsibility to reopen the Bug report if necessary, and/or fix the problem forthwith. (NB: If you are a system administrator and have no idea what this message is talking about, this may indicate a serious mail system misconfiguration somewhere. Please contact ow...@bugs.debian.org immediately.) -- 1020010: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1020010 Debian Bug Tracking System Contact ow...@bugs.debian.org with problems
--- Begin Message ---Source: cvc4 Version: 1.8-2 Severity: serious Justification: FTBFS Tags: bookworm sid ftbfs User: lu...@debian.org Usertags: ftbfs-20220917 ftbfs-bookworm Hi, During a rebuild of all packages in sid, your package failed to build on amd64. Relevant part (hopefully): > make[3]: Entering directory '/<<PKGBUILDDIR>>/obj-x86_64-linux-gnu' > make[3]: Leaving directory '/<<PKGBUILDDIR>>/obj-x86_64-linux-gnu' > [ 1%] Generating metakind.h > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr && /usr/bin/cmake -E env > CMAKE_SOURCE_DIR=/<<PKGBUILDDIR>> /<<PKGBUILDDIR>>/src/expr/mkmetakind > /<<PKGBUILDDIR>>/src/expr/metakind_template.h > /<<PKGBUILDDIR>>/src/theory/builtin/kinds > /<<PKGBUILDDIR>>/src/theory/booleans/kinds > /<<PKGBUILDDIR>>/src/theory/uf/kinds /<<PKGBUILDDIR>>/src/theory/arith/kinds > /<<PKGBUILDDIR>>/src/theory/bv/kinds /<<PKGBUILDDIR>>/src/theory/fp/kinds > /<<PKGBUILDDIR>>/src/theory/arrays/kinds > /<<PKGBUILDDIR>>/src/theory/datatypes/kinds > /<<PKGBUILDDIR>>/src/theory/sep/kinds /<<PKGBUILDDIR>>/src/theory/sets/kinds > /<<PKGBUILDDIR>>/src/theory/strings/kinds > /<<PKGBUILDDIR>>/src/theory/quantifiers/kinds > > /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr/metakind.h > [ 1%] Built target gen-tokens > [ 1%] Generating theory_traits.h > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/theory && > /<<PKGBUILDDIR>>/src/theory/mktheorytraits > /<<PKGBUILDDIR>>/src/theory/theory_traits_template.h > /<<PKGBUILDDIR>>/src/theory/builtin/kinds > /<<PKGBUILDDIR>>/src/theory/booleans/kinds > /<<PKGBUILDDIR>>/src/theory/uf/kinds /<<PKGBUILDDIR>>/src/theory/arith/kinds > /<<PKGBUILDDIR>>/src/theory/bv/kinds /<<PKGBUILDDIR>>/src/theory/fp/kinds > /<<PKGBUILDDIR>>/src/theory/arrays/kinds > /<<PKGBUILDDIR>>/src/theory/datatypes/kinds > /<<PKGBUILDDIR>>/src/theory/sep/kinds /<<PKGBUILDDIR>>/src/theory/sets/kinds > /<<PKGBUILDDIR>>/src/theory/strings/kinds > /<<PKGBUILDDIR>>/src/theory/quantifiers/kinds > > /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/theory/theory_traits.h > [ 1%] Generating Debug_tags.tmp > [ 1%] Built target gen-gitinfo > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/base && > /<<PKGBUILDDIR>>/src/base/gentmptags.sh /<<PKGBUILDDIR>>/src/base Debug > /<<PKGBUILDDIR>>/src/api/cvc4cpp.cpp\ /<<PKGBUILDDIR>>/src/api/cvc4cpp.h\ > /<<PKGBUILDDIR>>/src/api/cvc4cppkind.h\ /<<PKGBUILDDIR>>/src/base/check.cpp\ > /<<PKGBUILDDIR>>/src/base/check.h\ > /<<PKGBUILDDIR>>/src/base/configuration.cpp\ > /<<PKGBUILDDIR>>/src/base/configuration.h\ > /<<PKGBUILDDIR>>/src/base/configuration_private.h\ > /<<PKGBUILDDIR>>/src/base/exception.cpp\ > /<<PKGBUILDDIR>>/src/base/exception.h\ > /<<PKGBUILDDIR>>/src/base/listener.cpp\ /<<PKGBUILDDIR>>/src/base/listener.h\ > /<<PKGBUILDDIR>>/src/base/map_util.h\ > /<<PKGBUILDDIR>>/src/base/modal_exception.h\ > /<<PKGBUILDDIR>>/src/base/output.cpp\ /<<PKGBUILDDIR>>/src/base/output.h\ > /<<PKGBUILDDIR>>/src/bindings/java_iterator_adapter.h\ > /<<PKGBUILDDIR>>/src/bindings/java_stream_adapters.h\ > /<<PKGBUILDDIR>>/src/bindings/swig.h\ > /<<PKGBUILDDIR>>/src/context/backtrackable.h\ > /<<PKGBUILDDIR>>/src/context/cddense_set.h\ > /<<PKGBUILDDIR>>/src/context/cdhashmap.h\ > /<<PKGBUILDDIR>>/src/context/cdhashmap_forward.h\ > /<<PKGBUILDDIR>>/src/context/cdhashset.h\ > /<<PKGBUILDDIR>>/src/context/cdhashset_forward.h\ > /<<PKGBUILDDIR>>/src/context/cdinsert_hashmap.h\ > /<<PKGBUILDDIR>>/src/context/cdinsert_hashmap_forward.h\ > /<<PKGBUILDDIR>>/src/context/cdlist.h\ > /<<PKGBUILDDIR>>/src/context/cdlist_forward.h\ > /<<PKGBUILDDIR>>/src/context/cdmaybe.h\ /<<PKGBUILDDIR>>/src/context/cdo.h\ > /<<PKGBUILDDIR>>/src/context/cdqueue.h\ > /<<PKGBUILDDIR>>/src/context/cdtrail_queue.h\ > /<<PKGBUILDDIR>>/src/context/context.cpp\ > /<<PKGBUILDDIR>>/src/context/context.h\ > /<<PKGBUILDDIR>>/src/context/context_mm.cpp\ > /<<PKGBUILDDIR>>/src/context/context_mm.h\ > /<<PKGBUILDDIR>>/src/decision/decision_attributes.h\ > /<<PKGBUILDDIR>>/src/decision/decision_engine.cpp\ > /<<PKGBUILDDIR>>/src/decision/decision_engine.h\ > /<<PKGBUILDDIR>>/src/decision/decision_strategy.h\ > /<<PKGBUILDDIR>>/src/decision/justification_heuristic.cpp\ > /<<PKGBUILDDIR>>/src/decision/justification_heuristic.h\ > /<<PKGBUILDDIR>>/src/expr/array.h\ > /<<PKGBUILDDIR>>/src/expr/array_store_all.cpp\ > /<<PKGBUILDDIR>>/src/expr/array_store_all.h\ > /<<PKGBUILDDIR>>/src/expr/ascription_type.h\ > /<<PKGBUILDDIR>>/src/expr/attribute.cpp\ > /<<PKGBUILDDIR>>/src/expr/attribute.h\ > /<<PKGBUILDDIR>>/src/expr/attribute_internals.h\ > /<<PKGBUILDDIR>>/src/expr/attribute_unique_id.h\ > /<<PKGBUILDDIR>>/src/expr/datatype.cpp\ /<<PKGBUILDDIR>>/src/expr/datatype.h\ > /<<PKGBUILDDIR>>/src/expr/dtype.cpp\ /<<PKGBUILDDIR>>/src/expr/dtype.h\ > /<<PKGBUILDDIR>>/src/expr/dtype_cons.cpp\ > /<<PKGBUILDDIR>>/src/expr/dtype_cons.h\ > /<<PKGBUILDDIR>>/src/expr/dtype_selector.cpp\ > /<<PKGBUILDDIR>>/src/expr/dtype_selector.h\ > /<<PKGBUILDDIR>>/src/expr/emptyset.cpp\ /<<PKGBUILDDIR>>/src/expr/emptyset.h\ > /<<PKGBUILDDIR>>/src/expr/expr_iomanip.cpp\ > /<<PKGBUILDDIR>>/src/expr/expr_iomanip.h\ > /<<PKGBUILDDIR>>/src/expr/expr_manager_scope.h\ > /<<PKGBUILDDIR>>/src/expr/expr_manager_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/expr_manager_template.h\ > /<<PKGBUILDDIR>>/src/expr/expr_sequence.cpp\ > /<<PKGBUILDDIR>>/src/expr/expr_sequence.h\ > /<<PKGBUILDDIR>>/src/expr/expr_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/expr_template.h\ > /<<PKGBUILDDIR>>/src/expr/kind_map.h\ > /<<PKGBUILDDIR>>/src/expr/kind_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/kind_template.h\ > /<<PKGBUILDDIR>>/src/expr/lazy_proof.cpp\ > /<<PKGBUILDDIR>>/src/expr/lazy_proof.h\ > /<<PKGBUILDDIR>>/src/expr/match_trie.cpp\ > /<<PKGBUILDDIR>>/src/expr/match_trie.h\ > /<<PKGBUILDDIR>>/src/expr/metakind_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/metakind_template.h\ > /<<PKGBUILDDIR>>/src/expr/node.cpp\ /<<PKGBUILDDIR>>/src/expr/node.h\ > /<<PKGBUILDDIR>>/src/expr/node_algorithm.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_algorithm.h\ > /<<PKGBUILDDIR>>/src/expr/node_builder.h\ > /<<PKGBUILDDIR>>/src/expr/node_manager.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_manager.h\ > /<<PKGBUILDDIR>>/src/expr/node_manager_attributes.h\ > /<<PKGBUILDDIR>>/src/expr/node_manager_listeners.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_manager_listeners.h\ > /<<PKGBUILDDIR>>/src/expr/node_self_iterator.h\ > /<<PKGBUILDDIR>>/src/expr/node_traversal.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_traversal.h\ > /<<PKGBUILDDIR>>/src/expr/node_trie.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_trie.h\ > /<<PKGBUILDDIR>>/src/expr/node_value.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_value.h\ > /<<PKGBUILDDIR>>/src/expr/node_visitor.h\ > /<<PKGBUILDDIR>>/src/expr/proof.cpp\ /<<PKGBUILDDIR>>/src/expr/proof.h\ > /<<PKGBUILDDIR>>/src/expr/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_checker.h\ > /<<PKGBUILDDIR>>/src/expr/proof_generator.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_generator.h\ > /<<PKGBUILDDIR>>/src/expr/proof_node.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_node.h\ > /<<PKGBUILDDIR>>/src/expr/proof_node_algorithm.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_node_algorithm.h\ > /<<PKGBUILDDIR>>/src/expr/proof_node_manager.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_node_manager.h\ > /<<PKGBUILDDIR>>/src/expr/proof_node_to_sexpr.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_node_to_sexpr.h\ > /<<PKGBUILDDIR>>/src/expr/proof_rule.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_rule.h\ > /<<PKGBUILDDIR>>/src/expr/proof_step_buffer.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_step_buffer.h\ > /<<PKGBUILDDIR>>/src/expr/record.cpp\ /<<PKGBUILDDIR>>/src/expr/record.h\ > /<<PKGBUILDDIR>>/src/expr/sequence.cpp\ /<<PKGBUILDDIR>>/src/expr/sequence.h\ > /<<PKGBUILDDIR>>/src/expr/skolem_manager.cpp\ > /<<PKGBUILDDIR>>/src/expr/skolem_manager.h\ > /<<PKGBUILDDIR>>/src/expr/sygus_datatype.cpp\ > /<<PKGBUILDDIR>>/src/expr/sygus_datatype.h\ > /<<PKGBUILDDIR>>/src/expr/symbol_table.cpp\ > /<<PKGBUILDDIR>>/src/expr/symbol_table.h\ > /<<PKGBUILDDIR>>/src/expr/term_canonize.cpp\ > /<<PKGBUILDDIR>>/src/expr/term_canonize.h\ > /<<PKGBUILDDIR>>/src/expr/term_conversion_proof_generator.cpp\ > /<<PKGBUILDDIR>>/src/expr/term_conversion_proof_generator.h\ > /<<PKGBUILDDIR>>/src/expr/type.cpp\ /<<PKGBUILDDIR>>/src/expr/type.h\ > /<<PKGBUILDDIR>>/src/expr/type_checker.h\ > /<<PKGBUILDDIR>>/src/expr/type_checker_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/type_checker_util.h\ > /<<PKGBUILDDIR>>/src/expr/type_matcher.cpp\ > /<<PKGBUILDDIR>>/src/expr/type_matcher.h\ > /<<PKGBUILDDIR>>/src/expr/type_node.cpp\ > /<<PKGBUILDDIR>>/src/expr/type_node.h\ > /<<PKGBUILDDIR>>/src/expr/type_properties_template.h\ > /<<PKGBUILDDIR>>/src/expr/uninterpreted_constant.cpp\ > /<<PKGBUILDDIR>>/src/expr/uninterpreted_constant.h\ > /<<PKGBUILDDIR>>/src/expr/variable_type_map.h\ > /<<PKGBUILDDIR>>/src/include/cvc4.h\ > /<<PKGBUILDDIR>>/src/include/cvc4_private.h\ > /<<PKGBUILDDIR>>/src/include/cvc4_private_library.h\ > /<<PKGBUILDDIR>>/src/include/cvc4_public.h\ > /<<PKGBUILDDIR>>/src/include/cvc4parser_private.h\ > /<<PKGBUILDDIR>>/src/include/cvc4parser_public.h\ > /<<PKGBUILDDIR>>/src/lib/clock_gettime.h\ /<<PKGBUILDDIR>>/src/lib/ffs.h\ > /<<PKGBUILDDIR>>/src/lib/replacements.h\ /<<PKGBUILDDIR>>/src/lib/strtok_r.h\ > /<<PKGBUILDDIR>>/src/main/command_executor.cpp\ > /<<PKGBUILDDIR>>/src/main/command_executor.h\ > /<<PKGBUILDDIR>>/src/main/driver_unified.cpp\ > /<<PKGBUILDDIR>>/src/main/interactive_shell.cpp\ > /<<PKGBUILDDIR>>/src/main/interactive_shell.h\ > /<<PKGBUILDDIR>>/src/main/main.cpp\ /<<PKGBUILDDIR>>/src/main/main.h\ > /<<PKGBUILDDIR>>/src/main/util.cpp\ > /<<PKGBUILDDIR>>/src/options/base_handlers.h\ > /<<PKGBUILDDIR>>/src/options/decision_weight.h\ > /<<PKGBUILDDIR>>/src/options/didyoumean.cpp\ > /<<PKGBUILDDIR>>/src/options/didyoumean.h\ > /<<PKGBUILDDIR>>/src/options/didyoumean_test.cpp\ > /<<PKGBUILDDIR>>/src/options/language.cpp\ > /<<PKGBUILDDIR>>/src/options/language.h\ > /<<PKGBUILDDIR>>/src/options/module_template.cpp\ > /<<PKGBUILDDIR>>/src/options/module_template.h\ > /<<PKGBUILDDIR>>/src/options/open_ostream.cpp\ > /<<PKGBUILDDIR>>/src/options/open_ostream.h\ > /<<PKGBUILDDIR>>/src/options/option_exception.cpp\ > /<<PKGBUILDDIR>>/src/options/option_exception.h\ > /<<PKGBUILDDIR>>/src/options/options.h\ > /<<PKGBUILDDIR>>/src/options/options_handler.cpp\ > /<<PKGBUILDDIR>>/src/options/options_handler.h\ > /<<PKGBUILDDIR>>/src/options/options_holder_template.h\ > /<<PKGBUILDDIR>>/src/options/options_public_functions.cpp\ > /<<PKGBUILDDIR>>/src/options/options_template.cpp\ > /<<PKGBUILDDIR>>/src/options/printer_modes.cpp\ > /<<PKGBUILDDIR>>/src/options/printer_modes.h\ > /<<PKGBUILDDIR>>/src/options/set_language.cpp\ > /<<PKGBUILDDIR>>/src/options/set_language.h\ > /<<PKGBUILDDIR>>/src/parser/antlr_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/antlr_input.h\ > /<<PKGBUILDDIR>>/src/parser/antlr_input_imports.cpp\ > /<<PKGBUILDDIR>>/src/parser/antlr_line_buffered_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/antlr_line_buffered_input.h\ > /<<PKGBUILDDIR>>/src/parser/antlr_tracing.h\ > /<<PKGBUILDDIR>>/src/parser/bounded_token_buffer.cpp\ > /<<PKGBUILDDIR>>/src/parser/bounded_token_buffer.h\ > /<<PKGBUILDDIR>>/src/parser/bounded_token_factory.cpp\ > /<<PKGBUILDDIR>>/src/parser/bounded_token_factory.h\ > /<<PKGBUILDDIR>>/src/parser/cvc/Cvc.g\ > /<<PKGBUILDDIR>>/src/parser/cvc/cvc.cpp\ > /<<PKGBUILDDIR>>/src/parser/cvc/cvc.h\ > /<<PKGBUILDDIR>>/src/parser/cvc/cvc_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/cvc/cvc_input.h\ > /<<PKGBUILDDIR>>/src/parser/input.cpp\ /<<PKGBUILDDIR>>/src/parser/input.h\ > /<<PKGBUILDDIR>>/src/parser/line_buffer.cpp\ > /<<PKGBUILDDIR>>/src/parser/line_buffer.h\ > /<<PKGBUILDDIR>>/src/parser/memory_mapped_input_buffer.cpp\ > /<<PKGBUILDDIR>>/src/parser/memory_mapped_input_buffer.h\ > /<<PKGBUILDDIR>>/src/parser/parse_op.cpp\ > /<<PKGBUILDDIR>>/src/parser/parse_op.h\ > /<<PKGBUILDDIR>>/src/parser/parser.cpp\ /<<PKGBUILDDIR>>/src/parser/parser.h\ > /<<PKGBUILDDIR>>/src/parser/parser_builder.cpp\ > /<<PKGBUILDDIR>>/src/parser/parser_builder.h\ > /<<PKGBUILDDIR>>/src/parser/parser_exception.h\ > /<<PKGBUILDDIR>>/src/parser/smt2/Smt2.g\ > /<<PKGBUILDDIR>>/src/parser/smt2/smt2.cpp\ > /<<PKGBUILDDIR>>/src/parser/smt2/smt2.h\ > /<<PKGBUILDDIR>>/src/parser/smt2/smt2_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/smt2/smt2_input.h\ > /<<PKGBUILDDIR>>/src/parser/smt2/sygus_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/smt2/sygus_input.h\ > /<<PKGBUILDDIR>>/src/parser/tptp/Tptp.g\ > /<<PKGBUILDDIR>>/src/parser/tptp/tptp.cpp\ > /<<PKGBUILDDIR>>/src/parser/tptp/tptp.h\ > /<<PKGBUILDDIR>>/src/parser/tptp/tptp_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/tptp/tptp_input.h\ > /<<PKGBUILDDIR>>/src/preprocessing/assertion_pipeline.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/assertion_pipeline.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ackermann.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ackermann.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/apply_substs.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/apply_substs.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bool_to_bv.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bool_to_bv.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_abstraction.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_abstraction.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_eager_atoms.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_eager_atoms.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_gauss.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_gauss.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_intro_pow2.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_intro_pow2.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_to_bool.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_to_bool.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_to_int.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_to_int.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/extended_rewriter_pass.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/extended_rewriter_pass.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/global_negate.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/global_negate.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ho_elim.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ho_elim.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/int_to_bv.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/int_to_bv.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ite_removal.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ite_removal.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ite_simp.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ite_simp.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/miplib_trick.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/miplib_trick.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/nl_ext_purify.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/nl_ext_purify.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/non_clausal_simp.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/non_clausal_simp.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/pseudo_boolean_processor.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/pseudo_boolean_processor.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/quantifier_macros.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/quantifier_macros.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/quantifiers_preprocess.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/quantifiers_preprocess.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/real_to_int.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/real_to_int.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/rewrite.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/rewrite.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sep_skolem_emp.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sep_skolem_emp.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sort_infer.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sort_infer.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/static_learning.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/static_learning.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sygus_inference.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sygus_inference.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/synth_rew_rules.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/synth_rew_rules.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/theory_preprocess.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/theory_preprocess.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/unconstrained_simplifier.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/unconstrained_simplifier.h\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass.h\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass_context.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass_context.h\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass_registry.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass_registry.h\ > /<<PKGBUILDDIR>>/src/preprocessing/util/ite_utilities.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/util/ite_utilities.h\ > /<<PKGBUILDDIR>>/src/printer/ast/ast_printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/ast/ast_printer.h\ > /<<PKGBUILDDIR>>/src/printer/cvc/cvc_printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/cvc/cvc_printer.h\ > /<<PKGBUILDDIR>>/src/printer/dagification_visitor.cpp\ > /<<PKGBUILDDIR>>/src/printer/dagification_visitor.h\ > /<<PKGBUILDDIR>>/src/printer/printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/printer.h\ > /<<PKGBUILDDIR>>/src/printer/smt2/smt2_printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/smt2/smt2_printer.h\ > /<<PKGBUILDDIR>>/src/printer/sygus_print_callback.cpp\ > /<<PKGBUILDDIR>>/src/printer/sygus_print_callback.h\ > /<<PKGBUILDDIR>>/src/printer/tptp/tptp_printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/tptp/tptp_printer.h\ > /<<PKGBUILDDIR>>/src/proof/arith_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/arith_proof.h\ > /<<PKGBUILDDIR>>/src/proof/arith_proof_recorder.cpp\ > /<<PKGBUILDDIR>>/src/proof/arith_proof_recorder.h\ > /<<PKGBUILDDIR>>/src/proof/array_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/array_proof.h\ > /<<PKGBUILDDIR>>/src/proof/bitvector_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/bitvector_proof.h\ > /<<PKGBUILDDIR>>/src/proof/clausal_bitvector_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/clausal_bitvector_proof.h\ > /<<PKGBUILDDIR>>/src/proof/clause_id.h\ > /<<PKGBUILDDIR>>/src/proof/cnf_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/cnf_proof.h\ > /<<PKGBUILDDIR>>/src/proof/dimacs.cpp\ /<<PKGBUILDDIR>>/src/proof/dimacs.h\ > /<<PKGBUILDDIR>>/src/proof/drat/drat_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/drat/drat_proof.h\ > /<<PKGBUILDDIR>>/src/proof/er/er_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/er/er_proof.h\ > /<<PKGBUILDDIR>>/src/proof/lemma_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/lemma_proof.h\ > /<<PKGBUILDDIR>>/src/proof/lfsc_proof_printer.cpp\ > /<<PKGBUILDDIR>>/src/proof/lfsc_proof_printer.h\ > /<<PKGBUILDDIR>>/src/proof/lrat/lrat_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/lrat/lrat_proof.h\ > /<<PKGBUILDDIR>>/src/proof/proof.h\ > /<<PKGBUILDDIR>>/src/proof/proof_manager.cpp\ > /<<PKGBUILDDIR>>/src/proof/proof_manager.h\ > /<<PKGBUILDDIR>>/src/proof/proof_output_channel.cpp\ > /<<PKGBUILDDIR>>/src/proof/proof_output_channel.h\ > /<<PKGBUILDDIR>>/src/proof/proof_utils.cpp\ > /<<PKGBUILDDIR>>/src/proof/proof_utils.h\ > /<<PKGBUILDDIR>>/src/proof/resolution_bitvector_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/resolution_bitvector_proof.h\ > /<<PKGBUILDDIR>>/src/proof/sat_proof.h\ > /<<PKGBUILDDIR>>/src/proof/sat_proof_implementation.h\ > /<<PKGBUILDDIR>>/src/proof/simplify_boolean_node.cpp\ > /<<PKGBUILDDIR>>/src/proof/simplify_boolean_node.h\ > /<<PKGBUILDDIR>>/src/proof/skolemization_manager.cpp\ > /<<PKGBUILDDIR>>/src/proof/skolemization_manager.h\ > /<<PKGBUILDDIR>>/src/proof/theory_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/theory_proof.h\ > /<<PKGBUILDDIR>>/src/proof/uf_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/uf_proof.h\ > /<<PKGBUILDDIR>>/src/proof/unsat_core.cpp\ > /<<PKGBUILDDIR>>/src/proof/unsat_core.h\ > /<<PKGBUILDDIR>>/src/prop/bv_sat_solver_notify.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/bvminisat.cpp\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/bvminisat.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/Dimacs.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/Main.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/Solver.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/Solver.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/SolverTypes.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Alg.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Alloc.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Heap.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/IntTypes.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Map.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Queue.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Sort.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Vec.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/XAlloc.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/simp/Main.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/simp/SimpSolver.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/simp/SimpSolver.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/Options.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/Options.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/ParseUtils.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/System.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/System.h\ > /<<PKGBUILDDIR>>/src/prop/cadical.cpp\ /<<PKGBUILDDIR>>/src/prop/cadical.h\ > /<<PKGBUILDDIR>>/src/prop/cnf_stream.cpp\ > /<<PKGBUILDDIR>>/src/prop/cnf_stream.h\ > /<<PKGBUILDDIR>>/src/prop/cryptominisat.cpp\ > /<<PKGBUILDDIR>>/src/prop/cryptominisat.h\ > /<<PKGBUILDDIR>>/src/prop/kissat.cpp\ /<<PKGBUILDDIR>>/src/prop/kissat.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/Dimacs.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/Main.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/Solver.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/Solver.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/SolverTypes.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/minisat.cpp\ > /<<PKGBUILDDIR>>/src/prop/minisat/minisat.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Alg.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Alloc.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Heap.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/IntTypes.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Map.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Queue.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Sort.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Vec.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/XAlloc.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/simp/Main.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/simp/SimpSolver.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/simp/SimpSolver.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/Options.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/Options.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/ParseUtils.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/System.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/System.h\ > /<<PKGBUILDDIR>>/src/prop/prop_engine.cpp\ > /<<PKGBUILDDIR>>/src/prop/prop_engine.h\ > /<<PKGBUILDDIR>>/src/prop/registrar.h\ > /<<PKGBUILDDIR>>/src/prop/sat_solver.h\ > /<<PKGBUILDDIR>>/src/prop/sat_solver_factory.cpp\ > /<<PKGBUILDDIR>>/src/prop/sat_solver_factory.h\ > /<<PKGBUILDDIR>>/src/prop/sat_solver_types.cpp\ > /<<PKGBUILDDIR>>/src/prop/sat_solver_types.h\ > /<<PKGBUILDDIR>>/src/prop/theory_proxy.cpp\ > /<<PKGBUILDDIR>>/src/prop/theory_proxy.h\ > /<<PKGBUILDDIR>>/src/smt/command.cpp\ /<<PKGBUILDDIR>>/src/smt/command.h\ > /<<PKGBUILDDIR>>/src/smt/command_list.cpp\ > /<<PKGBUILDDIR>>/src/smt/command_list.h\ > /<<PKGBUILDDIR>>/src/smt/defined_function.h\ > /<<PKGBUILDDIR>>/src/smt/dump.cpp\ /<<PKGBUILDDIR>>/src/smt/dump.h\ > /<<PKGBUILDDIR>>/src/smt/logic_exception.h\ > /<<PKGBUILDDIR>>/src/smt/logic_request.cpp\ > /<<PKGBUILDDIR>>/src/smt/logic_request.h\ > /<<PKGBUILDDIR>>/src/smt/managed_ostreams.cpp\ > /<<PKGBUILDDIR>>/src/smt/managed_ostreams.h\ > /<<PKGBUILDDIR>>/src/smt/model.cpp\ /<<PKGBUILDDIR>>/src/smt/model.h\ > /<<PKGBUILDDIR>>/src/smt/model_blocker.cpp\ > /<<PKGBUILDDIR>>/src/smt/model_blocker.h\ > /<<PKGBUILDDIR>>/src/smt/model_core_builder.cpp\ > /<<PKGBUILDDIR>>/src/smt/model_core_builder.h\ > /<<PKGBUILDDIR>>/src/smt/process_assertions.cpp\ > /<<PKGBUILDDIR>>/src/smt/process_assertions.h\ > /<<PKGBUILDDIR>>/src/smt/set_defaults.cpp\ > /<<PKGBUILDDIR>>/src/smt/set_defaults.h\ > /<<PKGBUILDDIR>>/src/smt/smt_engine.cpp\ > /<<PKGBUILDDIR>>/src/smt/smt_engine.h\ > /<<PKGBUILDDIR>>/src/smt/smt_engine_scope.cpp\ > /<<PKGBUILDDIR>>/src/smt/smt_engine_scope.h\ > /<<PKGBUILDDIR>>/src/smt/smt_engine_stats.cpp\ > /<<PKGBUILDDIR>>/src/smt/smt_engine_stats.h\ > /<<PKGBUILDDIR>>/src/smt/smt_statistics_registry.cpp\ > /<<PKGBUILDDIR>>/src/smt/smt_statistics_registry.h\ > /<<PKGBUILDDIR>>/src/smt/term_formula_removal.cpp\ > /<<PKGBUILDDIR>>/src/smt/term_formula_removal.h\ > /<<PKGBUILDDIR>>/src/smt/update_ostream.h\ > /<<PKGBUILDDIR>>/src/smt_util/boolean_simplification.cpp\ > /<<PKGBUILDDIR>>/src/smt_util/boolean_simplification.h\ > /<<PKGBUILDDIR>>/src/smt_util/nary_builder.cpp\ > /<<PKGBUILDDIR>>/src/smt_util/nary_builder.h\ > /<<PKGBUILDDIR>>/src/theory/arith/approx_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/approx_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_ite_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_ite_utils.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_msum.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_msum.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_static_learner.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_static_learner.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_utilities.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_utilities.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arithvar.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arithvar.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arithvar_node_map.h\ > /<<PKGBUILDDIR>>/src/theory/arith/attempt_solution_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/attempt_solution_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/bound_counts.h\ > /<<PKGBUILDDIR>>/src/theory/arith/callbacks.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/callbacks.h\ > /<<PKGBUILDDIR>>/src/theory/arith/congruence_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/congruence_manager.h\ > /<<PKGBUILDDIR>>/src/theory/arith/constraint.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/constraint.h\ > /<<PKGBUILDDIR>>/src/theory/arith/constraint_forward.h\ > /<<PKGBUILDDIR>>/src/theory/arith/cut_log.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/cut_log.h\ > /<<PKGBUILDDIR>>/src/theory/arith/delta_rational.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/delta_rational.h\ > /<<PKGBUILDDIR>>/src/theory/arith/dio_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/dio_solver.h\ > /<<PKGBUILDDIR>>/src/theory/arith/dual_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/dual_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/error_set.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/error_set.h\ > /<<PKGBUILDDIR>>/src/theory/arith/fc_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/fc_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/infer_bounds.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/infer_bounds.h\ > /<<PKGBUILDDIR>>/src/theory/arith/linear_equality.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/linear_equality.h\ > /<<PKGBUILDDIR>>/src/theory/arith/matrix.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/matrix.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_constraint.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_constraint.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_lemma_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_lemma_utils.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_model.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_monomial.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_monomial.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_solver.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nonlinear_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nonlinear_extension.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/transcendental_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/transcendental_solver.h\ > /<<PKGBUILDDIR>>/src/theory/arith/normal_form.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/normal_form.h\ > /<<PKGBUILDDIR>>/src/theory/arith/partial_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/partial_model.h\ > /<<PKGBUILDDIR>>/src/theory/arith/simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/simplex_update.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/simplex_update.h\ > /<<PKGBUILDDIR>>/src/theory/arith/soi_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/soi_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/tableau.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/tableau.h\ > /<<PKGBUILDDIR>>/src/theory/arith/tableau_sizes.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/tableau_sizes.h\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith.h\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith_private.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith_private.h\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith_private_forward.h\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/arith/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/array_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/array_info.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/array_proof_reconstruction.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/array_proof_reconstruction.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/static_fact_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/static_fact_manager.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/union_find.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/union_find.h\ > /<<PKGBUILDDIR>>/src/theory/assertion.cpp\ > /<<PKGBUILDDIR>>/src/theory/assertion.h\ > /<<PKGBUILDDIR>>/src/theory/atom_requests.cpp\ > /<<PKGBUILDDIR>>/src/theory/atom_requests.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/circuit_propagator.cpp\ > /<<PKGBUILDDIR>>/src/theory/booleans/circuit_propagator.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/theory/booleans/proof_checker.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool.cpp\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/theory/builtin/proof_checker.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin.cpp\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/type_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/builtin/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/bv/abstraction.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/abstraction.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/aig_bitblaster.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/aig_bitblaster.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/bitblast_strategies_template.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/bitblast_utils.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/bitblaster.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/eager_bitblaster.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/eager_bitblaster.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/lazy_bitblaster.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/lazy_bitblaster.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_eager_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_eager_solver.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_inequality_graph.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_inequality_graph.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_quick_check.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_quick_check.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_algebraic.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_algebraic.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_bitblast.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_bitblast.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_core.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_core.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_inequality.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_inequality.h\ > /<<PKGBUILDDIR>>/src/theory/bv/slicer.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/slicer.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_core.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_normalization.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_simplification.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_utils.h\ > /<<PKGBUILDDIR>>/src/theory/bv/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/care_graph.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/datatypes_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/datatypes_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_datatype_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_datatype_utils.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_extension.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_simple_sym.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_simple_sym.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes_utils.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/type_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/decision_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/decision_manager.h\ > /<<PKGBUILDDIR>>/src/theory/decision_strategy.cpp\ > /<<PKGBUILDDIR>>/src/theory/decision_strategy.h\ > /<<PKGBUILDDIR>>/src/theory/eager_proof_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/eager_proof_generator.h\ > /<<PKGBUILDDIR>>/src/theory/engine_output_channel.cpp\ > /<<PKGBUILDDIR>>/src/theory/engine_output_channel.h\ > /<<PKGBUILDDIR>>/src/theory/evaluator.cpp\ > /<<PKGBUILDDIR>>/src/theory/evaluator.h\ > /<<PKGBUILDDIR>>/src/theory/example/ecdata.cpp\ > /<<PKGBUILDDIR>>/src/theory/example/ecdata.h\ > /<<PKGBUILDDIR>>/src/theory/example/theory_uf_tim.cpp\ > /<<PKGBUILDDIR>>/src/theory/example/theory_uf_tim.h\ > /<<PKGBUILDDIR>>/src/theory/ext_theory.cpp\ > /<<PKGBUILDDIR>>/src/theory/ext_theory.h\ > /<<PKGBUILDDIR>>/src/theory/fp/fp_converter.cpp\ > /<<PKGBUILDDIR>>/src/theory/fp/fp_converter.h\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp.cpp\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp.h\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/fp/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/interrupted.h\ > /<<PKGBUILDDIR>>/src/theory/logic_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/logic_info.h\ > /<<PKGBUILDDIR>>/src/theory/output_channel.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/alpha_equivalence.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/alpha_equivalence.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/anti_skolem.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/anti_skolem.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/bv_inverter.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/bv_inverter.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/bv_inverter_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/bv_inverter_utils.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/candidate_rewrite_database.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/candidate_rewrite_database.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/candidate_rewrite_filter.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/candidate_rewrite_filter.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/vts_term_cache.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/vts_term_cache.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/conjecture_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/conjecture_generator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/dynamic_rewrite.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/dynamic_rewrite.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/candidate_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/candidate_generator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/ho_trigger.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/ho_trigger.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/inst_match_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/inst_match_generator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp\ > > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/inst_strategy_e_matching.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/instantiation_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/instantiation_engine.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/trigger.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/trigger.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/equality_infer.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/equality_infer.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/equality_query.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/equality_query.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/expr_miner.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/expr_miner.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/expr_miner_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/expr_miner_manager.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/extended_rewrite.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/extended_rewrite.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/first_order_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/first_order_model.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/bounded_integers.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/bounded_integers.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/full_model_check.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/full_model_check.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/model_builder.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/model_builder.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/model_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/model_engine.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fun_def_evaluator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fun_def_evaluator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fun_def_process.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fun_def_process.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_match.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_match.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_match_trie.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_match_trie.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_strategy_enumerative.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_strategy_enumerative.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/instantiate.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/instantiate.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/lazy_trie.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/lazy_trie.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/proof_checker.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_conflict_find.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_conflict_find.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_epr.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_epr.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_relevance.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_relevance.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_rep_bound_ext.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_rep_bound_ext.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_split.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_split.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_util.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_util.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quantifiers_attributes.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quantifiers_attributes.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quantifiers_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quantifiers_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/query_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/query_generator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/relevant_domain.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/relevant_domain.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/single_inv_partition.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/single_inv_partition.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/skolemize.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/skolemize.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/solution_filter.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/solution_filter.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/ce_guided_single_inv.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis_core_connective.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis_core_connective.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis_unif.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis_unif.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/enum_stream_substitution.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/enum_stream_substitution.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_eval_cache.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_eval_cache.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_infer.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_infer.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_min_eval.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_min_eval.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_abduct.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_abduct.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_enumerator_basic.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_eval_unfold.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_explain.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_explain.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_cons.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_norm.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_red.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_red.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_invariance.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_invariance.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_module.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_module.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_pbe.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_pbe.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_process_conj.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_process_conj.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_repair_const.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_repair_const.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_stats.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_stats.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_io.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_io.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_rl.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_rl.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_strat.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_strat.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/synth_conjecture.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/synth_conjecture.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/synth_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/synth_engine.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/term_database_sygus.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/term_database_sygus.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/transition_inference.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/transition_inference.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/type_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/type_info.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/type_node_id_trie.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/type_node_id_trie.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus_inst.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus_inst.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus_sampler.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus_sampler.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_database.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_database.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_enumeration.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_enumeration.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_util.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_util.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/theory_quantifiers.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/theory_quantifiers.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/theory_quantifiers_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers_engine.h\ > /<<PKGBUILDDIR>>/src/theory/rep_set.cpp\ > /<<PKGBUILDDIR>>/src/theory/rep_set.h\ > /<<PKGBUILDDIR>>/src/theory/rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/rewriter_attributes.h\ > /<<PKGBUILDDIR>>/src/theory/rewriter_tables_template.h\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep.cpp\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep.h\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/sets/cardinality_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/cardinality_extension.h\ > /<<PKGBUILDDIR>>/src/theory/sets/inference_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/inference_manager.h\ > /<<PKGBUILDDIR>>/src/theory/sets/normal_form.h\ > /<<PKGBUILDDIR>>/src/theory/sets/rels_utils.h\ > /<<PKGBUILDDIR>>/src/theory/sets/skolem_cache.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/skolem_cache.h\ > /<<PKGBUILDDIR>>/src/theory/sets/solver_state.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/solver_state.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_private.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_private.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_rels.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_rels.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_type_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/shared_terms_database.cpp\ > /<<PKGBUILDDIR>>/src/theory/shared_terms_database.h\ > /<<PKGBUILDDIR>>/src/theory/smt_engine_subsolver.cpp\ > /<<PKGBUILDDIR>>/src/theory/smt_engine_subsolver.h\ > /<<PKGBUILDDIR>>/src/theory/sort_inference.cpp\ > /<<PKGBUILDDIR>>/src/theory/sort_inference.h\ > /<<PKGBUILDDIR>>/src/theory/strings/arith_entail.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/arith_entail.h\ > /<<PKGBUILDDIR>>/src/theory/strings/base_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/base_solver.h\ > /<<PKGBUILDDIR>>/src/theory/strings/core_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/core_solver.h\ > /<<PKGBUILDDIR>>/src/theory/strings/eqc_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/eqc_info.h\ > /<<PKGBUILDDIR>>/src/theory/strings/extf_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/extf_solver.h\ > /<<PKGBUILDDIR>>/src/theory/strings/infer_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/infer_info.h\ > /<<PKGBUILDDIR>>/src/theory/strings/inference_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/inference_manager.h\ > /<<PKGBUILDDIR>>/src/theory/strings/normal_form.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/normal_form.h\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_elim.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_elim.h\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_entail.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_entail.h\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_operation.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_operation.h\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_solver.h\ > /<<PKGBUILDDIR>>/src/theory/strings/rewrites.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/rewrites.h\ > /<<PKGBUILDDIR>>/src/theory/strings/sequences_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/sequences_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/strings/sequences_stats.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/sequences_stats.h\ > /<<PKGBUILDDIR>>/src/theory/strings/skolem_cache.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/skolem_cache.h\ > /<<PKGBUILDDIR>>/src/theory/strings/solver_state.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/solver_state.h\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_entail.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_entail.h\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_fmf.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_fmf.h\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/strings/term_registry.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/term_registry.h\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings.h\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_preprocess.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_preprocess.h\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_utils.h\ > /<<PKGBUILDDIR>>/src/theory/strings/type_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/strings/word.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/word.h\ > /<<PKGBUILDDIR>>/src/theory/subs_minimize.cpp\ > /<<PKGBUILDDIR>>/src/theory/subs_minimize.h\ > /<<PKGBUILDDIR>>/src/theory/substitutions.cpp\ > /<<PKGBUILDDIR>>/src/theory/substitutions.h\ > /<<PKGBUILDDIR>>/src/theory/term_registration_visitor.cpp\ > /<<PKGBUILDDIR>>/src/theory/term_registration_visitor.h\ > /<<PKGBUILDDIR>>/src/theory/theory.cpp\ /<<PKGBUILDDIR>>/src/theory/theory.h\ > /<<PKGBUILDDIR>>/src/theory/theory_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_engine.h\ > /<<PKGBUILDDIR>>/src/theory/theory_id.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_id.h\ > /<<PKGBUILDDIR>>/src/theory/theory_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_model.h\ > /<<PKGBUILDDIR>>/src/theory/theory_model_builder.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_model_builder.h\ > /<<PKGBUILDDIR>>/src/theory/theory_preprocessor.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_preprocessor.h\ > /<<PKGBUILDDIR>>/src/theory/theory_proof_step_buffer.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_proof_step_buffer.h\ > /<<PKGBUILDDIR>>/src/theory/theory_registrar.h\ > /<<PKGBUILDDIR>>/src/theory/theory_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/theory_test_utils.h\ > /<<PKGBUILDDIR>>/src/theory/theory_traits_template.h\ > /<<PKGBUILDDIR>>/src/theory/trust_node.cpp\ > /<<PKGBUILDDIR>>/src/theory/trust_node.h\ > /<<PKGBUILDDIR>>/src/theory/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/type_enumerator_template.cpp\ > /<<PKGBUILDDIR>>/src/theory/type_set.cpp\ > /<<PKGBUILDDIR>>/src/theory/type_set.h\ > /<<PKGBUILDDIR>>/src/theory/uf/cardinality_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/cardinality_extension.h\ > /<<PKGBUILDDIR>>/src/theory/uf/equality_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/equality_engine.h\ > /<<PKGBUILDDIR>>/src/theory/uf/equality_engine_types.h\ > /<<PKGBUILDDIR>>/src/theory/uf/ho_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/ho_extension.h\ > /<<PKGBUILDDIR>>/src/theory/uf/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/proof_checker.h\ > /<<PKGBUILDDIR>>/src/theory/uf/symmetry_breaker.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/symmetry_breaker.h\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf.h\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf_model.h\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/valuation.cpp\ > /<<PKGBUILDDIR>>/src/theory/valuation.h\ > /<<PKGBUILDDIR>>/src/util/abstract_value.cpp\ > /<<PKGBUILDDIR>>/src/util/abstract_value.h\ > /<<PKGBUILDDIR>>/src/util/bin_heap.h\ > /<<PKGBUILDDIR>>/src/util/bitvector.cpp\ > /<<PKGBUILDDIR>>/src/util/bitvector.h\ /<<PKGBUILDDIR>>/src/util/bool.h\ > /<<PKGBUILDDIR>>/src/util/cardinality.cpp\ > /<<PKGBUILDDIR>>/src/util/cardinality.h\ > /<<PKGBUILDDIR>>/src/util/dense_map.h\ > /<<PKGBUILDDIR>>/src/util/divisible.cpp\ > /<<PKGBUILDDIR>>/src/util/divisible.h\ > /<<PKGBUILDDIR>>/src/util/floatingpoint.cpp\ > /<<PKGBUILDDIR>>/src/util/gmp_util.h\ /<<PKGBUILDDIR>>/src/util/hash.h\ > /<<PKGBUILDDIR>>/src/util/index.cpp\ /<<PKGBUILDDIR>>/src/util/index.h\ > /<<PKGBUILDDIR>>/src/util/integer_cln_imp.cpp\ > /<<PKGBUILDDIR>>/src/util/integer_cln_imp.h\ > /<<PKGBUILDDIR>>/src/util/integer_gmp_imp.cpp\ > /<<PKGBUILDDIR>>/src/util/integer_gmp_imp.h\ > /<<PKGBUILDDIR>>/src/util/maybe.h\ > /<<PKGBUILDDIR>>/src/util/ostream_util.cpp\ > /<<PKGBUILDDIR>>/src/util/ostream_util.h\ /<<PKGBUILDDIR>>/src/util/proof.h\ > /<<PKGBUILDDIR>>/src/util/random.cpp\ /<<PKGBUILDDIR>>/src/util/random.h\ > /<<PKGBUILDDIR>>/src/util/rational_cln_imp.cpp\ > /<<PKGBUILDDIR>>/src/util/rational_cln_imp.h\ > /<<PKGBUILDDIR>>/src/util/rational_gmp_imp.cpp\ > /<<PKGBUILDDIR>>/src/util/rational_gmp_imp.h\ > /<<PKGBUILDDIR>>/src/util/regexp.cpp\ /<<PKGBUILDDIR>>/src/util/regexp.h\ > /<<PKGBUILDDIR>>/src/util/resource_manager.cpp\ > /<<PKGBUILDDIR>>/src/util/resource_manager.h\ > /<<PKGBUILDDIR>>/src/util/result.cpp\ /<<PKGBUILDDIR>>/src/util/result.h\ > /<<PKGBUILDDIR>>/src/util/safe_print.cpp\ > /<<PKGBUILDDIR>>/src/util/safe_print.h\ > /<<PKGBUILDDIR>>/src/util/sampler.cpp\ /<<PKGBUILDDIR>>/src/util/sampler.h\ > /<<PKGBUILDDIR>>/src/util/sexpr.cpp\ /<<PKGBUILDDIR>>/src/util/sexpr.h\ > /<<PKGBUILDDIR>>/src/util/smt2_quote_string.cpp\ > /<<PKGBUILDDIR>>/src/util/smt2_quote_string.h\ > /<<PKGBUILDDIR>>/src/util/statistics.cpp\ > /<<PKGBUILDDIR>>/src/util/statistics.h\ > /<<PKGBUILDDIR>>/src/util/statistics_registry.cpp\ > /<<PKGBUILDDIR>>/src/util/statistics_registry.h\ > /<<PKGBUILDDIR>>/src/util/string.cpp\ /<<PKGBUILDDIR>>/src/util/string.h\ > /<<PKGBUILDDIR>>/src/util/tuple.h\ > /<<PKGBUILDDIR>>/src/util/unsafe_interrupt_exception.h\ > /<<PKGBUILDDIR>>/src/util/utility.cpp\ /<<PKGBUILDDIR>>/src/util/utility.h > [ 2%] Generating rewriter_tables.h > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/theory && > /<<PKGBUILDDIR>>/src/theory/mkrewriter > /<<PKGBUILDDIR>>/src/theory/rewriter_tables_template.h > /<<PKGBUILDDIR>>/src/theory/builtin/kinds > /<<PKGBUILDDIR>>/src/theory/booleans/kinds > /<<PKGBUILDDIR>>/src/theory/uf/kinds /<<PKGBUILDDIR>>/src/theory/arith/kinds > /<<PKGBUILDDIR>>/src/theory/bv/kinds /<<PKGBUILDDIR>>/src/theory/fp/kinds > /<<PKGBUILDDIR>>/src/theory/arrays/kinds > /<<PKGBUILDDIR>>/src/theory/datatypes/kinds > /<<PKGBUILDDIR>>/src/theory/sep/kinds /<<PKGBUILDDIR>>/src/theory/sets/kinds > /<<PKGBUILDDIR>>/src/theory/strings/kinds > /<<PKGBUILDDIR>>/src/theory/quantifiers/kinds > > /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/theory/rewriter_tables.h > grep: warning: stray \ before " > grep: warning: stray \ before " > [ 3%] Generating type_checker.cpp > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr && /usr/bin/cmake -E env > CMAKE_SOURCE_DIR=/<<PKGBUILDDIR>> /<<PKGBUILDDIR>>/src/expr/mkexpr > /<<PKGBUILDDIR>>/src/expr/type_checker_template.cpp > /<<PKGBUILDDIR>>/src/theory/builtin/kinds > /<<PKGBUILDDIR>>/src/theory/booleans/kinds > /<<PKGBUILDDIR>>/src/theory/uf/kinds /<<PKGBUILDDIR>>/src/theory/arith/kinds > /<<PKGBUILDDIR>>/src/theory/bv/kinds /<<PKGBUILDDIR>>/src/theory/fp/kinds > /<<PKGBUILDDIR>>/src/theory/arrays/kinds > /<<PKGBUILDDIR>>/src/theory/datatypes/kinds > /<<PKGBUILDDIR>>/src/theory/sep/kinds /<<PKGBUILDDIR>>/src/theory/sets/kinds > /<<PKGBUILDDIR>>/src/theory/strings/kinds > /<<PKGBUILDDIR>>/src/theory/quantifiers/kinds > > /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr/type_checker.cpp > [ 3%] Generating Trace_tags.tmp > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/base && > /<<PKGBUILDDIR>>/src/base/gentmptags.sh /<<PKGBUILDDIR>>/src/base Trace > /<<PKGBUILDDIR>>/src/api/cvc4cpp.cpp\ /<<PKGBUILDDIR>>/src/api/cvc4cpp.h\ > /<<PKGBUILDDIR>>/src/api/cvc4cppkind.h\ /<<PKGBUILDDIR>>/src/base/check.cpp\ > /<<PKGBUILDDIR>>/src/base/check.h\ > /<<PKGBUILDDIR>>/src/base/configuration.cpp\ > /<<PKGBUILDDIR>>/src/base/configuration.h\ > /<<PKGBUILDDIR>>/src/base/configuration_private.h\ > /<<PKGBUILDDIR>>/src/base/exception.cpp\ > /<<PKGBUILDDIR>>/src/base/exception.h\ > /<<PKGBUILDDIR>>/src/base/listener.cpp\ /<<PKGBUILDDIR>>/src/base/listener.h\ > /<<PKGBUILDDIR>>/src/base/map_util.h\ > /<<PKGBUILDDIR>>/src/base/modal_exception.h\ > /<<PKGBUILDDIR>>/src/base/output.cpp\ /<<PKGBUILDDIR>>/src/base/output.h\ > /<<PKGBUILDDIR>>/src/bindings/java_iterator_adapter.h\ > /<<PKGBUILDDIR>>/src/bindings/java_stream_adapters.h\ > /<<PKGBUILDDIR>>/src/bindings/swig.h\ > /<<PKGBUILDDIR>>/src/context/backtrackable.h\ > /<<PKGBUILDDIR>>/src/context/cddense_set.h\ > /<<PKGBUILDDIR>>/src/context/cdhashmap.h\ > /<<PKGBUILDDIR>>/src/context/cdhashmap_forward.h\ > /<<PKGBUILDDIR>>/src/context/cdhashset.h\ > /<<PKGBUILDDIR>>/src/context/cdhashset_forward.h\ > /<<PKGBUILDDIR>>/src/context/cdinsert_hashmap.h\ > /<<PKGBUILDDIR>>/src/context/cdinsert_hashmap_forward.h\ > /<<PKGBUILDDIR>>/src/context/cdlist.h\ > /<<PKGBUILDDIR>>/src/context/cdlist_forward.h\ > /<<PKGBUILDDIR>>/src/context/cdmaybe.h\ /<<PKGBUILDDIR>>/src/context/cdo.h\ > /<<PKGBUILDDIR>>/src/context/cdqueue.h\ > /<<PKGBUILDDIR>>/src/context/cdtrail_queue.h\ > /<<PKGBUILDDIR>>/src/context/context.cpp\ > /<<PKGBUILDDIR>>/src/context/context.h\ > /<<PKGBUILDDIR>>/src/context/context_mm.cpp\ > /<<PKGBUILDDIR>>/src/context/context_mm.h\ > /<<PKGBUILDDIR>>/src/decision/decision_attributes.h\ > /<<PKGBUILDDIR>>/src/decision/decision_engine.cpp\ > /<<PKGBUILDDIR>>/src/decision/decision_engine.h\ > /<<PKGBUILDDIR>>/src/decision/decision_strategy.h\ > /<<PKGBUILDDIR>>/src/decision/justification_heuristic.cpp\ > /<<PKGBUILDDIR>>/src/decision/justification_heuristic.h\ > /<<PKGBUILDDIR>>/src/expr/array.h\ > /<<PKGBUILDDIR>>/src/expr/array_store_all.cpp\ > /<<PKGBUILDDIR>>/src/expr/array_store_all.h\ > /<<PKGBUILDDIR>>/src/expr/ascription_type.h\ > /<<PKGBUILDDIR>>/src/expr/attribute.cpp\ > /<<PKGBUILDDIR>>/src/expr/attribute.h\ > /<<PKGBUILDDIR>>/src/expr/attribute_internals.h\ > /<<PKGBUILDDIR>>/src/expr/attribute_unique_id.h\ > /<<PKGBUILDDIR>>/src/expr/datatype.cpp\ /<<PKGBUILDDIR>>/src/expr/datatype.h\ > /<<PKGBUILDDIR>>/src/expr/dtype.cpp\ /<<PKGBUILDDIR>>/src/expr/dtype.h\ > /<<PKGBUILDDIR>>/src/expr/dtype_cons.cpp\ > /<<PKGBUILDDIR>>/src/expr/dtype_cons.h\ > /<<PKGBUILDDIR>>/src/expr/dtype_selector.cpp\ > /<<PKGBUILDDIR>>/src/expr/dtype_selector.h\ > /<<PKGBUILDDIR>>/src/expr/emptyset.cpp\ /<<PKGBUILDDIR>>/src/expr/emptyset.h\ > /<<PKGBUILDDIR>>/src/expr/expr_iomanip.cpp\ > /<<PKGBUILDDIR>>/src/expr/expr_iomanip.h\ > /<<PKGBUILDDIR>>/src/expr/expr_manager_scope.h\ > /<<PKGBUILDDIR>>/src/expr/expr_manager_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/expr_manager_template.h\ > /<<PKGBUILDDIR>>/src/expr/expr_sequence.cpp\ > /<<PKGBUILDDIR>>/src/expr/expr_sequence.h\ > /<<PKGBUILDDIR>>/src/expr/expr_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/expr_template.h\ > /<<PKGBUILDDIR>>/src/expr/kind_map.h\ > /<<PKGBUILDDIR>>/src/expr/kind_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/kind_template.h\ > /<<PKGBUILDDIR>>/src/expr/lazy_proof.cpp\ > /<<PKGBUILDDIR>>/src/expr/lazy_proof.h\ > /<<PKGBUILDDIR>>/src/expr/match_trie.cpp\ > /<<PKGBUILDDIR>>/src/expr/match_trie.h\ > /<<PKGBUILDDIR>>/src/expr/metakind_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/metakind_template.h\ > /<<PKGBUILDDIR>>/src/expr/node.cpp\ /<<PKGBUILDDIR>>/src/expr/node.h\ > /<<PKGBUILDDIR>>/src/expr/node_algorithm.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_algorithm.h\ > /<<PKGBUILDDIR>>/src/expr/node_builder.h\ > /<<PKGBUILDDIR>>/src/expr/node_manager.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_manager.h\ > /<<PKGBUILDDIR>>/src/expr/node_manager_attributes.h\ > /<<PKGBUILDDIR>>/src/expr/node_manager_listeners.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_manager_listeners.h\ > /<<PKGBUILDDIR>>/src/expr/node_self_iterator.h\ > /<<PKGBUILDDIR>>/src/expr/node_traversal.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_traversal.h\ > /<<PKGBUILDDIR>>/src/expr/node_trie.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_trie.h\ > /<<PKGBUILDDIR>>/src/expr/node_value.cpp\ > /<<PKGBUILDDIR>>/src/expr/node_value.h\ > /<<PKGBUILDDIR>>/src/expr/node_visitor.h\ > /<<PKGBUILDDIR>>/src/expr/proof.cpp\ /<<PKGBUILDDIR>>/src/expr/proof.h\ > /<<PKGBUILDDIR>>/src/expr/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_checker.h\ > /<<PKGBUILDDIR>>/src/expr/proof_generator.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_generator.h\ > /<<PKGBUILDDIR>>/src/expr/proof_node.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_node.h\ > /<<PKGBUILDDIR>>/src/expr/proof_node_algorithm.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_node_algorithm.h\ > /<<PKGBUILDDIR>>/src/expr/proof_node_manager.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_node_manager.h\ > /<<PKGBUILDDIR>>/src/expr/proof_node_to_sexpr.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_node_to_sexpr.h\ > /<<PKGBUILDDIR>>/src/expr/proof_rule.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_rule.h\ > /<<PKGBUILDDIR>>/src/expr/proof_step_buffer.cpp\ > /<<PKGBUILDDIR>>/src/expr/proof_step_buffer.h\ > /<<PKGBUILDDIR>>/src/expr/record.cpp\ /<<PKGBUILDDIR>>/src/expr/record.h\ > /<<PKGBUILDDIR>>/src/expr/sequence.cpp\ /<<PKGBUILDDIR>>/src/expr/sequence.h\ > /<<PKGBUILDDIR>>/src/expr/skolem_manager.cpp\ > /<<PKGBUILDDIR>>/src/expr/skolem_manager.h\ > /<<PKGBUILDDIR>>/src/expr/sygus_datatype.cpp\ > /<<PKGBUILDDIR>>/src/expr/sygus_datatype.h\ > /<<PKGBUILDDIR>>/src/expr/symbol_table.cpp\ > /<<PKGBUILDDIR>>/src/expr/symbol_table.h\ > /<<PKGBUILDDIR>>/src/expr/term_canonize.cpp\ > /<<PKGBUILDDIR>>/src/expr/term_canonize.h\ > /<<PKGBUILDDIR>>/src/expr/term_conversion_proof_generator.cpp\ > /<<PKGBUILDDIR>>/src/expr/term_conversion_proof_generator.h\ > /<<PKGBUILDDIR>>/src/expr/type.cpp\ /<<PKGBUILDDIR>>/src/expr/type.h\ > /<<PKGBUILDDIR>>/src/expr/type_checker.h\ > /<<PKGBUILDDIR>>/src/expr/type_checker_template.cpp\ > /<<PKGBUILDDIR>>/src/expr/type_checker_util.h\ > /<<PKGBUILDDIR>>/src/expr/type_matcher.cpp\ > /<<PKGBUILDDIR>>/src/expr/type_matcher.h\ > /<<PKGBUILDDIR>>/src/expr/type_node.cpp\ > /<<PKGBUILDDIR>>/src/expr/type_node.h\ > /<<PKGBUILDDIR>>/src/expr/type_properties_template.h\ > /<<PKGBUILDDIR>>/src/expr/uninterpreted_constant.cpp\ > /<<PKGBUILDDIR>>/src/expr/uninterpreted_constant.h\ > /<<PKGBUILDDIR>>/src/expr/variable_type_map.h\ > /<<PKGBUILDDIR>>/src/include/cvc4.h\ > /<<PKGBUILDDIR>>/src/include/cvc4_private.h\ > /<<PKGBUILDDIR>>/src/include/cvc4_private_library.h\ > /<<PKGBUILDDIR>>/src/include/cvc4_public.h\ > /<<PKGBUILDDIR>>/src/include/cvc4parser_private.h\ > /<<PKGBUILDDIR>>/src/include/cvc4parser_public.h\ > /<<PKGBUILDDIR>>/src/lib/clock_gettime.h\ /<<PKGBUILDDIR>>/src/lib/ffs.h\ > /<<PKGBUILDDIR>>/src/lib/replacements.h\ /<<PKGBUILDDIR>>/src/lib/strtok_r.h\ > /<<PKGBUILDDIR>>/src/main/command_executor.cpp\ > /<<PKGBUILDDIR>>/src/main/command_executor.h\ > /<<PKGBUILDDIR>>/src/main/driver_unified.cpp\ > /<<PKGBUILDDIR>>/src/main/interactive_shell.cpp\ > /<<PKGBUILDDIR>>/src/main/interactive_shell.h\ > /<<PKGBUILDDIR>>/src/main/main.cpp\ /<<PKGBUILDDIR>>/src/main/main.h\ > /<<PKGBUILDDIR>>/src/main/util.cpp\ > /<<PKGBUILDDIR>>/src/options/base_handlers.h\ > /<<PKGBUILDDIR>>/src/options/decision_weight.h\ > /<<PKGBUILDDIR>>/src/options/didyoumean.cpp\ > /<<PKGBUILDDIR>>/src/options/didyoumean.h\ > /<<PKGBUILDDIR>>/src/options/didyoumean_test.cpp\ > /<<PKGBUILDDIR>>/src/options/language.cpp\ > /<<PKGBUILDDIR>>/src/options/language.h\ > /<<PKGBUILDDIR>>/src/options/module_template.cpp\ > /<<PKGBUILDDIR>>/src/options/module_template.h\ > /<<PKGBUILDDIR>>/src/options/open_ostream.cpp\ > /<<PKGBUILDDIR>>/src/options/open_ostream.h\ > /<<PKGBUILDDIR>>/src/options/option_exception.cpp\ > /<<PKGBUILDDIR>>/src/options/option_exception.h\ > /<<PKGBUILDDIR>>/src/options/options.h\ > /<<PKGBUILDDIR>>/src/options/options_handler.cpp\ > /<<PKGBUILDDIR>>/src/options/options_handler.h\ > /<<PKGBUILDDIR>>/src/options/options_holder_template.h\ > /<<PKGBUILDDIR>>/src/options/options_public_functions.cpp\ > /<<PKGBUILDDIR>>/src/options/options_template.cpp\ > /<<PKGBUILDDIR>>/src/options/printer_modes.cpp\ > /<<PKGBUILDDIR>>/src/options/printer_modes.h\ > /<<PKGBUILDDIR>>/src/options/set_language.cpp\ > /<<PKGBUILDDIR>>/src/options/set_language.h\ > /<<PKGBUILDDIR>>/src/parser/antlr_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/antlr_input.h\ > /<<PKGBUILDDIR>>/src/parser/antlr_input_imports.cpp\ > /<<PKGBUILDDIR>>/src/parser/antlr_line_buffered_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/antlr_line_buffered_input.h\ > /<<PKGBUILDDIR>>/src/parser/antlr_tracing.h\ > /<<PKGBUILDDIR>>/src/parser/bounded_token_buffer.cpp\ > /<<PKGBUILDDIR>>/src/parser/bounded_token_buffer.h\ > /<<PKGBUILDDIR>>/src/parser/bounded_token_factory.cpp\ > /<<PKGBUILDDIR>>/src/parser/bounded_token_factory.h\ > /<<PKGBUILDDIR>>/src/parser/cvc/Cvc.g\ > /<<PKGBUILDDIR>>/src/parser/cvc/cvc.cpp\ > /<<PKGBUILDDIR>>/src/parser/cvc/cvc.h\ > /<<PKGBUILDDIR>>/src/parser/cvc/cvc_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/cvc/cvc_input.h\ > /<<PKGBUILDDIR>>/src/parser/input.cpp\ /<<PKGBUILDDIR>>/src/parser/input.h\ > /<<PKGBUILDDIR>>/src/parser/line_buffer.cpp\ > /<<PKGBUILDDIR>>/src/parser/line_buffer.h\ > /<<PKGBUILDDIR>>/src/parser/memory_mapped_input_buffer.cpp\ > /<<PKGBUILDDIR>>/src/parser/memory_mapped_input_buffer.h\ > /<<PKGBUILDDIR>>/src/parser/parse_op.cpp\ > /<<PKGBUILDDIR>>/src/parser/parse_op.h\ > /<<PKGBUILDDIR>>/src/parser/parser.cpp\ /<<PKGBUILDDIR>>/src/parser/parser.h\ > /<<PKGBUILDDIR>>/src/parser/parser_builder.cpp\ > /<<PKGBUILDDIR>>/src/parser/parser_builder.h\ > /<<PKGBUILDDIR>>/src/parser/parser_exception.h\ > /<<PKGBUILDDIR>>/src/parser/smt2/Smt2.g\ > /<<PKGBUILDDIR>>/src/parser/smt2/smt2.cpp\ > /<<PKGBUILDDIR>>/src/parser/smt2/smt2.h\ > /<<PKGBUILDDIR>>/src/parser/smt2/smt2_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/smt2/smt2_input.h\ > /<<PKGBUILDDIR>>/src/parser/smt2/sygus_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/smt2/sygus_input.h\ > /<<PKGBUILDDIR>>/src/parser/tptp/Tptp.g\ > /<<PKGBUILDDIR>>/src/parser/tptp/tptp.cpp\ > /<<PKGBUILDDIR>>/src/parser/tptp/tptp.h\ > /<<PKGBUILDDIR>>/src/parser/tptp/tptp_input.cpp\ > /<<PKGBUILDDIR>>/src/parser/tptp/tptp_input.h\ > /<<PKGBUILDDIR>>/src/preprocessing/assertion_pipeline.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/assertion_pipeline.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ackermann.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ackermann.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/apply_substs.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/apply_substs.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bool_to_bv.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bool_to_bv.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_abstraction.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_abstraction.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_eager_atoms.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_eager_atoms.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_gauss.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_gauss.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_intro_pow2.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_intro_pow2.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_to_bool.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_to_bool.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_to_int.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/bv_to_int.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/extended_rewriter_pass.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/extended_rewriter_pass.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/global_negate.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/global_negate.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ho_elim.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ho_elim.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/int_to_bv.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/int_to_bv.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ite_removal.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ite_removal.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ite_simp.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/ite_simp.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/miplib_trick.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/miplib_trick.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/nl_ext_purify.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/nl_ext_purify.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/non_clausal_simp.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/non_clausal_simp.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/pseudo_boolean_processor.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/pseudo_boolean_processor.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/quantifier_macros.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/quantifier_macros.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/quantifiers_preprocess.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/quantifiers_preprocess.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/real_to_int.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/real_to_int.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/rewrite.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/rewrite.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sep_skolem_emp.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sep_skolem_emp.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sort_infer.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sort_infer.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/static_learning.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/static_learning.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sygus_inference.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/sygus_inference.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/synth_rew_rules.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/synth_rew_rules.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/theory_preprocess.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/theory_preprocess.h\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/unconstrained_simplifier.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/passes/unconstrained_simplifier.h\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass.h\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass_context.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass_context.h\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass_registry.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/preprocessing_pass_registry.h\ > /<<PKGBUILDDIR>>/src/preprocessing/util/ite_utilities.cpp\ > /<<PKGBUILDDIR>>/src/preprocessing/util/ite_utilities.h\ > /<<PKGBUILDDIR>>/src/printer/ast/ast_printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/ast/ast_printer.h\ > /<<PKGBUILDDIR>>/src/printer/cvc/cvc_printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/cvc/cvc_printer.h\ > /<<PKGBUILDDIR>>/src/printer/dagification_visitor.cpp\ > /<<PKGBUILDDIR>>/src/printer/dagification_visitor.h\ > /<<PKGBUILDDIR>>/src/printer/printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/printer.h\ > /<<PKGBUILDDIR>>/src/printer/smt2/smt2_printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/smt2/smt2_printer.h\ > /<<PKGBUILDDIR>>/src/printer/sygus_print_callback.cpp\ > /<<PKGBUILDDIR>>/src/printer/sygus_print_callback.h\ > /<<PKGBUILDDIR>>/src/printer/tptp/tptp_printer.cpp\ > /<<PKGBUILDDIR>>/src/printer/tptp/tptp_printer.h\ > /<<PKGBUILDDIR>>/src/proof/arith_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/arith_proof.h\ > /<<PKGBUILDDIR>>/src/proof/arith_proof_recorder.cpp\ > /<<PKGBUILDDIR>>/src/proof/arith_proof_recorder.h\ > /<<PKGBUILDDIR>>/src/proof/array_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/array_proof.h\ > /<<PKGBUILDDIR>>/src/proof/bitvector_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/bitvector_proof.h\ > /<<PKGBUILDDIR>>/src/proof/clausal_bitvector_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/clausal_bitvector_proof.h\ > /<<PKGBUILDDIR>>/src/proof/clause_id.h\ > /<<PKGBUILDDIR>>/src/proof/cnf_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/cnf_proof.h\ > /<<PKGBUILDDIR>>/src/proof/dimacs.cpp\ /<<PKGBUILDDIR>>/src/proof/dimacs.h\ > /<<PKGBUILDDIR>>/src/proof/drat/drat_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/drat/drat_proof.h\ > /<<PKGBUILDDIR>>/src/proof/er/er_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/er/er_proof.h\ > /<<PKGBUILDDIR>>/src/proof/lemma_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/lemma_proof.h\ > /<<PKGBUILDDIR>>/src/proof/lfsc_proof_printer.cpp\ > /<<PKGBUILDDIR>>/src/proof/lfsc_proof_printer.h\ > /<<PKGBUILDDIR>>/src/proof/lrat/lrat_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/lrat/lrat_proof.h\ > /<<PKGBUILDDIR>>/src/proof/proof.h\ > /<<PKGBUILDDIR>>/src/proof/proof_manager.cpp\ > /<<PKGBUILDDIR>>/src/proof/proof_manager.h\ > /<<PKGBUILDDIR>>/src/proof/proof_output_channel.cpp\ > /<<PKGBUILDDIR>>/src/proof/proof_output_channel.h\ > /<<PKGBUILDDIR>>/src/proof/proof_utils.cpp\ > /<<PKGBUILDDIR>>/src/proof/proof_utils.h\ > /<<PKGBUILDDIR>>/src/proof/resolution_bitvector_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/resolution_bitvector_proof.h\ > /<<PKGBUILDDIR>>/src/proof/sat_proof.h\ > /<<PKGBUILDDIR>>/src/proof/sat_proof_implementation.h\ > /<<PKGBUILDDIR>>/src/proof/simplify_boolean_node.cpp\ > /<<PKGBUILDDIR>>/src/proof/simplify_boolean_node.h\ > /<<PKGBUILDDIR>>/src/proof/skolemization_manager.cpp\ > /<<PKGBUILDDIR>>/src/proof/skolemization_manager.h\ > /<<PKGBUILDDIR>>/src/proof/theory_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/theory_proof.h\ > /<<PKGBUILDDIR>>/src/proof/uf_proof.cpp\ > /<<PKGBUILDDIR>>/src/proof/uf_proof.h\ > /<<PKGBUILDDIR>>/src/proof/unsat_core.cpp\ > /<<PKGBUILDDIR>>/src/proof/unsat_core.h\ > /<<PKGBUILDDIR>>/src/prop/bv_sat_solver_notify.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/bvminisat.cpp\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/bvminisat.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/Dimacs.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/Main.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/Solver.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/Solver.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/core/SolverTypes.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Alg.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Alloc.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Heap.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/IntTypes.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Map.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Queue.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Sort.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/Vec.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/mtl/XAlloc.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/simp/Main.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/simp/SimpSolver.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/simp/SimpSolver.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/Options.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/Options.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/ParseUtils.h\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/System.cc\ > /<<PKGBUILDDIR>>/src/prop/bvminisat/utils/System.h\ > /<<PKGBUILDDIR>>/src/prop/cadical.cpp\ /<<PKGBUILDDIR>>/src/prop/cadical.h\ > /<<PKGBUILDDIR>>/src/prop/cnf_stream.cpp\ > /<<PKGBUILDDIR>>/src/prop/cnf_stream.h\ > /<<PKGBUILDDIR>>/src/prop/cryptominisat.cpp\ > /<<PKGBUILDDIR>>/src/prop/cryptominisat.h\ > /<<PKGBUILDDIR>>/src/prop/kissat.cpp\ /<<PKGBUILDDIR>>/src/prop/kissat.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/Dimacs.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/Main.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/Solver.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/Solver.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/core/SolverTypes.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/minisat.cpp\ > /<<PKGBUILDDIR>>/src/prop/minisat/minisat.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Alg.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Alloc.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Heap.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/IntTypes.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Map.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Queue.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Sort.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/Vec.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/mtl/XAlloc.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/simp/Main.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/simp/SimpSolver.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/simp/SimpSolver.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/Options.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/Options.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/ParseUtils.h\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/System.cc\ > /<<PKGBUILDDIR>>/src/prop/minisat/utils/System.h\ > /<<PKGBUILDDIR>>/src/prop/prop_engine.cpp\ > /<<PKGBUILDDIR>>/src/prop/prop_engine.h\ > /<<PKGBUILDDIR>>/src/prop/registrar.h\ > /<<PKGBUILDDIR>>/src/prop/sat_solver.h\ > /<<PKGBUILDDIR>>/src/prop/sat_solver_factory.cpp\ > /<<PKGBUILDDIR>>/src/prop/sat_solver_factory.h\ > /<<PKGBUILDDIR>>/src/prop/sat_solver_types.cpp\ > /<<PKGBUILDDIR>>/src/prop/sat_solver_types.h\ > /<<PKGBUILDDIR>>/src/prop/theory_proxy.cpp\ > /<<PKGBUILDDIR>>/src/prop/theory_proxy.h\ > /<<PKGBUILDDIR>>/src/smt/command.cpp\ /<<PKGBUILDDIR>>/src/smt/command.h\ > /<<PKGBUILDDIR>>/src/smt/command_list.cpp\ > /<<PKGBUILDDIR>>/src/smt/command_list.h\ > /<<PKGBUILDDIR>>/src/smt/defined_function.h\ > /<<PKGBUILDDIR>>/src/smt/dump.cpp\ /<<PKGBUILDDIR>>/src/smt/dump.h\ > /<<PKGBUILDDIR>>/src/smt/logic_exception.h\ > /<<PKGBUILDDIR>>/src/smt/logic_request.cpp\ > /<<PKGBUILDDIR>>/src/smt/logic_request.h\ > /<<PKGBUILDDIR>>/src/smt/managed_ostreams.cpp\ > /<<PKGBUILDDIR>>/src/smt/managed_ostreams.h\ > /<<PKGBUILDDIR>>/src/smt/model.cpp\ /<<PKGBUILDDIR>>/src/smt/model.h\ > /<<PKGBUILDDIR>>/src/smt/model_blocker.cpp\ > /<<PKGBUILDDIR>>/src/smt/model_blocker.h\ > /<<PKGBUILDDIR>>/src/smt/model_core_builder.cpp\ > /<<PKGBUILDDIR>>/src/smt/model_core_builder.h\ > /<<PKGBUILDDIR>>/src/smt/process_assertions.cpp\ > /<<PKGBUILDDIR>>/src/smt/process_assertions.h\ > /<<PKGBUILDDIR>>/src/smt/set_defaults.cpp\ > /<<PKGBUILDDIR>>/src/smt/set_defaults.h\ > /<<PKGBUILDDIR>>/src/smt/smt_engine.cpp\ > /<<PKGBUILDDIR>>/src/smt/smt_engine.h\ > /<<PKGBUILDDIR>>/src/smt/smt_engine_scope.cpp\ > /<<PKGBUILDDIR>>/src/smt/smt_engine_scope.h\ > /<<PKGBUILDDIR>>/src/smt/smt_engine_stats.cpp\ > /<<PKGBUILDDIR>>/src/smt/smt_engine_stats.h\ > /<<PKGBUILDDIR>>/src/smt/smt_statistics_registry.cpp\ > /<<PKGBUILDDIR>>/src/smt/smt_statistics_registry.h\ > /<<PKGBUILDDIR>>/src/smt/term_formula_removal.cpp\ > /<<PKGBUILDDIR>>/src/smt/term_formula_removal.h\ > /<<PKGBUILDDIR>>/src/smt/update_ostream.h\ > /<<PKGBUILDDIR>>/src/smt_util/boolean_simplification.cpp\ > /<<PKGBUILDDIR>>/src/smt_util/boolean_simplification.h\ > /<<PKGBUILDDIR>>/src/smt_util/nary_builder.cpp\ > /<<PKGBUILDDIR>>/src/smt_util/nary_builder.h\ > /<<PKGBUILDDIR>>/src/theory/arith/approx_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/approx_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_ite_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_ite_utils.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_msum.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_msum.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_static_learner.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_static_learner.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_utilities.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arith_utilities.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arithvar.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/arithvar.h\ > /<<PKGBUILDDIR>>/src/theory/arith/arithvar_node_map.h\ > /<<PKGBUILDDIR>>/src/theory/arith/attempt_solution_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/attempt_solution_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/bound_counts.h\ > /<<PKGBUILDDIR>>/src/theory/arith/callbacks.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/callbacks.h\ > /<<PKGBUILDDIR>>/src/theory/arith/congruence_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/congruence_manager.h\ > /<<PKGBUILDDIR>>/src/theory/arith/constraint.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/constraint.h\ > /<<PKGBUILDDIR>>/src/theory/arith/constraint_forward.h\ > /<<PKGBUILDDIR>>/src/theory/arith/cut_log.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/cut_log.h\ > /<<PKGBUILDDIR>>/src/theory/arith/delta_rational.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/delta_rational.h\ > /<<PKGBUILDDIR>>/src/theory/arith/dio_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/dio_solver.h\ > /<<PKGBUILDDIR>>/src/theory/arith/dual_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/dual_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/error_set.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/error_set.h\ > /<<PKGBUILDDIR>>/src/theory/arith/fc_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/fc_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/infer_bounds.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/infer_bounds.h\ > /<<PKGBUILDDIR>>/src/theory/arith/linear_equality.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/linear_equality.h\ > /<<PKGBUILDDIR>>/src/theory/arith/matrix.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/matrix.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_constraint.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_constraint.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_lemma_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_lemma_utils.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_model.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_monomial.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_monomial.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nl_solver.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nonlinear_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/nonlinear_extension.h\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/transcendental_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/nl/transcendental_solver.h\ > /<<PKGBUILDDIR>>/src/theory/arith/normal_form.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/normal_form.h\ > /<<PKGBUILDDIR>>/src/theory/arith/partial_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/partial_model.h\ > /<<PKGBUILDDIR>>/src/theory/arith/simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/simplex_update.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/simplex_update.h\ > /<<PKGBUILDDIR>>/src/theory/arith/soi_simplex.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/soi_simplex.h\ > /<<PKGBUILDDIR>>/src/theory/arith/tableau.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/tableau.h\ > /<<PKGBUILDDIR>>/src/theory/arith/tableau_sizes.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/tableau_sizes.h\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith.h\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith_private.cpp\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith_private.h\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith_private_forward.h\ > /<<PKGBUILDDIR>>/src/theory/arith/theory_arith_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/arith/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/array_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/array_info.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/array_proof_reconstruction.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/array_proof_reconstruction.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/static_fact_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/static_fact_manager.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/theory_arrays_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/arrays/union_find.cpp\ > /<<PKGBUILDDIR>>/src/theory/arrays/union_find.h\ > /<<PKGBUILDDIR>>/src/theory/assertion.cpp\ > /<<PKGBUILDDIR>>/src/theory/assertion.h\ > /<<PKGBUILDDIR>>/src/theory/atom_requests.cpp\ > /<<PKGBUILDDIR>>/src/theory/atom_requests.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/circuit_propagator.cpp\ > /<<PKGBUILDDIR>>/src/theory/booleans/circuit_propagator.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/theory/booleans/proof_checker.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool.cpp\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/theory_bool_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/booleans/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/theory/builtin/proof_checker.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin.cpp\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/theory_builtin_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/builtin/type_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/builtin/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/bv/abstraction.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/abstraction.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/aig_bitblaster.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/aig_bitblaster.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/bitblast_strategies_template.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/bitblast_utils.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/bitblaster.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/eager_bitblaster.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/eager_bitblaster.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/lazy_bitblaster.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bitblast/lazy_bitblaster.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_eager_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_eager_solver.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_inequality_graph.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_inequality_graph.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_quick_check.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_quick_check.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_algebraic.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_algebraic.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_bitblast.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_bitblast.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_core.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_core.h\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_inequality.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/bv_subtheory_inequality.h\ > /<<PKGBUILDDIR>>/src/theory/bv/slicer.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/slicer.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_core.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_normalization.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewrite_rules_simplification.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/bv/theory_bv_utils.h\ > /<<PKGBUILDDIR>>/src/theory/bv/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/care_graph.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/datatypes_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/datatypes_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_datatype_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_datatype_utils.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_extension.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_simple_sym.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/sygus_simple_sym.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/theory_datatypes_utils.h\ > /<<PKGBUILDDIR>>/src/theory/datatypes/type_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/datatypes/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/decision_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/decision_manager.h\ > /<<PKGBUILDDIR>>/src/theory/decision_strategy.cpp\ > /<<PKGBUILDDIR>>/src/theory/decision_strategy.h\ > /<<PKGBUILDDIR>>/src/theory/eager_proof_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/eager_proof_generator.h\ > /<<PKGBUILDDIR>>/src/theory/engine_output_channel.cpp\ > /<<PKGBUILDDIR>>/src/theory/engine_output_channel.h\ > /<<PKGBUILDDIR>>/src/theory/evaluator.cpp\ > /<<PKGBUILDDIR>>/src/theory/evaluator.h\ > /<<PKGBUILDDIR>>/src/theory/example/ecdata.cpp\ > /<<PKGBUILDDIR>>/src/theory/example/ecdata.h\ > /<<PKGBUILDDIR>>/src/theory/example/theory_uf_tim.cpp\ > /<<PKGBUILDDIR>>/src/theory/example/theory_uf_tim.h\ > /<<PKGBUILDDIR>>/src/theory/ext_theory.cpp\ > /<<PKGBUILDDIR>>/src/theory/ext_theory.h\ > /<<PKGBUILDDIR>>/src/theory/fp/fp_converter.cpp\ > /<<PKGBUILDDIR>>/src/theory/fp/fp_converter.h\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp.cpp\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp.h\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/fp/theory_fp_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/fp/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/interrupted.h\ > /<<PKGBUILDDIR>>/src/theory/logic_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/logic_info.h\ > /<<PKGBUILDDIR>>/src/theory/output_channel.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/alpha_equivalence.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/alpha_equivalence.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/anti_skolem.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/anti_skolem.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/bv_inverter.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/bv_inverter.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/bv_inverter_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/bv_inverter_utils.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/candidate_rewrite_database.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/candidate_rewrite_database.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/candidate_rewrite_filter.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/candidate_rewrite_filter.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_instantiator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/ceg_instantiator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/vts_term_cache.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/cegqi/vts_term_cache.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/conjecture_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/conjecture_generator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/dynamic_rewrite.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/dynamic_rewrite.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/candidate_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/candidate_generator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/ho_trigger.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/ho_trigger.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/inst_match_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/inst_match_generator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp\ > > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/inst_strategy_e_matching.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/instantiation_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/instantiation_engine.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/trigger.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/ematching/trigger.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/equality_infer.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/equality_infer.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/equality_query.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/equality_query.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/expr_miner.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/expr_miner.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/expr_miner_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/expr_miner_manager.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/extended_rewrite.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/extended_rewrite.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/first_order_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/first_order_model.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/bounded_integers.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/bounded_integers.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/full_model_check.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/full_model_check.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/model_builder.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/model_builder.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/model_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fmf/model_engine.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fun_def_evaluator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fun_def_evaluator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fun_def_process.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/fun_def_process.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_match.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_match.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_match_trie.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_match_trie.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_strategy_enumerative.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/inst_strategy_enumerative.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/instantiate.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/instantiate.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/lazy_trie.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/lazy_trie.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/proof_checker.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_conflict_find.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_conflict_find.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_epr.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_epr.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_relevance.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_relevance.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_rep_bound_ext.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_rep_bound_ext.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_split.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_split.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_util.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quant_util.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quantifiers_attributes.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quantifiers_attributes.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quantifiers_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/quantifiers_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/query_generator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/query_generator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/relevant_domain.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/relevant_domain.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/single_inv_partition.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/single_inv_partition.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/skolemize.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/skolemize.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/solution_filter.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/solution_filter.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/ce_guided_single_inv.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis_core_connective.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis_core_connective.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis_unif.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/cegis_unif.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/enum_stream_substitution.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/enum_stream_substitution.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_eval_cache.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_eval_cache.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_infer.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_infer.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_min_eval.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/example_min_eval.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_abduct.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_abduct.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_enumerator_basic.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_eval_unfold.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_explain.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_explain.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_cons.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_norm.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_red.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_grammar_red.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_invariance.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_invariance.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_module.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_module.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_pbe.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_pbe.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_process_conj.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_process_conj.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_repair_const.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_repair_const.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_stats.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_stats.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_io.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_io.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_rl.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_rl.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_strat.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/sygus_unif_strat.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/synth_conjecture.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/synth_conjecture.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/synth_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/synth_engine.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/term_database_sygus.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/term_database_sygus.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/transition_inference.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/transition_inference.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/type_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/type_info.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/type_node_id_trie.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus/type_node_id_trie.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus_inst.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus_inst.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus_sampler.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/sygus_sampler.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_database.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_database.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_enumeration.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_enumeration.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_util.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/term_util.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/theory_quantifiers.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/theory_quantifiers.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers/theory_quantifiers_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/quantifiers_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/quantifiers_engine.h\ > /<<PKGBUILDDIR>>/src/theory/rep_set.cpp\ > /<<PKGBUILDDIR>>/src/theory/rep_set.h\ > /<<PKGBUILDDIR>>/src/theory/rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/rewriter_attributes.h\ > /<<PKGBUILDDIR>>/src/theory/rewriter_tables_template.h\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep.cpp\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep.h\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/sep/theory_sep_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/sets/cardinality_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/cardinality_extension.h\ > /<<PKGBUILDDIR>>/src/theory/sets/inference_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/inference_manager.h\ > /<<PKGBUILDDIR>>/src/theory/sets/normal_form.h\ > /<<PKGBUILDDIR>>/src/theory/sets/rels_utils.h\ > /<<PKGBUILDDIR>>/src/theory/sets/skolem_cache.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/skolem_cache.h\ > /<<PKGBUILDDIR>>/src/theory/sets/solver_state.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/solver_state.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_private.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_private.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_rels.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_rels.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_type_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/sets/theory_sets_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/shared_terms_database.cpp\ > /<<PKGBUILDDIR>>/src/theory/shared_terms_database.h\ > /<<PKGBUILDDIR>>/src/theory/smt_engine_subsolver.cpp\ > /<<PKGBUILDDIR>>/src/theory/smt_engine_subsolver.h\ > /<<PKGBUILDDIR>>/src/theory/sort_inference.cpp\ > /<<PKGBUILDDIR>>/src/theory/sort_inference.h\ > /<<PKGBUILDDIR>>/src/theory/strings/arith_entail.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/arith_entail.h\ > /<<PKGBUILDDIR>>/src/theory/strings/base_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/base_solver.h\ > /<<PKGBUILDDIR>>/src/theory/strings/core_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/core_solver.h\ > /<<PKGBUILDDIR>>/src/theory/strings/eqc_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/eqc_info.h\ > /<<PKGBUILDDIR>>/src/theory/strings/extf_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/extf_solver.h\ > /<<PKGBUILDDIR>>/src/theory/strings/infer_info.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/infer_info.h\ > /<<PKGBUILDDIR>>/src/theory/strings/inference_manager.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/inference_manager.h\ > /<<PKGBUILDDIR>>/src/theory/strings/normal_form.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/normal_form.h\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_elim.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_elim.h\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_entail.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_entail.h\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_operation.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_operation.h\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_solver.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/regexp_solver.h\ > /<<PKGBUILDDIR>>/src/theory/strings/rewrites.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/rewrites.h\ > /<<PKGBUILDDIR>>/src/theory/strings/sequences_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/sequences_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/strings/sequences_stats.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/sequences_stats.h\ > /<<PKGBUILDDIR>>/src/theory/strings/skolem_cache.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/skolem_cache.h\ > /<<PKGBUILDDIR>>/src/theory/strings/solver_state.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/solver_state.h\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_entail.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_entail.h\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_fmf.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_fmf.h\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_rewriter.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/strings_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/strings/term_registry.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/term_registry.h\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings.h\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_preprocess.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_preprocess.h\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_utils.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/theory_strings_utils.h\ > /<<PKGBUILDDIR>>/src/theory/strings/type_enumerator.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/strings/word.cpp\ > /<<PKGBUILDDIR>>/src/theory/strings/word.h\ > /<<PKGBUILDDIR>>/src/theory/subs_minimize.cpp\ > /<<PKGBUILDDIR>>/src/theory/subs_minimize.h\ > /<<PKGBUILDDIR>>/src/theory/substitutions.cpp\ > /<<PKGBUILDDIR>>/src/theory/substitutions.h\ > /<<PKGBUILDDIR>>/src/theory/term_registration_visitor.cpp\ > /<<PKGBUILDDIR>>/src/theory/term_registration_visitor.h\ > /<<PKGBUILDDIR>>/src/theory/theory.cpp\ /<<PKGBUILDDIR>>/src/theory/theory.h\ > /<<PKGBUILDDIR>>/src/theory/theory_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_engine.h\ > /<<PKGBUILDDIR>>/src/theory/theory_id.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_id.h\ > /<<PKGBUILDDIR>>/src/theory/theory_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_model.h\ > /<<PKGBUILDDIR>>/src/theory/theory_model_builder.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_model_builder.h\ > /<<PKGBUILDDIR>>/src/theory/theory_preprocessor.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_preprocessor.h\ > /<<PKGBUILDDIR>>/src/theory/theory_proof_step_buffer.cpp\ > /<<PKGBUILDDIR>>/src/theory/theory_proof_step_buffer.h\ > /<<PKGBUILDDIR>>/src/theory/theory_registrar.h\ > /<<PKGBUILDDIR>>/src/theory/theory_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/theory_test_utils.h\ > /<<PKGBUILDDIR>>/src/theory/theory_traits_template.h\ > /<<PKGBUILDDIR>>/src/theory/trust_node.cpp\ > /<<PKGBUILDDIR>>/src/theory/trust_node.h\ > /<<PKGBUILDDIR>>/src/theory/type_enumerator.h\ > /<<PKGBUILDDIR>>/src/theory/type_enumerator_template.cpp\ > /<<PKGBUILDDIR>>/src/theory/type_set.cpp\ > /<<PKGBUILDDIR>>/src/theory/type_set.h\ > /<<PKGBUILDDIR>>/src/theory/uf/cardinality_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/cardinality_extension.h\ > /<<PKGBUILDDIR>>/src/theory/uf/equality_engine.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/equality_engine.h\ > /<<PKGBUILDDIR>>/src/theory/uf/equality_engine_types.h\ > /<<PKGBUILDDIR>>/src/theory/uf/ho_extension.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/ho_extension.h\ > /<<PKGBUILDDIR>>/src/theory/uf/proof_checker.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/proof_checker.h\ > /<<PKGBUILDDIR>>/src/theory/uf/symmetry_breaker.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/symmetry_breaker.h\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf.h\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf_model.cpp\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf_model.h\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf_rewriter.h\ > /<<PKGBUILDDIR>>/src/theory/uf/theory_uf_type_rules.h\ > /<<PKGBUILDDIR>>/src/theory/valuation.cpp\ > /<<PKGBUILDDIR>>/src/theory/valuation.h\ > /<<PKGBUILDDIR>>/src/util/abstract_value.cpp\ > /<<PKGBUILDDIR>>/src/util/abstract_value.h\ > /<<PKGBUILDDIR>>/src/util/bin_heap.h\ > /<<PKGBUILDDIR>>/src/util/bitvector.cpp\ > /<<PKGBUILDDIR>>/src/util/bitvector.h\ /<<PKGBUILDDIR>>/src/util/bool.h\ > /<<PKGBUILDDIR>>/src/util/cardinality.cpp\ > /<<PKGBUILDDIR>>/src/util/cardinality.h\ > /<<PKGBUILDDIR>>/src/util/dense_map.h\ > /<<PKGBUILDDIR>>/src/util/divisible.cpp\ > /<<PKGBUILDDIR>>/src/util/divisible.h\ > /<<PKGBUILDDIR>>/src/util/floatingpoint.cpp\ > /<<PKGBUILDDIR>>/src/util/gmp_util.h\ /<<PKGBUILDDIR>>/src/util/hash.h\ > /<<PKGBUILDDIR>>/src/util/index.cpp\ /<<PKGBUILDDIR>>/src/util/index.h\ > /<<PKGBUILDDIR>>/src/util/integer_cln_imp.cpp\ > /<<PKGBUILDDIR>>/src/util/integer_cln_imp.h\ > /<<PKGBUILDDIR>>/src/util/integer_gmp_imp.cpp\ > /<<PKGBUILDDIR>>/src/util/integer_gmp_imp.h\ > /<<PKGBUILDDIR>>/src/util/maybe.h\ > /<<PKGBUILDDIR>>/src/util/ostream_util.cpp\ > /<<PKGBUILDDIR>>/src/util/ostream_util.h\ /<<PKGBUILDDIR>>/src/util/proof.h\ > /<<PKGBUILDDIR>>/src/util/random.cpp\ /<<PKGBUILDDIR>>/src/util/random.h\ > /<<PKGBUILDDIR>>/src/util/rational_cln_imp.cpp\ > /<<PKGBUILDDIR>>/src/util/rational_cln_imp.h\ > /<<PKGBUILDDIR>>/src/util/rational_gmp_imp.cpp\ > /<<PKGBUILDDIR>>/src/util/rational_gmp_imp.h\ > /<<PKGBUILDDIR>>/src/util/regexp.cpp\ /<<PKGBUILDDIR>>/src/util/regexp.h\ > /<<PKGBUILDDIR>>/src/util/resource_manager.cpp\ > /<<PKGBUILDDIR>>/src/util/resource_manager.h\ > /<<PKGBUILDDIR>>/src/util/result.cpp\ /<<PKGBUILDDIR>>/src/util/result.h\ > /<<PKGBUILDDIR>>/src/util/safe_print.cpp\ > /<<PKGBUILDDIR>>/src/util/safe_print.h\ > /<<PKGBUILDDIR>>/src/util/sampler.cpp\ /<<PKGBUILDDIR>>/src/util/sampler.h\ > /<<PKGBUILDDIR>>/src/util/sexpr.cpp\ /<<PKGBUILDDIR>>/src/util/sexpr.h\ > /<<PKGBUILDDIR>>/src/util/smt2_quote_string.cpp\ > /<<PKGBUILDDIR>>/src/util/smt2_quote_string.h\ > /<<PKGBUILDDIR>>/src/util/statistics.cpp\ > /<<PKGBUILDDIR>>/src/util/statistics.h\ > /<<PKGBUILDDIR>>/src/util/statistics_registry.cpp\ > /<<PKGBUILDDIR>>/src/util/statistics_registry.h\ > /<<PKGBUILDDIR>>/src/util/string.cpp\ /<<PKGBUILDDIR>>/src/util/string.h\ > /<<PKGBUILDDIR>>/src/util/tuple.h\ > /<<PKGBUILDDIR>>/src/util/unsafe_interrupt_exception.h\ > /<<PKGBUILDDIR>>/src/util/utility.cpp\ /<<PKGBUILDDIR>>/src/util/utility.h > grep: warning: stray \ before " > grep: warning: stray \ before " > [ 3%] Generating type_properties.h > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr && /usr/bin/cmake -E env > CMAKE_SOURCE_DIR=/<<PKGBUILDDIR>> /<<PKGBUILDDIR>>/src/expr/mkkind > /<<PKGBUILDDIR>>/src/expr/type_properties_template.h > /<<PKGBUILDDIR>>/src/theory/builtin/kinds > /<<PKGBUILDDIR>>/src/theory/booleans/kinds > /<<PKGBUILDDIR>>/src/theory/uf/kinds /<<PKGBUILDDIR>>/src/theory/arith/kinds > /<<PKGBUILDDIR>>/src/theory/bv/kinds /<<PKGBUILDDIR>>/src/theory/fp/kinds > /<<PKGBUILDDIR>>/src/theory/arrays/kinds > /<<PKGBUILDDIR>>/src/theory/datatypes/kinds > /<<PKGBUILDDIR>>/src/theory/sep/kinds /<<PKGBUILDDIR>>/src/theory/sets/kinds > /<<PKGBUILDDIR>>/src/theory/strings/kinds > /<<PKGBUILDDIR>>/src/theory/quantifiers/kinds > > /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr/type_properties.h > [ 3%] Generating Debug_tags > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/base && > /<<PKGBUILDDIR>>/src/base/gentags.sh Debug > [ 3%] Generating Trace_tags > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/base && > /<<PKGBUILDDIR>>/src/base/gentags.sh Trace > [ 3%] Generating Debug_tags.h > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/base && > /<<PKGBUILDDIR>>/src/base/genheader.sh /<<PKGBUILDDIR>>/src/base Debug > [ 4%] Generating Trace_tags.h > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/base && > /<<PKGBUILDDIR>>/src/base/genheader.sh /<<PKGBUILDDIR>>/src/base Trace > make[3]: Leaving directory '/<<PKGBUILDDIR>>/obj-x86_64-linux-gnu' > [ 4%] Built target gen-tags > [ 4%] Generating kind.cpp > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr && /usr/bin/cmake -E env > CMAKE_SOURCE_DIR=/<<PKGBUILDDIR>> /<<PKGBUILDDIR>>/src/expr/mkkind > /<<PKGBUILDDIR>>/src/expr/kind_template.cpp > /<<PKGBUILDDIR>>/src/theory/builtin/kinds > /<<PKGBUILDDIR>>/src/theory/booleans/kinds > /<<PKGBUILDDIR>>/src/theory/uf/kinds /<<PKGBUILDDIR>>/src/theory/arith/kinds > /<<PKGBUILDDIR>>/src/theory/bv/kinds /<<PKGBUILDDIR>>/src/theory/fp/kinds > /<<PKGBUILDDIR>>/src/theory/arrays/kinds > /<<PKGBUILDDIR>>/src/theory/datatypes/kinds > /<<PKGBUILDDIR>>/src/theory/sep/kinds /<<PKGBUILDDIR>>/src/theory/sets/kinds > /<<PKGBUILDDIR>>/src/theory/strings/kinds > /<<PKGBUILDDIR>>/src/theory/quantifiers/kinds > > /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr/kind.cpp > make[3]: Leaving directory '/<<PKGBUILDDIR>>/obj-x86_64-linux-gnu' > [ 4%] Generating expr.h > cd /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr && /usr/bin/cmake -E env > CMAKE_SOURCE_DIR=/<<PKGBUILDDIR>> /<<PKGBUILDDIR>>/src/expr/mkexpr > /<<PKGBUILDDIR>>/src/expr/expr_template.h > /<<PKGBUILDDIR>>/src/theory/builtin/kinds > /<<PKGBUILDDIR>>/src/theory/booleans/kinds > /<<PKGBUILDDIR>>/src/theory/uf/kinds /<<PKGBUILDDIR>>/src/theory/arith/kinds > /<<PKGBUILDDIR>>/src/theory/bv/kinds /<<PKGBUILDDIR>>/src/theory/fp/kinds > /<<PKGBUILDDIR>>/src/theory/arrays/kinds > /<<PKGBUILDDIR>>/src/theory/datatypes/kinds > /<<PKGBUILDDIR>>/src/theory/sep/kinds /<<PKGBUILDDIR>>/src/theory/sets/kinds > /<<PKGBUILDDIR>>/src/theory/strings/kinds > /<<PKGBUILDDIR>>/src/theory/quantifiers/kinds > > /<<PKGBUILDDIR>>/obj-x86_64-linux-gnu/src/expr/expr.h > [ 4%] Built target gen-options > make[3]: Leaving directory '/<<PKGBUILDDIR>>/obj-x86_64-linux-gnu' > [ 4%] Built target gen-theory > /<<PKGBUILDDIR>>/src/expr/expr_template.h:0: error: undefined replacement > ${getConst_instantiations} > make[3]: *** [src/expr/CMakeFiles/gen-expr.dir/build.make:117: > src/expr/expr.h] Error 1 The full build log is available from: http://qa-logs.debian.net/2022/09/17/cvc4_1.8-2_unstable.log All bugs filed during this archive rebuild are listed at: https://bugs.debian.org/cgi-bin/pkgreport.cgi?tag=ftbfs-20220917;users=lu...@debian.org or: https://udd.debian.org/bugs/?release=na&merged=ign&fnewerval=7&flastmodval=7&fusertag=only&fusertagtag=ftbfs-20220917&fusertaguser=lu...@debian.org&allbugs=1&cseverity=1&ctags=1&caffected=1#results A list of current common problems and possible solutions is available at http://wiki.debian.org/qa.debian.org/FTBFS . You're welcome to contribute! If you reassign this bug to another package, please marking it as 'affects'-ing this package. See https://www.debian.org/Bugs/server-control#affects If you fail to reproduce this, please provide a build log and diff it with mine so that we can identify if something relevant changed in the meantime.
--- End Message ---
--- Begin Message ---Source: cvc4 Source-Version: 1.8-3 Done: Scott Talbert <s...@techie.net> We believe that the bug you reported is fixed in the latest version of cvc4, which is due to be installed in the Debian FTP archive. A summary of the changes between this version and the previous one is attached. Thank you for reporting the bug, which will now be closed. If you have further comments please address them to 1020...@bugs.debian.org, and the maintainer will reopen the bug report if appropriate. Debian distribution maintenance software pp. Scott Talbert <s...@techie.net> (supplier of updated cvc4 package) (This message was generated automatically at their request; if you believe that there is a problem with it please contact the archive administrators by mailing ftpmas...@ftp-master.debian.org) -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 Format: 1.8 Date: Sat, 29 Oct 2022 14:49:40 -0400 Source: cvc4 Architecture: source Version: 1.8-3 Distribution: unstable Urgency: medium Maintainer: Debian Science Maintainers <debian-science-maintainers@alioth-lists.debian.net> Changed-By: Scott Talbert <s...@techie.net> Closes: 1020010 Changes: cvc4 (1.8-3) unstable; urgency=medium . * Team upload. * Fix FTBFS with bash 5.2 (Closes: #1020010) * Fix FTBFS due to cryptominisat API changes by disabling cryptominisat Checksums-Sha1: 3cc23445e891a081c5988a03763fc5a8bdb3877d 2244 cvc4_1.8-3.dsc 65d5a6a58c48952a5ab85d237fd97f3668debe61 16728 cvc4_1.8-3.debian.tar.xz 8f8d60cf5eb070df026fe08c7febf31bf846edf8 10669 cvc4_1.8-3_amd64.buildinfo Checksums-Sha256: 9eff67686af16ae138139c72d985ba2055f8b9f7499e72227084c05d205a8e5e 2244 cvc4_1.8-3.dsc 2352cb3bcf46a49d70fd3f5d46664a85810ed2f17fa12b6038e387ba34a426e2 16728 cvc4_1.8-3.debian.tar.xz 296c7d6381d121ebcd95877df433563cbe961ed96850ab164a914d80940f8b10 10669 cvc4_1.8-3_amd64.buildinfo Files: 8de14465c33e6e26fd27411178b9d47a 2244 math optional cvc4_1.8-3.dsc 046098e2ea74c89f4bda2efad82b4af2 16728 math optional cvc4_1.8-3.debian.tar.xz 084ffc94a537e59d992bfe495ee68004 10669 math optional cvc4_1.8-3_amd64.buildinfo -----BEGIN PGP SIGNATURE----- iQJDBAEBCgAtFiEEbnQ09Yl9Q7F/zVe3U9W8ZLUjeKIFAmNdgvQPHHN3dEB0ZWNo aWUubmV0AAoJEFPVvGS1I3iichcP/i8ZmV5rmjyQjRxMSPZZRSPr42+aOuzQyXvi Uuq1ek9UNiE+SZg7FkhdkgcVZm/2FOM89yDBcEffIpqB/f9uRXpwm/AJBSSDAQy9 pSmpV0ROn/EzdmLOI5JLJNzdA2ig6v+HRG5tP/8LxSpqqoGzP1WAKR7I/2g4wlT3 fkEDPI63gRKuordHKQYLxJdxMQA8cY0kckEP/us0VUS4ie6skbU4lqmYR9cmbwG4 G/k0GAIG9jTqmOgt0+QgVKsyHWIk4xk3mt/aNm4YJlsyXlxue7M9w3DPHzf6mwVF ClSvfD9ZcAQV/Prw63dEK3Xhgr5pZxpvX6pL0O/UFf2h6q1itc0aWKrG3mvOPLUF mjY3FF0HMd7s2S5iWziw1D9aVaFWtd5VdegeaqhfIn6Ltb+/sRXhsFHFZc5yJe3n 1cixWp20g5LOWO0wemXVpfp+mAEd+ZTd2/7bUy+MmkIXwUcEV66EgtMIpMWg43Ua D8AsObMtJR1SSuiVi3YDzJ9FqwlOyRG5LeB99xzv+kaHT3WJyLfi3TicKG0astpn xPjF8zFSD64GL8xTiE/brPO7L4eLMxSnrOKG2zRONsGTiv2DOgxPCYkByxC8k1J2 SJvFTrPGdCzJ2tyuSvk48LDN7Lw9JxJw6XNFSMO7I8OJudMJDFThFVx2xojf1aan QezYMiUE =UMqr -----END PGP SIGNATURE-----
--- End Message ---
-- debian-science-maintainers mailing list debian-science-maintainers@alioth-lists.debian.net https://alioth-lists.debian.net/cgi-bin/mailman/listinfo/debian-science-maintainers
