Flawfinder version 2.0.10, (C) 2001-2019 David A. Wheeler.
Number of rules (primarily dangerous function names) in C/C++ ruleset: 223
Examining data/z3-4.8.9/cmake/target_arch_detect.cpp
Examining data/z3-4.8.9/contrib/qprofdiff/main.cpp
Examining data/z3-4.8.9/examples/c++/example.cpp
Examining data/z3-4.8.9/examples/c/test_capi.c
Examining data/z3-4.8.9/examples/maxsat/maxsat.c
Examining data/z3-4.8.9/examples/tptp/tptp5.cpp
Examining data/z3-4.8.9/examples/tptp/tptp5.h
Examining data/z3-4.8.9/examples/tptp/tptp5.lex.cpp
Examining data/z3-4.8.9/examples/tptp/tptp5.tab.c
Examining data/z3-4.8.9/examples/tptp/tptp5.tab.h
Examining data/z3-4.8.9/src/ackermannization/ackermannize_bv_model_converter.cpp
Examining data/z3-4.8.9/src/ackermannization/ackermannize_bv_model_converter.h
Examining data/z3-4.8.9/src/ackermannization/ackermannize_bv_tactic.cpp
Examining data/z3-4.8.9/src/ackermannization/ackermannize_bv_tactic.h
Examining data/z3-4.8.9/src/ackermannization/ackr_bound_probe.cpp
Examining data/z3-4.8.9/src/ackermannization/ackr_bound_probe.h
Examining data/z3-4.8.9/src/ackermannization/ackr_helper.cpp
Examining data/z3-4.8.9/src/ackermannization/ackr_helper.h
Examining data/z3-4.8.9/src/ackermannization/ackr_info.h
Examining data/z3-4.8.9/src/ackermannization/ackr_model_converter.cpp
Examining data/z3-4.8.9/src/ackermannization/ackr_model_converter.h
Examining data/z3-4.8.9/src/ackermannization/lackr.cpp
Examining data/z3-4.8.9/src/ackermannization/lackr.h
Examining data/z3-4.8.9/src/ackermannization/lackr_model_constructor.cpp
Examining data/z3-4.8.9/src/ackermannization/lackr_model_constructor.h
Examining data/z3-4.8.9/src/ackermannization/lackr_model_converter_lazy.cpp
Examining data/z3-4.8.9/src/ackermannization/lackr_model_converter_lazy.h
Examining data/z3-4.8.9/src/api/api_algebraic.cpp
Examining data/z3-4.8.9/src/api/api_arith.cpp
Examining data/z3-4.8.9/src/api/api_array.cpp
Examining data/z3-4.8.9/src/api/api_ast.cpp
Examining data/z3-4.8.9/src/api/api_ast_map.cpp
Examining data/z3-4.8.9/src/api/api_ast_map.h
Examining data/z3-4.8.9/src/api/api_ast_vector.cpp
Examining data/z3-4.8.9/src/api/api_ast_vector.h
Examining data/z3-4.8.9/src/api/api_bv.cpp
Examining data/z3-4.8.9/src/api/api_config_params.cpp
Examining data/z3-4.8.9/src/api/api_context.cpp
Examining data/z3-4.8.9/src/api/api_context.h
Examining data/z3-4.8.9/src/api/api_datalog.cpp
Examining data/z3-4.8.9/src/api/api_datalog.h
Examining data/z3-4.8.9/src/api/api_datatype.cpp
Examining data/z3-4.8.9/src/api/api_fpa.cpp
Examining data/z3-4.8.9/src/api/api_goal.cpp
Examining data/z3-4.8.9/src/api/api_goal.h
Examining data/z3-4.8.9/src/api/api_log.cpp
Examining data/z3-4.8.9/src/api/api_model.cpp
Examining data/z3-4.8.9/src/api/api_model.h
Examining data/z3-4.8.9/src/api/api_numeral.cpp
Examining data/z3-4.8.9/src/api/api_opt.cpp
Examining data/z3-4.8.9/src/api/api_params.cpp
Examining data/z3-4.8.9/src/api/api_parsers.cpp
Examining data/z3-4.8.9/src/api/api_pb.cpp
Examining data/z3-4.8.9/src/api/api_polynomial.cpp
Examining data/z3-4.8.9/src/api/api_polynomial.h
Examining data/z3-4.8.9/src/api/api_qe.cpp
Examining data/z3-4.8.9/src/api/api_quant.cpp
Examining data/z3-4.8.9/src/api/api_rcf.cpp
Examining data/z3-4.8.9/src/api/api_seq.cpp
Examining data/z3-4.8.9/src/api/api_solver.cpp
Examining data/z3-4.8.9/src/api/api_solver.h
Examining data/z3-4.8.9/src/api/api_special_relations.cpp
Examining data/z3-4.8.9/src/api/api_stats.cpp
Examining data/z3-4.8.9/src/api/api_stats.h
Examining data/z3-4.8.9/src/api/api_tactic.cpp
Examining data/z3-4.8.9/src/api/api_tactic.h
Examining data/z3-4.8.9/src/api/api_util.h
Examining data/z3-4.8.9/src/api/c++/z3++.h
Examining data/z3-4.8.9/src/api/dll/dll.cpp
Examining data/z3-4.8.9/src/api/julia/z3jl.cpp
Examining data/z3-4.8.9/src/api/ml/z3native_stubs.h
Examining data/z3-4.8.9/src/api/z3.h
Examining data/z3-4.8.9/src/api/z3_algebraic.h
Examining data/z3-4.8.9/src/api/z3_api.h
Examining data/z3-4.8.9/src/api/z3_ast_containers.h
Examining data/z3-4.8.9/src/api/z3_fixedpoint.h
Examining data/z3-4.8.9/src/api/z3_fpa.h
Examining data/z3-4.8.9/src/api/z3_logger.h
Examining data/z3-4.8.9/src/api/z3_macros.h
Examining data/z3-4.8.9/src/api/z3_optimization.h
Examining data/z3-4.8.9/src/api/z3_polynomial.h
Examining data/z3-4.8.9/src/api/z3_private.h
Examining data/z3-4.8.9/src/api/z3_rcf.h
Examining data/z3-4.8.9/src/api/z3_replayer.cpp
Examining data/z3-4.8.9/src/api/z3_replayer.h
Examining data/z3-4.8.9/src/api/z3_spacer.h
Examining data/z3-4.8.9/src/api/z3_v1.h
Examining data/z3-4.8.9/src/ast/act_cache.cpp
Examining data/z3-4.8.9/src/ast/act_cache.h
Examining data/z3-4.8.9/src/ast/arith_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/arith_decl_plugin.h
Examining data/z3-4.8.9/src/ast/array_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/array_decl_plugin.h
Examining data/z3-4.8.9/src/ast/ast.cpp
Examining data/z3-4.8.9/src/ast/ast.h
Examining data/z3-4.8.9/src/ast/ast_ll_pp.cpp
Examining data/z3-4.8.9/src/ast/ast_ll_pp.h
Examining data/z3-4.8.9/src/ast/ast_lt.cpp
Examining data/z3-4.8.9/src/ast/ast_lt.h
Examining data/z3-4.8.9/src/ast/ast_pp.h
Examining data/z3-4.8.9/src/ast/ast_pp_dot.cpp
Examining data/z3-4.8.9/src/ast/ast_pp_dot.h
Examining data/z3-4.8.9/src/ast/ast_pp_util.cpp
Examining data/z3-4.8.9/src/ast/ast_pp_util.h
Examining data/z3-4.8.9/src/ast/ast_printer.cpp
Examining data/z3-4.8.9/src/ast/ast_printer.h
Examining data/z3-4.8.9/src/ast/ast_smt2_pp.cpp
Examining data/z3-4.8.9/src/ast/ast_smt2_pp.h
Examining data/z3-4.8.9/src/ast/ast_smt_pp.cpp
Examining data/z3-4.8.9/src/ast/ast_smt_pp.h
Examining data/z3-4.8.9/src/ast/ast_trail.h
Examining data/z3-4.8.9/src/ast/ast_translation.cpp
Examining data/z3-4.8.9/src/ast/ast_translation.h
Examining data/z3-4.8.9/src/ast/ast_util.cpp
Examining data/z3-4.8.9/src/ast/ast_util.h
Examining data/z3-4.8.9/src/ast/bv_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/bv_decl_plugin.h
Examining data/z3-4.8.9/src/ast/datatype_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/datatype_decl_plugin.h
Examining data/z3-4.8.9/src/ast/decl_collector.cpp
Examining data/z3-4.8.9/src/ast/decl_collector.h
Examining data/z3-4.8.9/src/ast/display_dimacs.cpp
Examining data/z3-4.8.9/src/ast/display_dimacs.h
Examining data/z3-4.8.9/src/ast/dl_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/dl_decl_plugin.h
Examining data/z3-4.8.9/src/ast/euf/euf_egraph.cpp
Examining data/z3-4.8.9/src/ast/euf/euf_egraph.h
Examining data/z3-4.8.9/src/ast/euf/euf_enode.cpp
Examining data/z3-4.8.9/src/ast/euf/euf_enode.h
Examining data/z3-4.8.9/src/ast/euf/euf_etable.cpp
Examining data/z3-4.8.9/src/ast/euf/euf_etable.h
Examining data/z3-4.8.9/src/ast/euf/euf_justification.h
Examining data/z3-4.8.9/src/ast/expr2polynomial.cpp
Examining data/z3-4.8.9/src/ast/expr2polynomial.h
Examining data/z3-4.8.9/src/ast/expr2var.cpp
Examining data/z3-4.8.9/src/ast/expr2var.h
Examining data/z3-4.8.9/src/ast/expr_abstract.cpp
Examining data/z3-4.8.9/src/ast/expr_abstract.h
Examining data/z3-4.8.9/src/ast/expr_delta_pair.h
Examining data/z3-4.8.9/src/ast/expr_functors.cpp
Examining data/z3-4.8.9/src/ast/expr_functors.h
Examining data/z3-4.8.9/src/ast/expr_map.cpp
Examining data/z3-4.8.9/src/ast/expr_map.h
Examining data/z3-4.8.9/src/ast/expr_stat.cpp
Examining data/z3-4.8.9/src/ast/expr_stat.h
Examining data/z3-4.8.9/src/ast/expr_substitution.cpp
Examining data/z3-4.8.9/src/ast/expr_substitution.h
Examining data/z3-4.8.9/src/ast/for_each_ast.cpp
Examining data/z3-4.8.9/src/ast/for_each_ast.h
Examining data/z3-4.8.9/src/ast/for_each_expr.cpp
Examining data/z3-4.8.9/src/ast/for_each_expr.h
Examining data/z3-4.8.9/src/ast/format.cpp
Examining data/z3-4.8.9/src/ast/format.h
Examining data/z3-4.8.9/src/ast/fpa/bv2fpa_converter.cpp
Examining data/z3-4.8.9/src/ast/fpa/bv2fpa_converter.h
Examining data/z3-4.8.9/src/ast/fpa/fpa2bv_converter.cpp
Examining data/z3-4.8.9/src/ast/fpa/fpa2bv_converter.h
Examining data/z3-4.8.9/src/ast/fpa/fpa2bv_rewriter.cpp
Examining data/z3-4.8.9/src/ast/fpa/fpa2bv_rewriter.h
Examining data/z3-4.8.9/src/ast/fpa_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/fpa_decl_plugin.h
Examining data/z3-4.8.9/src/ast/func_decl_dependencies.cpp
Examining data/z3-4.8.9/src/ast/func_decl_dependencies.h
Examining data/z3-4.8.9/src/ast/has_free_vars.cpp
Examining data/z3-4.8.9/src/ast/has_free_vars.h
Examining data/z3-4.8.9/src/ast/justified_expr.h
Examining data/z3-4.8.9/src/ast/macro_substitution.cpp
Examining data/z3-4.8.9/src/ast/macro_substitution.h
Examining data/z3-4.8.9/src/ast/macros/macro_finder.cpp
Examining data/z3-4.8.9/src/ast/macros/macro_finder.h
Examining data/z3-4.8.9/src/ast/macros/macro_manager.cpp
Examining data/z3-4.8.9/src/ast/macros/macro_manager.h
Examining data/z3-4.8.9/src/ast/macros/macro_util.cpp
Examining data/z3-4.8.9/src/ast/macros/macro_util.h
Examining data/z3-4.8.9/src/ast/macros/quasi_macros.cpp
Examining data/z3-4.8.9/src/ast/macros/quasi_macros.h
Examining data/z3-4.8.9/src/ast/normal_forms/defined_names.cpp
Examining data/z3-4.8.9/src/ast/normal_forms/defined_names.h
Examining data/z3-4.8.9/src/ast/normal_forms/name_exprs.cpp
Examining data/z3-4.8.9/src/ast/normal_forms/name_exprs.h
Examining data/z3-4.8.9/src/ast/normal_forms/nnf.cpp
Examining data/z3-4.8.9/src/ast/normal_forms/nnf.h
Examining data/z3-4.8.9/src/ast/normal_forms/pull_quant.cpp
Examining data/z3-4.8.9/src/ast/normal_forms/pull_quant.h
Examining data/z3-4.8.9/src/ast/num_occurs.cpp
Examining data/z3-4.8.9/src/ast/num_occurs.h
Examining data/z3-4.8.9/src/ast/occurs.cpp
Examining data/z3-4.8.9/src/ast/occurs.h
Examining data/z3-4.8.9/src/ast/pattern/expr_pattern_match.cpp
Examining data/z3-4.8.9/src/ast/pattern/expr_pattern_match.h
Examining data/z3-4.8.9/src/ast/pattern/pattern_inference.cpp
Examining data/z3-4.8.9/src/ast/pattern/pattern_inference.h
Examining data/z3-4.8.9/src/ast/pb_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/pb_decl_plugin.h
Examining data/z3-4.8.9/src/ast/pp.cpp
Examining data/z3-4.8.9/src/ast/pp.h
Examining data/z3-4.8.9/src/ast/proofs/proof_checker.cpp
Examining data/z3-4.8.9/src/ast/proofs/proof_checker.h
Examining data/z3-4.8.9/src/ast/proofs/proof_utils.cpp
Examining data/z3-4.8.9/src/ast/proofs/proof_utils.h
Examining data/z3-4.8.9/src/ast/recfun_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/recfun_decl_plugin.h
Examining data/z3-4.8.9/src/ast/recurse_expr.h
Examining data/z3-4.8.9/src/ast/recurse_expr_def.h
Examining data/z3-4.8.9/src/ast/reg_decl_plugins.cpp
Examining data/z3-4.8.9/src/ast/reg_decl_plugins.h
Examining data/z3-4.8.9/src/ast/rewriter/arith_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/arith_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/array_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/array_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/ast_counter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/ast_counter.h
Examining data/z3-4.8.9/src/ast/rewriter/bit2int.cpp
Examining data/z3-4.8.9/src/ast/rewriter/bit2int.h
Examining data/z3-4.8.9/src/ast/rewriter/bit_blaster/bit_blaster.cpp
Examining data/z3-4.8.9/src/ast/rewriter/bit_blaster/bit_blaster.h
Examining data/z3-4.8.9/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h
Examining data/z3-4.8.9/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
Examining data/z3-4.8.9/src/ast/rewriter/bool_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/bool_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/bv_bounds.cpp
Examining data/z3-4.8.9/src/ast/rewriter/bv_bounds.h
Examining data/z3-4.8.9/src/ast/rewriter/bv_elim.cpp
Examining data/z3-4.8.9/src/ast/rewriter/bv_elim.h
Examining data/z3-4.8.9/src/ast/rewriter/bv_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/bv_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/datatype_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/datatype_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/der.cpp
Examining data/z3-4.8.9/src/ast/rewriter/der.h
Examining data/z3-4.8.9/src/ast/rewriter/distribute_forall.cpp
Examining data/z3-4.8.9/src/ast/rewriter/distribute_forall.h
Examining data/z3-4.8.9/src/ast/rewriter/dl_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/dl_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/elim_bounds.cpp
Examining data/z3-4.8.9/src/ast/rewriter/elim_bounds.h
Examining data/z3-4.8.9/src/ast/rewriter/enum2bv_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/enum2bv_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/expr_replacer.cpp
Examining data/z3-4.8.9/src/ast/rewriter/expr_replacer.h
Examining data/z3-4.8.9/src/ast/rewriter/expr_safe_replace.cpp
Examining data/z3-4.8.9/src/ast/rewriter/expr_safe_replace.h
Examining data/z3-4.8.9/src/ast/rewriter/factor_equivs.cpp
Examining data/z3-4.8.9/src/ast/rewriter/factor_equivs.h
Examining data/z3-4.8.9/src/ast/rewriter/factor_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/factor_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/fpa_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/fpa_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/func_decl_replace.cpp
Examining data/z3-4.8.9/src/ast/rewriter/func_decl_replace.h
Examining data/z3-4.8.9/src/ast/rewriter/hoist_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/hoist_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/inj_axiom.cpp
Examining data/z3-4.8.9/src/ast/rewriter/inj_axiom.h
Examining data/z3-4.8.9/src/ast/rewriter/label_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/label_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/maximize_ac_sharing.cpp
Examining data/z3-4.8.9/src/ast/rewriter/maximize_ac_sharing.h
Examining data/z3-4.8.9/src/ast/rewriter/mk_extract_proc.cpp
Examining data/z3-4.8.9/src/ast/rewriter/mk_extract_proc.h
Examining data/z3-4.8.9/src/ast/rewriter/mk_simplified_app.cpp
Examining data/z3-4.8.9/src/ast/rewriter/mk_simplified_app.h
Examining data/z3-4.8.9/src/ast/rewriter/pb2bv_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/pb2bv_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/pb_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/pb_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/pb_rewriter_def.h
Examining data/z3-4.8.9/src/ast/rewriter/poly_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/poly_rewriter_def.h
Examining data/z3-4.8.9/src/ast/rewriter/push_app_ite.cpp
Examining data/z3-4.8.9/src/ast/rewriter/push_app_ite.h
Examining data/z3-4.8.9/src/ast/rewriter/quant_hoist.cpp
Examining data/z3-4.8.9/src/ast/rewriter/quant_hoist.h
Examining data/z3-4.8.9/src/ast/rewriter/recfun_replace.h
Examining data/z3-4.8.9/src/ast/rewriter/recfun_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/recfun_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/rewriter_def.h
Examining data/z3-4.8.9/src/ast/rewriter/rewriter_types.h
Examining data/z3-4.8.9/src/ast/rewriter/seq_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/seq_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/th_rewriter.cpp
Examining data/z3-4.8.9/src/ast/rewriter/th_rewriter.h
Examining data/z3-4.8.9/src/ast/rewriter/value_sweep.cpp
Examining data/z3-4.8.9/src/ast/rewriter/value_sweep.h
Examining data/z3-4.8.9/src/ast/rewriter/var_subst.cpp
Examining data/z3-4.8.9/src/ast/rewriter/var_subst.h
Examining data/z3-4.8.9/src/ast/scoped_proof.h
Examining data/z3-4.8.9/src/ast/seq_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/seq_decl_plugin.h
Examining data/z3-4.8.9/src/ast/shared_occs.cpp
Examining data/z3-4.8.9/src/ast/shared_occs.h
Examining data/z3-4.8.9/src/ast/special_relations_decl_plugin.cpp
Examining data/z3-4.8.9/src/ast/special_relations_decl_plugin.h
Examining data/z3-4.8.9/src/ast/static_features.cpp
Examining data/z3-4.8.9/src/ast/static_features.h
Examining data/z3-4.8.9/src/ast/substitution/expr_offset.h
Examining data/z3-4.8.9/src/ast/substitution/expr_offset_map.h
Examining data/z3-4.8.9/src/ast/substitution/matcher.cpp
Examining data/z3-4.8.9/src/ast/substitution/matcher.h
Examining data/z3-4.8.9/src/ast/substitution/substitution.cpp
Examining data/z3-4.8.9/src/ast/substitution/substitution.h
Examining data/z3-4.8.9/src/ast/substitution/substitution_tree.cpp
Examining data/z3-4.8.9/src/ast/substitution/substitution_tree.h
Examining data/z3-4.8.9/src/ast/substitution/unifier.cpp
Examining data/z3-4.8.9/src/ast/substitution/unifier.h
Examining data/z3-4.8.9/src/ast/substitution/var_offset_map.h
Examining data/z3-4.8.9/src/ast/used_symbols.h
Examining data/z3-4.8.9/src/ast/used_vars.cpp
Examining data/z3-4.8.9/src/ast/used_vars.h
Examining data/z3-4.8.9/src/ast/value_generator.cpp
Examining data/z3-4.8.9/src/ast/value_generator.h
Examining data/z3-4.8.9/src/ast/well_sorted.cpp
Examining data/z3-4.8.9/src/ast/well_sorted.h
Examining data/z3-4.8.9/src/cmd_context/basic_cmds.cpp
Examining data/z3-4.8.9/src/cmd_context/basic_cmds.h
Examining data/z3-4.8.9/src/cmd_context/check_logic.cpp
Examining data/z3-4.8.9/src/cmd_context/check_logic.h
Examining data/z3-4.8.9/src/cmd_context/cmd_context.cpp
Examining data/z3-4.8.9/src/cmd_context/cmd_context.h
Examining data/z3-4.8.9/src/cmd_context/cmd_context_to_goal.cpp
Examining data/z3-4.8.9/src/cmd_context/cmd_context_to_goal.h
Examining data/z3-4.8.9/src/cmd_context/cmd_util.cpp
Examining data/z3-4.8.9/src/cmd_context/cmd_util.h
Examining data/z3-4.8.9/src/cmd_context/echo_tactic.cpp
Examining data/z3-4.8.9/src/cmd_context/echo_tactic.h
Examining data/z3-4.8.9/src/cmd_context/eval_cmd.cpp
Examining data/z3-4.8.9/src/cmd_context/eval_cmd.h
Examining data/z3-4.8.9/src/cmd_context/extra_cmds/dbg_cmds.cpp
Examining data/z3-4.8.9/src/cmd_context/extra_cmds/dbg_cmds.h
Examining data/z3-4.8.9/src/cmd_context/extra_cmds/polynomial_cmds.cpp
Examining data/z3-4.8.9/src/cmd_context/extra_cmds/polynomial_cmds.h
Examining data/z3-4.8.9/src/cmd_context/extra_cmds/subpaving_cmds.cpp
Examining data/z3-4.8.9/src/cmd_context/extra_cmds/subpaving_cmds.h
Examining data/z3-4.8.9/src/cmd_context/parametric_cmd.cpp
Examining data/z3-4.8.9/src/cmd_context/parametric_cmd.h
Examining data/z3-4.8.9/src/cmd_context/pdecl.cpp
Examining data/z3-4.8.9/src/cmd_context/pdecl.h
Examining data/z3-4.8.9/src/cmd_context/simplify_cmd.cpp
Examining data/z3-4.8.9/src/cmd_context/simplify_cmd.h
Examining data/z3-4.8.9/src/cmd_context/tactic_cmds.cpp
Examining data/z3-4.8.9/src/cmd_context/tactic_cmds.h
Examining data/z3-4.8.9/src/cmd_context/tactic_manager.cpp
Examining data/z3-4.8.9/src/cmd_context/tactic_manager.h
Examining data/z3-4.8.9/src/math/automata/automaton.cpp
Examining data/z3-4.8.9/src/math/automata/automaton.h
Examining data/z3-4.8.9/src/math/automata/boolean_algebra.h
Examining data/z3-4.8.9/src/math/automata/symbolic_automata.h
Examining data/z3-4.8.9/src/math/automata/symbolic_automata_def.h
Examining data/z3-4.8.9/src/math/dd/dd_bdd.cpp
Examining data/z3-4.8.9/src/math/dd/dd_bdd.h
Examining data/z3-4.8.9/src/math/dd/dd_pdd.cpp
Examining data/z3-4.8.9/src/math/dd/dd_pdd.h
Examining data/z3-4.8.9/src/math/dd/pdd_eval.h
Examining data/z3-4.8.9/src/math/dd/pdd_interval.h
Examining data/z3-4.8.9/src/math/grobner/grobner.cpp
Examining data/z3-4.8.9/src/math/grobner/grobner.h
Examining data/z3-4.8.9/src/math/grobner/pdd_simplifier.cpp
Examining data/z3-4.8.9/src/math/grobner/pdd_simplifier.h
Examining data/z3-4.8.9/src/math/grobner/pdd_solver.cpp
Examining data/z3-4.8.9/src/math/grobner/pdd_solver.h
Examining data/z3-4.8.9/src/math/hilbert/heap_trie.h
Examining data/z3-4.8.9/src/math/hilbert/hilbert_basis.cpp
Examining data/z3-4.8.9/src/math/hilbert/hilbert_basis.h
Examining data/z3-4.8.9/src/math/interval/dep_intervals.cpp
Examining data/z3-4.8.9/src/math/interval/dep_intervals.h
Examining data/z3-4.8.9/src/math/interval/interval.h
Examining data/z3-4.8.9/src/math/interval/interval_def.h
Examining data/z3-4.8.9/src/math/interval/interval_mpq.cpp
Examining data/z3-4.8.9/src/math/lp/binary_heap_priority_queue.cpp
Examining data/z3-4.8.9/src/math/lp/binary_heap_priority_queue.h
Examining data/z3-4.8.9/src/math/lp/binary_heap_priority_queue_def.h
Examining data/z3-4.8.9/src/math/lp/binary_heap_upair_queue.cpp
Examining data/z3-4.8.9/src/math/lp/binary_heap_upair_queue.h
Examining data/z3-4.8.9/src/math/lp/binary_heap_upair_queue_def.h
Examining data/z3-4.8.9/src/math/lp/bound_analyzer_on_row.h
Examining data/z3-4.8.9/src/math/lp/breakpoint.h
Examining data/z3-4.8.9/src/math/lp/column_info.h
Examining data/z3-4.8.9/src/math/lp/column_namer.h
Examining data/z3-4.8.9/src/math/lp/conversion_helper.h
Examining data/z3-4.8.9/src/math/lp/core_solver_pretty_printer.cpp
Examining data/z3-4.8.9/src/math/lp/core_solver_pretty_printer.h
Examining data/z3-4.8.9/src/math/lp/core_solver_pretty_printer_def.h
Examining data/z3-4.8.9/src/math/lp/cross_nested.h
Examining data/z3-4.8.9/src/math/lp/dense_matrix.cpp
Examining data/z3-4.8.9/src/math/lp/dense_matrix.h
Examining data/z3-4.8.9/src/math/lp/dense_matrix_def.h
Examining data/z3-4.8.9/src/math/lp/emonics.cpp
Examining data/z3-4.8.9/src/math/lp/emonics.h
Examining data/z3-4.8.9/src/math/lp/eta_matrix.cpp
Examining data/z3-4.8.9/src/math/lp/eta_matrix.h
Examining data/z3-4.8.9/src/math/lp/eta_matrix_def.h
Examining data/z3-4.8.9/src/math/lp/explanation.h
Examining data/z3-4.8.9/src/math/lp/factorization.cpp
Examining data/z3-4.8.9/src/math/lp/factorization.h
Examining data/z3-4.8.9/src/math/lp/factorization_factory_imp.cpp
Examining data/z3-4.8.9/src/math/lp/factorization_factory_imp.h
Examining data/z3-4.8.9/src/math/lp/general_matrix.h
Examining data/z3-4.8.9/src/math/lp/gomory.cpp
Examining data/z3-4.8.9/src/math/lp/gomory.h
Examining data/z3-4.8.9/src/math/lp/hnf.h
Examining data/z3-4.8.9/src/math/lp/hnf_cutter.cpp
Examining data/z3-4.8.9/src/math/lp/hnf_cutter.h
Examining data/z3-4.8.9/src/math/lp/horner.cpp
Examining data/z3-4.8.9/src/math/lp/horner.h
Examining data/z3-4.8.9/src/math/lp/implied_bound.h
Examining data/z3-4.8.9/src/math/lp/incremental_vector.h
Examining data/z3-4.8.9/src/math/lp/indexed_value.h
Examining data/z3-4.8.9/src/math/lp/indexed_vector.cpp
Examining data/z3-4.8.9/src/math/lp/indexed_vector.h
Examining data/z3-4.8.9/src/math/lp/indexed_vector_def.h
Examining data/z3-4.8.9/src/math/lp/indexer_of_constraints.h
Examining data/z3-4.8.9/src/math/lp/int_branch.cpp
Examining data/z3-4.8.9/src/math/lp/int_branch.h
Examining data/z3-4.8.9/src/math/lp/int_cube.cpp
Examining data/z3-4.8.9/src/math/lp/int_cube.h
Examining data/z3-4.8.9/src/math/lp/int_gcd_test.cpp
Examining data/z3-4.8.9/src/math/lp/int_gcd_test.h
Examining data/z3-4.8.9/src/math/lp/int_solver.cpp
Examining data/z3-4.8.9/src/math/lp/int_solver.h
Examining data/z3-4.8.9/src/math/lp/lar_constraints.h
Examining data/z3-4.8.9/src/math/lp/lar_core_solver.cpp
Examining data/z3-4.8.9/src/math/lp/lar_core_solver.h
Examining data/z3-4.8.9/src/math/lp/lar_core_solver_def.h
Examining data/z3-4.8.9/src/math/lp/lar_solution_signature.h
Examining data/z3-4.8.9/src/math/lp/lar_solver.cpp
Examining data/z3-4.8.9/src/math/lp/lar_solver.h
Examining data/z3-4.8.9/src/math/lp/lar_term.h
Examining data/z3-4.8.9/src/math/lp/lia_move.h
Examining data/z3-4.8.9/src/math/lp/lp_bound_propagator.h
Examining data/z3-4.8.9/src/math/lp/lp_core_solver_base.cpp
Examining data/z3-4.8.9/src/math/lp/lp_core_solver_base.h
Examining data/z3-4.8.9/src/math/lp/lp_core_solver_base_def.h
Examining data/z3-4.8.9/src/math/lp/lp_dual_core_solver.cpp
Examining data/z3-4.8.9/src/math/lp/lp_dual_core_solver.h
Examining data/z3-4.8.9/src/math/lp/lp_dual_core_solver_def.h
Examining data/z3-4.8.9/src/math/lp/lp_dual_simplex.cpp
Examining data/z3-4.8.9/src/math/lp/lp_dual_simplex.h
Examining data/z3-4.8.9/src/math/lp/lp_dual_simplex_def.h
Examining data/z3-4.8.9/src/math/lp/lp_primal_core_solver.cpp
Examining data/z3-4.8.9/src/math/lp/lp_primal_core_solver.h
Examining data/z3-4.8.9/src/math/lp/lp_primal_core_solver_def.h
Examining data/z3-4.8.9/src/math/lp/lp_primal_core_solver_tableau_def.h
Examining data/z3-4.8.9/src/math/lp/lp_primal_simplex.cpp
Examining data/z3-4.8.9/src/math/lp/lp_primal_simplex.h
Examining data/z3-4.8.9/src/math/lp/lp_primal_simplex_def.h
Examining data/z3-4.8.9/src/math/lp/lp_settings.cpp
Examining data/z3-4.8.9/src/math/lp/lp_settings.h
Examining data/z3-4.8.9/src/math/lp/lp_settings_def.h
Examining data/z3-4.8.9/src/math/lp/lp_solver.cpp
Examining data/z3-4.8.9/src/math/lp/lp_solver.h
Examining data/z3-4.8.9/src/math/lp/lp_solver_def.h
Examining data/z3-4.8.9/src/math/lp/lp_types.h
Examining data/z3-4.8.9/src/math/lp/lp_utils.cpp
Examining data/z3-4.8.9/src/math/lp/lp_utils.h
Examining data/z3-4.8.9/src/math/lp/lu.cpp
Examining data/z3-4.8.9/src/math/lp/lu.h
Examining data/z3-4.8.9/src/math/lp/lu_def.h
Examining data/z3-4.8.9/src/math/lp/matrix.cpp
Examining data/z3-4.8.9/src/math/lp/matrix.h
Examining data/z3-4.8.9/src/math/lp/matrix_def.h
Examining data/z3-4.8.9/src/math/lp/mon_eq.cpp
Examining data/z3-4.8.9/src/math/lp/monic.h
Examining data/z3-4.8.9/src/math/lp/monomial_bounds.cpp
Examining data/z3-4.8.9/src/math/lp/monomial_bounds.h
Examining data/z3-4.8.9/src/math/lp/mps_reader.h
Examining data/z3-4.8.9/src/math/lp/nex.h
Examining data/z3-4.8.9/src/math/lp/nex_creator.cpp
Examining data/z3-4.8.9/src/math/lp/nex_creator.h
Examining data/z3-4.8.9/src/math/lp/nla_basics_lemmas.cpp
Examining data/z3-4.8.9/src/math/lp/nla_basics_lemmas.h
Examining data/z3-4.8.9/src/math/lp/nla_common.cpp
Examining data/z3-4.8.9/src/math/lp/nla_common.h
Examining data/z3-4.8.9/src/math/lp/nla_core.cpp
Examining data/z3-4.8.9/src/math/lp/nla_core.h
Examining data/z3-4.8.9/src/math/lp/nla_defs.h
Examining data/z3-4.8.9/src/math/lp/nla_intervals.cpp
Examining data/z3-4.8.9/src/math/lp/nla_intervals.h
Examining data/z3-4.8.9/src/math/lp/nla_monotone_lemmas.cpp
Examining data/z3-4.8.9/src/math/lp/nla_monotone_lemmas.h
Examining data/z3-4.8.9/src/math/lp/nla_order_lemmas.cpp
Examining data/z3-4.8.9/src/math/lp/nla_order_lemmas.h
Examining data/z3-4.8.9/src/math/lp/nla_settings.h
Examining data/z3-4.8.9/src/math/lp/nla_solver.cpp
Examining data/z3-4.8.9/src/math/lp/nla_solver.h
Examining data/z3-4.8.9/src/math/lp/nla_tangent_lemmas.cpp
Examining data/z3-4.8.9/src/math/lp/nla_tangent_lemmas.h
Examining data/z3-4.8.9/src/math/lp/nra_solver.cpp
Examining data/z3-4.8.9/src/math/lp/nra_solver.h
Examining data/z3-4.8.9/src/math/lp/numeric_pair.h
Examining data/z3-4.8.9/src/math/lp/permutation_matrix.cpp
Examining data/z3-4.8.9/src/math/lp/permutation_matrix.h
Examining data/z3-4.8.9/src/math/lp/permutation_matrix_def.h
Examining data/z3-4.8.9/src/math/lp/polynomial.h
Examining data/z3-4.8.9/src/math/lp/random_updater.cpp
Examining data/z3-4.8.9/src/math/lp/random_updater.h
Examining data/z3-4.8.9/src/math/lp/random_updater_def.h
Examining data/z3-4.8.9/src/math/lp/row_eta_matrix.cpp
Examining data/z3-4.8.9/src/math/lp/row_eta_matrix.h
Examining data/z3-4.8.9/src/math/lp/row_eta_matrix_def.h
Examining data/z3-4.8.9/src/math/lp/scaler.cpp
Examining data/z3-4.8.9/src/math/lp/scaler.h
Examining data/z3-4.8.9/src/math/lp/scaler_def.h
Examining data/z3-4.8.9/src/math/lp/sparse_vector.h
Examining data/z3-4.8.9/src/math/lp/square_dense_submatrix.cpp
Examining data/z3-4.8.9/src/math/lp/square_dense_submatrix.h
Examining data/z3-4.8.9/src/math/lp/square_dense_submatrix_def.h
Examining data/z3-4.8.9/src/math/lp/square_sparse_matrix.cpp
Examining data/z3-4.8.9/src/math/lp/square_sparse_matrix.h
Examining data/z3-4.8.9/src/math/lp/square_sparse_matrix_def.h
Examining data/z3-4.8.9/src/math/lp/stacked_vector.h
Examining data/z3-4.8.9/src/math/lp/static_matrix.cpp
Examining data/z3-4.8.9/src/math/lp/static_matrix.h
Examining data/z3-4.8.9/src/math/lp/static_matrix_def.h
Examining data/z3-4.8.9/src/math/lp/tail_matrix.h
Examining data/z3-4.8.9/src/math/lp/test_bound_analyzer.h
Examining data/z3-4.8.9/src/math/lp/u_set.h
Examining data/z3-4.8.9/src/math/lp/ul_pair.h
Examining data/z3-4.8.9/src/math/lp/var_eqs.h
Examining data/z3-4.8.9/src/math/lp/var_register.h
Examining data/z3-4.8.9/src/math/polynomial/algebraic_numbers.cpp
Examining data/z3-4.8.9/src/math/polynomial/algebraic_numbers.h
Examining data/z3-4.8.9/src/math/polynomial/linear_eq_solver.h
Examining data/z3-4.8.9/src/math/polynomial/polynomial.cpp
Examining data/z3-4.8.9/src/math/polynomial/polynomial.h
Examining data/z3-4.8.9/src/math/polynomial/polynomial_cache.cpp
Examining data/z3-4.8.9/src/math/polynomial/polynomial_cache.h
Examining data/z3-4.8.9/src/math/polynomial/polynomial_primes.h
Examining data/z3-4.8.9/src/math/polynomial/polynomial_var2value.h
Examining data/z3-4.8.9/src/math/polynomial/rpolynomial.cpp
Examining data/z3-4.8.9/src/math/polynomial/rpolynomial.h
Examining data/z3-4.8.9/src/math/polynomial/sexpr2upolynomial.cpp
Examining data/z3-4.8.9/src/math/polynomial/sexpr2upolynomial.h
Examining data/z3-4.8.9/src/math/polynomial/upolynomial.cpp
Examining data/z3-4.8.9/src/math/polynomial/upolynomial.h
Examining data/z3-4.8.9/src/math/polynomial/upolynomial_factorization.cpp
Examining data/z3-4.8.9/src/math/polynomial/upolynomial_factorization.h
Examining data/z3-4.8.9/src/math/polynomial/upolynomial_factorization_int.h
Examining data/z3-4.8.9/src/math/realclosure/mpz_matrix.cpp
Examining data/z3-4.8.9/src/math/realclosure/mpz_matrix.h
Examining data/z3-4.8.9/src/math/realclosure/realclosure.cpp
Examining data/z3-4.8.9/src/math/realclosure/realclosure.h
Examining data/z3-4.8.9/src/math/simplex/bit_matrix.cpp
Examining data/z3-4.8.9/src/math/simplex/bit_matrix.h
Examining data/z3-4.8.9/src/math/simplex/model_based_opt.cpp
Examining data/z3-4.8.9/src/math/simplex/model_based_opt.h
Examining data/z3-4.8.9/src/math/simplex/network_flow.h
Examining data/z3-4.8.9/src/math/simplex/network_flow_def.h
Examining data/z3-4.8.9/src/math/simplex/simplex.cpp
Examining data/z3-4.8.9/src/math/simplex/simplex.h
Examining data/z3-4.8.9/src/math/simplex/simplex_def.h
Examining data/z3-4.8.9/src/math/simplex/sparse_matrix.h
Examining data/z3-4.8.9/src/math/simplex/sparse_matrix_def.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving.cpp
Examining data/z3-4.8.9/src/math/subpaving/subpaving.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving_hwf.cpp
Examining data/z3-4.8.9/src/math/subpaving/subpaving_hwf.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving_mpf.cpp
Examining data/z3-4.8.9/src/math/subpaving/subpaving_mpf.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving_mpff.cpp
Examining data/z3-4.8.9/src/math/subpaving/subpaving_mpff.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving_mpfx.cpp
Examining data/z3-4.8.9/src/math/subpaving/subpaving_mpfx.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving_mpq.cpp
Examining data/z3-4.8.9/src/math/subpaving/subpaving_mpq.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving_t.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h
Examining data/z3-4.8.9/src/math/subpaving/subpaving_types.h
Examining data/z3-4.8.9/src/math/subpaving/tactic/expr2subpaving.cpp
Examining data/z3-4.8.9/src/math/subpaving/tactic/expr2subpaving.h
Examining data/z3-4.8.9/src/math/subpaving/tactic/subpaving_tactic.cpp
Examining data/z3-4.8.9/src/math/subpaving/tactic/subpaving_tactic.h
Examining data/z3-4.8.9/src/model/array_factory.cpp
Examining data/z3-4.8.9/src/model/array_factory.h
Examining data/z3-4.8.9/src/model/datatype_factory.cpp
Examining data/z3-4.8.9/src/model/datatype_factory.h
Examining data/z3-4.8.9/src/model/func_interp.cpp
Examining data/z3-4.8.9/src/model/func_interp.h
Examining data/z3-4.8.9/src/model/model.cpp
Examining data/z3-4.8.9/src/model/model.h
Examining data/z3-4.8.9/src/model/model2expr.cpp
Examining data/z3-4.8.9/src/model/model2expr.h
Examining data/z3-4.8.9/src/model/model_core.cpp
Examining data/z3-4.8.9/src/model/model_core.h
Examining data/z3-4.8.9/src/model/model_evaluator.cpp
Examining data/z3-4.8.9/src/model/model_evaluator.h
Examining data/z3-4.8.9/src/model/model_implicant.cpp
Examining data/z3-4.8.9/src/model/model_implicant.h
Examining data/z3-4.8.9/src/model/model_pp.cpp
Examining data/z3-4.8.9/src/model/model_pp.h
Examining data/z3-4.8.9/src/model/model_smt2_pp.cpp
Examining data/z3-4.8.9/src/model/model_smt2_pp.h
Examining data/z3-4.8.9/src/model/model_v2_pp.cpp
Examining data/z3-4.8.9/src/model/model_v2_pp.h
Examining data/z3-4.8.9/src/model/numeral_factory.cpp
Examining data/z3-4.8.9/src/model/numeral_factory.h
Examining data/z3-4.8.9/src/model/seq_factory.h
Examining data/z3-4.8.9/src/model/struct_factory.cpp
Examining data/z3-4.8.9/src/model/struct_factory.h
Examining data/z3-4.8.9/src/model/value_factory.cpp
Examining data/z3-4.8.9/src/model/value_factory.h
Examining data/z3-4.8.9/src/muz/base/bind_variables.cpp
Examining data/z3-4.8.9/src/muz/base/bind_variables.h
Examining data/z3-4.8.9/src/muz/base/dl_boogie_proof.cpp
Examining data/z3-4.8.9/src/muz/base/dl_boogie_proof.h
Examining data/z3-4.8.9/src/muz/base/dl_context.cpp
Examining data/z3-4.8.9/src/muz/base/dl_context.h
Examining data/z3-4.8.9/src/muz/base/dl_costs.cpp
Examining data/z3-4.8.9/src/muz/base/dl_costs.h
Examining data/z3-4.8.9/src/muz/base/dl_engine_base.h
Examining data/z3-4.8.9/src/muz/base/dl_rule.cpp
Examining data/z3-4.8.9/src/muz/base/dl_rule.h
Examining data/z3-4.8.9/src/muz/base/dl_rule_set.cpp
Examining data/z3-4.8.9/src/muz/base/dl_rule_set.h
Examining data/z3-4.8.9/src/muz/base/dl_rule_subsumption_index.cpp
Examining data/z3-4.8.9/src/muz/base/dl_rule_subsumption_index.h
Examining data/z3-4.8.9/src/muz/base/dl_rule_transformer.cpp
Examining data/z3-4.8.9/src/muz/base/dl_rule_transformer.h
Examining data/z3-4.8.9/src/muz/base/dl_util.cpp
Examining data/z3-4.8.9/src/muz/base/dl_util.h
Examining data/z3-4.8.9/src/muz/base/hnf.cpp
Examining data/z3-4.8.9/src/muz/base/hnf.h
Examining data/z3-4.8.9/src/muz/base/rule_properties.cpp
Examining data/z3-4.8.9/src/muz/base/rule_properties.h
Examining data/z3-4.8.9/src/muz/bmc/dl_bmc_engine.cpp
Examining data/z3-4.8.9/src/muz/bmc/dl_bmc_engine.h
Examining data/z3-4.8.9/src/muz/clp/clp_context.cpp
Examining data/z3-4.8.9/src/muz/clp/clp_context.h
Examining data/z3-4.8.9/src/muz/dataflow/dataflow.cpp
Examining data/z3-4.8.9/src/muz/dataflow/dataflow.h
Examining data/z3-4.8.9/src/muz/dataflow/reachability.h
Examining data/z3-4.8.9/src/muz/ddnf/ddnf.cpp
Examining data/z3-4.8.9/src/muz/ddnf/ddnf.h
Examining data/z3-4.8.9/src/muz/fp/datalog_parser.cpp
Examining data/z3-4.8.9/src/muz/fp/datalog_parser.h
Examining data/z3-4.8.9/src/muz/fp/dl_cmds.cpp
Examining data/z3-4.8.9/src/muz/fp/dl_cmds.h
Examining data/z3-4.8.9/src/muz/fp/dl_register_engine.cpp
Examining data/z3-4.8.9/src/muz/fp/dl_register_engine.h
Examining data/z3-4.8.9/src/muz/fp/horn_tactic.cpp
Examining data/z3-4.8.9/src/muz/fp/horn_tactic.h
Examining data/z3-4.8.9/src/muz/rel/aig_exporter.cpp
Examining data/z3-4.8.9/src/muz/rel/aig_exporter.h
Examining data/z3-4.8.9/src/muz/rel/check_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/check_relation.h
Examining data/z3-4.8.9/src/muz/rel/dl_base.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_base.h
Examining data/z3-4.8.9/src/muz/rel/dl_bound_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_bound_relation.h
Examining data/z3-4.8.9/src/muz/rel/dl_check_table.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_check_table.h
Examining data/z3-4.8.9/src/muz/rel/dl_compiler.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_compiler.h
Examining data/z3-4.8.9/src/muz/rel/dl_external_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_external_relation.h
Examining data/z3-4.8.9/src/muz/rel/dl_finite_product_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_finite_product_relation.h
Examining data/z3-4.8.9/src/muz/rel/dl_instruction.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_instruction.h
Examining data/z3-4.8.9/src/muz/rel/dl_interval_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_interval_relation.h
Examining data/z3-4.8.9/src/muz/rel/dl_lazy_table.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_lazy_table.h
Examining data/z3-4.8.9/src/muz/rel/dl_mk_explanations.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_mk_explanations.h
Examining data/z3-4.8.9/src/muz/rel/dl_mk_similarity_compressor.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_mk_similarity_compressor.h
Examining data/z3-4.8.9/src/muz/rel/dl_mk_simple_joins.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_mk_simple_joins.h
Examining data/z3-4.8.9/src/muz/rel/dl_product_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_product_relation.h
Examining data/z3-4.8.9/src/muz/rel/dl_relation_manager.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_relation_manager.h
Examining data/z3-4.8.9/src/muz/rel/dl_sieve_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_sieve_relation.h
Examining data/z3-4.8.9/src/muz/rel/dl_sparse_table.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_sparse_table.h
Examining data/z3-4.8.9/src/muz/rel/dl_table.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_table.h
Examining data/z3-4.8.9/src/muz/rel/dl_table_plugin.h
Examining data/z3-4.8.9/src/muz/rel/dl_table_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/dl_table_relation.h
Examining data/z3-4.8.9/src/muz/rel/dl_vector_relation.h
Examining data/z3-4.8.9/src/muz/rel/doc.cpp
Examining data/z3-4.8.9/src/muz/rel/doc.h
Examining data/z3-4.8.9/src/muz/rel/karr_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/karr_relation.h
Examining data/z3-4.8.9/src/muz/rel/rel_context.cpp
Examining data/z3-4.8.9/src/muz/rel/rel_context.h
Examining data/z3-4.8.9/src/muz/rel/tbv.cpp
Examining data/z3-4.8.9/src/muz/rel/tbv.h
Examining data/z3-4.8.9/src/muz/rel/udoc_relation.cpp
Examining data/z3-4.8.9/src/muz/rel/udoc_relation.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_antiunify.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_antiunify.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_arith_generalizers.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_callback.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_callback.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_context.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_context.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_dl_interface.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_dl_interface.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_farkas_learner.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_farkas_learner.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_generalizers.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_generalizers.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_iuc_proof.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_iuc_proof.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_iuc_solver.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_iuc_solver.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_json.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_json.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_legacy_frames.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_legacy_frames.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_legacy_mbp.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_legacy_mev.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_legacy_mev.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_manager.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_manager.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_matrix.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_matrix.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_mbc.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_mbc.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_mev_array.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_mev_array.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_pdr.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_pdr.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_proof_utils.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_proof_utils.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_prop_solver.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_prop_solver.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_qe_project.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_qe_project.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_quant_generalizer.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_sat_answer.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_sat_answer.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_sem_matcher.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_sem_matcher.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_sym_mux.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_sym_mux.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_unsat_core_learner.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_unsat_core_learner.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_unsat_core_plugin.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_unsat_core_plugin.h
Examining data/z3-4.8.9/src/muz/spacer/spacer_util.cpp
Examining data/z3-4.8.9/src/muz/spacer/spacer_util.h
Examining data/z3-4.8.9/src/muz/tab/tab_context.cpp
Examining data/z3-4.8.9/src/muz/tab/tab_context.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_array_blast.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_array_blast.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_array_eq_rewrite.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_array_eq_rewrite.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_array_instantiation.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_array_instantiation.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_backwards.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_backwards.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_bit_blast.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_bit_blast.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_coalesce.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_coalesce.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_coi_filter.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_coi_filter.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_different.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_elim_term_ite.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_elim_term_ite.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_filter_rules.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_filter_rules.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_interp_tail_simplifier.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_karr_invariants.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_karr_invariants.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_loop_counter.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_loop_counter.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_magic_sets.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_magic_sets.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_magic_symbolic.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_magic_symbolic.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_quantifier_abstraction.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_quantifier_instantiation.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_rule_inliner.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_rule_inliner.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_scale.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_scale.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_separate_negated_tails.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_separate_negated_tails.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_slice.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_slice.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_subsumption_checker.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_subsumption_checker.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_synchronize.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_synchronize.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_unbound_compressor.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_unbound_compressor.h
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_unfold.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_mk_unfold.h
Examining data/z3-4.8.9/src/muz/transforms/dl_transforms.cpp
Examining data/z3-4.8.9/src/muz/transforms/dl_transforms.h
Examining data/z3-4.8.9/src/nlsat/nlsat_assignment.h
Examining data/z3-4.8.9/src/nlsat/nlsat_clause.cpp
Examining data/z3-4.8.9/src/nlsat/nlsat_clause.h
Examining data/z3-4.8.9/src/nlsat/nlsat_evaluator.cpp
Examining data/z3-4.8.9/src/nlsat/nlsat_evaluator.h
Examining data/z3-4.8.9/src/nlsat/nlsat_explain.cpp
Examining data/z3-4.8.9/src/nlsat/nlsat_explain.h
Examining data/z3-4.8.9/src/nlsat/nlsat_interval_set.cpp
Examining data/z3-4.8.9/src/nlsat/nlsat_interval_set.h
Examining data/z3-4.8.9/src/nlsat/nlsat_justification.h
Examining data/z3-4.8.9/src/nlsat/nlsat_scoped_literal_vector.h
Examining data/z3-4.8.9/src/nlsat/nlsat_solver.cpp
Examining data/z3-4.8.9/src/nlsat/nlsat_solver.h
Examining data/z3-4.8.9/src/nlsat/nlsat_types.cpp
Examining data/z3-4.8.9/src/nlsat/nlsat_types.h
Examining data/z3-4.8.9/src/nlsat/tactic/goal2nlsat.cpp
Examining data/z3-4.8.9/src/nlsat/tactic/goal2nlsat.h
Examining data/z3-4.8.9/src/nlsat/tactic/nlsat_tactic.cpp
Examining data/z3-4.8.9/src/nlsat/tactic/nlsat_tactic.h
Examining data/z3-4.8.9/src/nlsat/tactic/qfnra_nlsat_tactic.cpp
Examining data/z3-4.8.9/src/nlsat/tactic/qfnra_nlsat_tactic.h
Examining data/z3-4.8.9/src/opt/maxlex.cpp
Examining data/z3-4.8.9/src/opt/maxlex.h
Examining data/z3-4.8.9/src/opt/maxres.cpp
Examining data/z3-4.8.9/src/opt/maxres.h
Examining data/z3-4.8.9/src/opt/maxsmt.cpp
Examining data/z3-4.8.9/src/opt/maxsmt.h
Examining data/z3-4.8.9/src/opt/opt_cmds.cpp
Examining data/z3-4.8.9/src/opt/opt_cmds.h
Examining data/z3-4.8.9/src/opt/opt_context.cpp
Examining data/z3-4.8.9/src/opt/opt_context.h
Examining data/z3-4.8.9/src/opt/opt_pareto.cpp
Examining data/z3-4.8.9/src/opt/opt_pareto.h
Examining data/z3-4.8.9/src/opt/opt_parse.cpp
Examining data/z3-4.8.9/src/opt/opt_parse.h
Examining data/z3-4.8.9/src/opt/opt_sls_solver.h
Examining data/z3-4.8.9/src/opt/opt_solver.cpp
Examining data/z3-4.8.9/src/opt/opt_solver.h
Examining data/z3-4.8.9/src/opt/optsmt.cpp
Examining data/z3-4.8.9/src/opt/optsmt.h
Examining data/z3-4.8.9/src/opt/pb_sls.cpp
Examining data/z3-4.8.9/src/opt/pb_sls.h
Examining data/z3-4.8.9/src/opt/sortmax.cpp
Examining data/z3-4.8.9/src/opt/wmax.cpp
Examining data/z3-4.8.9/src/opt/wmax.h
Examining data/z3-4.8.9/src/params/bit_blaster_params.h
Examining data/z3-4.8.9/src/params/context_params.cpp
Examining data/z3-4.8.9/src/params/context_params.h
Examining data/z3-4.8.9/src/params/pattern_inference_params.cpp
Examining data/z3-4.8.9/src/params/pattern_inference_params.h
Examining data/z3-4.8.9/src/parsers/smt2/marshal.cpp
Examining data/z3-4.8.9/src/parsers/smt2/marshal.h
Examining data/z3-4.8.9/src/parsers/smt2/smt2parser.cpp
Examining data/z3-4.8.9/src/parsers/smt2/smt2parser.h
Examining data/z3-4.8.9/src/parsers/smt2/smt2scanner.cpp
Examining data/z3-4.8.9/src/parsers/smt2/smt2scanner.h
Examining data/z3-4.8.9/src/parsers/util/cost_parser.cpp
Examining data/z3-4.8.9/src/parsers/util/cost_parser.h
Examining data/z3-4.8.9/src/parsers/util/pattern_validation.cpp
Examining data/z3-4.8.9/src/parsers/util/pattern_validation.h
Examining data/z3-4.8.9/src/parsers/util/scanner.cpp
Examining data/z3-4.8.9/src/parsers/util/scanner.h
Examining data/z3-4.8.9/src/parsers/util/simple_parser.cpp
Examining data/z3-4.8.9/src/parsers/util/simple_parser.h
Examining data/z3-4.8.9/src/qe/nlarith_util.cpp
Examining data/z3-4.8.9/src/qe/nlarith_util.h
Examining data/z3-4.8.9/src/qe/nlqsat.cpp
Examining data/z3-4.8.9/src/qe/nlqsat.h
Examining data/z3-4.8.9/src/qe/qe.cpp
Examining data/z3-4.8.9/src/qe/qe.h
Examining data/z3-4.8.9/src/qe/qe_arith.cpp
Examining data/z3-4.8.9/src/qe/qe_arith.h
Examining data/z3-4.8.9/src/qe/qe_arith_plugin.cpp
Examining data/z3-4.8.9/src/qe/qe_array_plugin.cpp
Examining data/z3-4.8.9/src/qe/qe_arrays.cpp
Examining data/z3-4.8.9/src/qe/qe_arrays.h
Examining data/z3-4.8.9/src/qe/qe_bool_plugin.cpp
Examining data/z3-4.8.9/src/qe/qe_bv_plugin.cpp
Examining data/z3-4.8.9/src/qe/qe_cmd.cpp
Examining data/z3-4.8.9/src/qe/qe_cmd.h
Examining data/z3-4.8.9/src/qe/qe_datatype_plugin.cpp
Examining data/z3-4.8.9/src/qe/qe_datatypes.cpp
Examining data/z3-4.8.9/src/qe/qe_datatypes.h
Examining data/z3-4.8.9/src/qe/qe_dl_plugin.cpp
Examining data/z3-4.8.9/src/qe/qe_lite.cpp
Examining data/z3-4.8.9/src/qe/qe_lite.h
Examining data/z3-4.8.9/src/qe/qe_mbi.cpp
Examining data/z3-4.8.9/src/qe/qe_mbi.h
Examining data/z3-4.8.9/src/qe/qe_mbp.cpp
Examining data/z3-4.8.9/src/qe/qe_mbp.h
Examining data/z3-4.8.9/src/qe/qe_solve_plugin.cpp
Examining data/z3-4.8.9/src/qe/qe_solve_plugin.h
Examining data/z3-4.8.9/src/qe/qe_tactic.cpp
Examining data/z3-4.8.9/src/qe/qe_tactic.h
Examining data/z3-4.8.9/src/qe/qe_term_graph.cpp
Examining data/z3-4.8.9/src/qe/qe_term_graph.h
Examining data/z3-4.8.9/src/qe/qe_vartest.h
Examining data/z3-4.8.9/src/qe/qsat.cpp
Examining data/z3-4.8.9/src/qe/qsat.h
Examining data/z3-4.8.9/src/sat/dimacs.cpp
Examining data/z3-4.8.9/src/sat/dimacs.h
Examining data/z3-4.8.9/src/sat/sat_aig_cuts.cpp
Examining data/z3-4.8.9/src/sat/sat_aig_cuts.h
Examining data/z3-4.8.9/src/sat/sat_aig_finder.cpp
Examining data/z3-4.8.9/src/sat/sat_aig_finder.h
Examining data/z3-4.8.9/src/sat/sat_allocator.h
Examining data/z3-4.8.9/src/sat/sat_anf_simplifier.cpp
Examining data/z3-4.8.9/src/sat/sat_anf_simplifier.h
Examining data/z3-4.8.9/src/sat/sat_asymm_branch.cpp
Examining data/z3-4.8.9/src/sat/sat_asymm_branch.h
Examining data/z3-4.8.9/src/sat/sat_bcd.cpp
Examining data/z3-4.8.9/src/sat/sat_bcd.h
Examining data/z3-4.8.9/src/sat/sat_big.cpp
Examining data/z3-4.8.9/src/sat/sat_big.h
Examining data/z3-4.8.9/src/sat/sat_binspr.cpp
Examining data/z3-4.8.9/src/sat/sat_binspr.h
Examining data/z3-4.8.9/src/sat/sat_clause.cpp
Examining data/z3-4.8.9/src/sat/sat_clause.h
Examining data/z3-4.8.9/src/sat/sat_clause_set.cpp
Examining data/z3-4.8.9/src/sat/sat_clause_set.h
Examining data/z3-4.8.9/src/sat/sat_clause_use_list.cpp
Examining data/z3-4.8.9/src/sat/sat_clause_use_list.h
Examining data/z3-4.8.9/src/sat/sat_cleaner.cpp
Examining data/z3-4.8.9/src/sat/sat_cleaner.h
Examining data/z3-4.8.9/src/sat/sat_config.cpp
Examining data/z3-4.8.9/src/sat/sat_config.h
Examining data/z3-4.8.9/src/sat/sat_cut_simplifier.cpp
Examining data/z3-4.8.9/src/sat/sat_cut_simplifier.h
Examining data/z3-4.8.9/src/sat/sat_cutset.cpp
Examining data/z3-4.8.9/src/sat/sat_cutset.h
Examining data/z3-4.8.9/src/sat/sat_cutset_compute_shift.h
Examining data/z3-4.8.9/src/sat/sat_ddfw.cpp
Examining data/z3-4.8.9/src/sat/sat_ddfw.h
Examining data/z3-4.8.9/src/sat/sat_drat.cpp
Examining data/z3-4.8.9/src/sat/sat_drat.h
Examining data/z3-4.8.9/src/sat/sat_elim_eqs.cpp
Examining data/z3-4.8.9/src/sat/sat_elim_eqs.h
Examining data/z3-4.8.9/src/sat/sat_elim_vars.cpp
Examining data/z3-4.8.9/src/sat/sat_elim_vars.h
Examining data/z3-4.8.9/src/sat/sat_extension.h
Examining data/z3-4.8.9/src/sat/sat_integrity_checker.cpp
Examining data/z3-4.8.9/src/sat/sat_integrity_checker.h
Examining data/z3-4.8.9/src/sat/sat_justification.h
Examining data/z3-4.8.9/src/sat/sat_local_search.cpp
Examining data/z3-4.8.9/src/sat/sat_local_search.h
Examining data/z3-4.8.9/src/sat/sat_lookahead.cpp
Examining data/z3-4.8.9/src/sat/sat_lookahead.h
Examining data/z3-4.8.9/src/sat/sat_lut_finder.cpp
Examining data/z3-4.8.9/src/sat/sat_lut_finder.h
Examining data/z3-4.8.9/src/sat/sat_model_converter.cpp
Examining data/z3-4.8.9/src/sat/sat_model_converter.h
Examining data/z3-4.8.9/src/sat/sat_mus.cpp
Examining data/z3-4.8.9/src/sat/sat_mus.h
Examining data/z3-4.8.9/src/sat/sat_npn3_finder.cpp
Examining data/z3-4.8.9/src/sat/sat_npn3_finder.h
Examining data/z3-4.8.9/src/sat/sat_parallel.cpp
Examining data/z3-4.8.9/src/sat/sat_parallel.h
Examining data/z3-4.8.9/src/sat/sat_prob.cpp
Examining data/z3-4.8.9/src/sat/sat_prob.h
Examining data/z3-4.8.9/src/sat/sat_probing.cpp
Examining data/z3-4.8.9/src/sat/sat_probing.h
Examining data/z3-4.8.9/src/sat/sat_scc.cpp
Examining data/z3-4.8.9/src/sat/sat_scc.h
Examining data/z3-4.8.9/src/sat/sat_simplifier.cpp
Examining data/z3-4.8.9/src/sat/sat_simplifier.h
Examining data/z3-4.8.9/src/sat/sat_solver.cpp
Examining data/z3-4.8.9/src/sat/sat_solver.h
Examining data/z3-4.8.9/src/sat/sat_solver/inc_sat_solver.cpp
Examining data/z3-4.8.9/src/sat/sat_solver/inc_sat_solver.h
Examining data/z3-4.8.9/src/sat/sat_solver_core.h
Examining data/z3-4.8.9/src/sat/sat_types.h
Examining data/z3-4.8.9/src/sat/sat_var_queue.h
Examining data/z3-4.8.9/src/sat/sat_watched.cpp
Examining data/z3-4.8.9/src/sat/sat_watched.h
Examining data/z3-4.8.9/src/sat/sat_xor_finder.cpp
Examining data/z3-4.8.9/src/sat/sat_xor_finder.h
Examining data/z3-4.8.9/src/sat/smt/array_axioms.cpp
Examining data/z3-4.8.9/src/sat/smt/array_internalize.cpp
Examining data/z3-4.8.9/src/sat/smt/array_model.cpp
Examining data/z3-4.8.9/src/sat/smt/array_solver.cpp
Examining data/z3-4.8.9/src/sat/smt/array_solver.h
Examining data/z3-4.8.9/src/sat/smt/atom2bool_var.cpp
Examining data/z3-4.8.9/src/sat/smt/atom2bool_var.h
Examining data/z3-4.8.9/src/sat/smt/ba_internalize.cpp
Examining data/z3-4.8.9/src/sat/smt/ba_solver.cpp
Examining data/z3-4.8.9/src/sat/smt/ba_solver.h
Examining data/z3-4.8.9/src/sat/smt/bv_ackerman.cpp
Examining data/z3-4.8.9/src/sat/smt/bv_ackerman.h
Examining data/z3-4.8.9/src/sat/smt/bv_internalize.cpp
Examining data/z3-4.8.9/src/sat/smt/bv_solver.cpp
Examining data/z3-4.8.9/src/sat/smt/bv_solver.h
Examining data/z3-4.8.9/src/sat/smt/euf_ackerman.cpp
Examining data/z3-4.8.9/src/sat/smt/euf_ackerman.h
Examining data/z3-4.8.9/src/sat/smt/euf_internalize.cpp
Examining data/z3-4.8.9/src/sat/smt/euf_invariant.cpp
Examining data/z3-4.8.9/src/sat/smt/euf_model.cpp
Examining data/z3-4.8.9/src/sat/smt/euf_proof.cpp
Examining data/z3-4.8.9/src/sat/smt/euf_solver.cpp
Examining data/z3-4.8.9/src/sat/smt/euf_solver.h
Examining data/z3-4.8.9/src/sat/smt/sat_smt.h
Examining data/z3-4.8.9/src/sat/smt/sat_th.cpp
Examining data/z3-4.8.9/src/sat/smt/sat_th.h
Examining data/z3-4.8.9/src/sat/smt/xor_solver.cpp
Examining data/z3-4.8.9/src/sat/tactic/goal2sat.cpp
Examining data/z3-4.8.9/src/sat/tactic/goal2sat.h
Examining data/z3-4.8.9/src/sat/tactic/sat_tactic.cpp
Examining data/z3-4.8.9/src/sat/tactic/sat_tactic.h
Examining data/z3-4.8.9/src/shell/datalog_frontend.cpp
Examining data/z3-4.8.9/src/shell/datalog_frontend.h
Examining data/z3-4.8.9/src/shell/dimacs_frontend.cpp
Examining data/z3-4.8.9/src/shell/dimacs_frontend.h
Examining data/z3-4.8.9/src/shell/drat_frontend.cpp
Examining data/z3-4.8.9/src/shell/drat_frontend.h
Examining data/z3-4.8.9/src/shell/lp_frontend.cpp
Examining data/z3-4.8.9/src/shell/lp_frontend.h
Examining data/z3-4.8.9/src/shell/main.cpp
Examining data/z3-4.8.9/src/shell/opt_frontend.cpp
Examining data/z3-4.8.9/src/shell/opt_frontend.h
Examining data/z3-4.8.9/src/shell/options.h
Examining data/z3-4.8.9/src/shell/smtlib_frontend.cpp
Examining data/z3-4.8.9/src/shell/smtlib_frontend.h
Examining data/z3-4.8.9/src/shell/z3_log_frontend.cpp
Examining data/z3-4.8.9/src/shell/z3_log_frontend.h
Examining data/z3-4.8.9/src/smt/arith_eq_adapter.cpp
Examining data/z3-4.8.9/src/smt/arith_eq_adapter.h
Examining data/z3-4.8.9/src/smt/arith_eq_solver.cpp
Examining data/z3-4.8.9/src/smt/arith_eq_solver.h
Examining data/z3-4.8.9/src/smt/asserted_formulas.cpp
Examining data/z3-4.8.9/src/smt/asserted_formulas.h
Examining data/z3-4.8.9/src/smt/cached_var_subst.cpp
Examining data/z3-4.8.9/src/smt/cached_var_subst.h
Examining data/z3-4.8.9/src/smt/cost_evaluator.cpp
Examining data/z3-4.8.9/src/smt/cost_evaluator.h
Examining data/z3-4.8.9/src/smt/database.h
Examining data/z3-4.8.9/src/smt/diff_logic.h
Examining data/z3-4.8.9/src/smt/dyn_ack.cpp
Examining data/z3-4.8.9/src/smt/dyn_ack.h
Examining data/z3-4.8.9/src/smt/elim_term_ite.cpp
Examining data/z3-4.8.9/src/smt/elim_term_ite.h
Examining data/z3-4.8.9/src/smt/expr_context_simplifier.cpp
Examining data/z3-4.8.9/src/smt/expr_context_simplifier.h
Examining data/z3-4.8.9/src/smt/fingerprints.cpp
Examining data/z3-4.8.9/src/smt/fingerprints.h
Examining data/z3-4.8.9/src/smt/mam.cpp
Examining data/z3-4.8.9/src/smt/mam.h
Examining data/z3-4.8.9/src/smt/old_interval.cpp
Examining data/z3-4.8.9/src/smt/old_interval.h
Examining data/z3-4.8.9/src/smt/params/dyn_ack_params.cpp
Examining data/z3-4.8.9/src/smt/params/dyn_ack_params.h
Examining data/z3-4.8.9/src/smt/params/preprocessor_params.cpp
Examining data/z3-4.8.9/src/smt/params/preprocessor_params.h
Examining data/z3-4.8.9/src/smt/params/qi_params.cpp
Examining data/z3-4.8.9/src/smt/params/qi_params.h
Examining data/z3-4.8.9/src/smt/params/smt_params.cpp
Examining data/z3-4.8.9/src/smt/params/smt_params.h
Examining data/z3-4.8.9/src/smt/params/theory_arith_params.cpp
Examining data/z3-4.8.9/src/smt/params/theory_arith_params.h
Examining data/z3-4.8.9/src/smt/params/theory_array_params.cpp
Examining data/z3-4.8.9/src/smt/params/theory_array_params.h
Examining data/z3-4.8.9/src/smt/params/theory_bv_params.cpp
Examining data/z3-4.8.9/src/smt/params/theory_bv_params.h
Examining data/z3-4.8.9/src/smt/params/theory_datatype_params.h
Examining data/z3-4.8.9/src/smt/params/theory_pb_params.cpp
Examining data/z3-4.8.9/src/smt/params/theory_pb_params.h
Examining data/z3-4.8.9/src/smt/params/theory_seq_params.cpp
Examining data/z3-4.8.9/src/smt/params/theory_seq_params.h
Examining data/z3-4.8.9/src/smt/params/theory_str_params.cpp
Examining data/z3-4.8.9/src/smt/params/theory_str_params.h
Examining data/z3-4.8.9/src/smt/proto_model/proto_model.cpp
Examining data/z3-4.8.9/src/smt/proto_model/proto_model.h
Examining data/z3-4.8.9/src/smt/qi_queue.cpp
Examining data/z3-4.8.9/src/smt/qi_queue.h
Examining data/z3-4.8.9/src/smt/seq_axioms.cpp
Examining data/z3-4.8.9/src/smt/seq_axioms.h
Examining data/z3-4.8.9/src/smt/seq_eq_solver.cpp
Examining data/z3-4.8.9/src/smt/seq_ne_solver.cpp
Examining data/z3-4.8.9/src/smt/seq_offset_eq.cpp
Examining data/z3-4.8.9/src/smt/seq_offset_eq.h
Examining data/z3-4.8.9/src/smt/seq_regex.cpp
Examining data/z3-4.8.9/src/smt/seq_regex.h
Examining data/z3-4.8.9/src/smt/seq_skolem.cpp
Examining data/z3-4.8.9/src/smt/seq_skolem.h
Examining data/z3-4.8.9/src/smt/seq_unicode.cpp
Examining data/z3-4.8.9/src/smt/seq_unicode.h
Examining data/z3-4.8.9/src/smt/smt2_extra_cmds.cpp
Examining data/z3-4.8.9/src/smt/smt2_extra_cmds.h
Examining data/z3-4.8.9/src/smt/smt_almost_cg_table.cpp
Examining data/z3-4.8.9/src/smt/smt_almost_cg_table.h
Examining data/z3-4.8.9/src/smt/smt_arith_value.cpp
Examining data/z3-4.8.9/src/smt/smt_arith_value.h
Examining data/z3-4.8.9/src/smt/smt_b_justification.h
Examining data/z3-4.8.9/src/smt/smt_bool_var_data.h
Examining data/z3-4.8.9/src/smt/smt_case_split_queue.cpp
Examining data/z3-4.8.9/src/smt/smt_case_split_queue.h
Examining data/z3-4.8.9/src/smt/smt_cg_table.cpp
Examining data/z3-4.8.9/src/smt/smt_cg_table.h
Examining data/z3-4.8.9/src/smt/smt_checker.cpp
Examining data/z3-4.8.9/src/smt/smt_checker.h
Examining data/z3-4.8.9/src/smt/smt_clause.cpp
Examining data/z3-4.8.9/src/smt/smt_clause.h
Examining data/z3-4.8.9/src/smt/smt_clause_proof.cpp
Examining data/z3-4.8.9/src/smt/smt_clause_proof.h
Examining data/z3-4.8.9/src/smt/smt_conflict_resolution.cpp
Examining data/z3-4.8.9/src/smt/smt_conflict_resolution.h
Examining data/z3-4.8.9/src/smt/smt_consequences.cpp
Examining data/z3-4.8.9/src/smt/smt_context.cpp
Examining data/z3-4.8.9/src/smt/smt_context.h
Examining data/z3-4.8.9/src/smt/smt_context_inv.cpp
Examining data/z3-4.8.9/src/smt/smt_context_pp.cpp
Examining data/z3-4.8.9/src/smt/smt_context_stat.cpp
Examining data/z3-4.8.9/src/smt/smt_enode.cpp
Examining data/z3-4.8.9/src/smt/smt_enode.h
Examining data/z3-4.8.9/src/smt/smt_eq_justification.h
Examining data/z3-4.8.9/src/smt/smt_failure.h
Examining data/z3-4.8.9/src/smt/smt_farkas_util.cpp
Examining data/z3-4.8.9/src/smt/smt_farkas_util.h
Examining data/z3-4.8.9/src/smt/smt_for_each_relevant_expr.cpp
Examining data/z3-4.8.9/src/smt/smt_for_each_relevant_expr.h
Examining data/z3-4.8.9/src/smt/smt_implied_equalities.cpp
Examining data/z3-4.8.9/src/smt/smt_implied_equalities.h
Examining data/z3-4.8.9/src/smt/smt_induction.cpp
Examining data/z3-4.8.9/src/smt/smt_induction.h
Examining data/z3-4.8.9/src/smt/smt_internalizer.cpp
Examining data/z3-4.8.9/src/smt/smt_justification.cpp
Examining data/z3-4.8.9/src/smt/smt_justification.h
Examining data/z3-4.8.9/src/smt/smt_kernel.cpp
Examining data/z3-4.8.9/src/smt/smt_kernel.h
Examining data/z3-4.8.9/src/smt/smt_literal.cpp
Examining data/z3-4.8.9/src/smt/smt_literal.h
Examining data/z3-4.8.9/src/smt/smt_lookahead.cpp
Examining data/z3-4.8.9/src/smt/smt_lookahead.h
Examining data/z3-4.8.9/src/smt/smt_model_checker.cpp
Examining data/z3-4.8.9/src/smt/smt_model_checker.h
Examining data/z3-4.8.9/src/smt/smt_model_finder.cpp
Examining data/z3-4.8.9/src/smt/smt_model_finder.h
Examining data/z3-4.8.9/src/smt/smt_model_generator.cpp
Examining data/z3-4.8.9/src/smt/smt_model_generator.h
Examining data/z3-4.8.9/src/smt/smt_parallel.cpp
Examining data/z3-4.8.9/src/smt/smt_parallel.h
Examining data/z3-4.8.9/src/smt/smt_quantifier.cpp
Examining data/z3-4.8.9/src/smt/smt_quantifier.h
Examining data/z3-4.8.9/src/smt/smt_quantifier_instances.h
Examining data/z3-4.8.9/src/smt/smt_quantifier_stat.cpp
Examining data/z3-4.8.9/src/smt/smt_quantifier_stat.h
Examining data/z3-4.8.9/src/smt/smt_quick_checker.cpp
Examining data/z3-4.8.9/src/smt/smt_quick_checker.h
Examining data/z3-4.8.9/src/smt/smt_relevancy.cpp
Examining data/z3-4.8.9/src/smt/smt_relevancy.h
Examining data/z3-4.8.9/src/smt/smt_setup.cpp
Examining data/z3-4.8.9/src/smt/smt_setup.h
Examining data/z3-4.8.9/src/smt/smt_solver.cpp
Examining data/z3-4.8.9/src/smt/smt_solver.h
Examining data/z3-4.8.9/src/smt/smt_statistics.cpp
Examining data/z3-4.8.9/src/smt/smt_statistics.h
Examining data/z3-4.8.9/src/smt/smt_theory.cpp
Examining data/z3-4.8.9/src/smt/smt_theory.h
Examining data/z3-4.8.9/src/smt/smt_types.h
Examining data/z3-4.8.9/src/smt/smt_value_sort.cpp
Examining data/z3-4.8.9/src/smt/smt_value_sort.h
Examining data/z3-4.8.9/src/smt/spanning_tree.h
Examining data/z3-4.8.9/src/smt/spanning_tree_base.h
Examining data/z3-4.8.9/src/smt/spanning_tree_def.h
Examining data/z3-4.8.9/src/smt/tactic/ctx_solver_simplify_tactic.cpp
Examining data/z3-4.8.9/src/smt/tactic/ctx_solver_simplify_tactic.h
Examining data/z3-4.8.9/src/smt/tactic/smt_tactic.cpp
Examining data/z3-4.8.9/src/smt/tactic/smt_tactic.h
Examining data/z3-4.8.9/src/smt/tactic/unit_subsumption_tactic.cpp
Examining data/z3-4.8.9/src/smt/tactic/unit_subsumption_tactic.h
Examining data/z3-4.8.9/src/smt/theory_arith.cpp
Examining data/z3-4.8.9/src/smt/theory_arith.h
Examining data/z3-4.8.9/src/smt/theory_arith_aux.h
Examining data/z3-4.8.9/src/smt/theory_arith_core.h
Examining data/z3-4.8.9/src/smt/theory_arith_def.h
Examining data/z3-4.8.9/src/smt/theory_arith_eq.h
Examining data/z3-4.8.9/src/smt/theory_arith_int.h
Examining data/z3-4.8.9/src/smt/theory_arith_inv.h
Examining data/z3-4.8.9/src/smt/theory_arith_nl.h
Examining data/z3-4.8.9/src/smt/theory_arith_pp.h
Examining data/z3-4.8.9/src/smt/theory_array.cpp
Examining data/z3-4.8.9/src/smt/theory_array.h
Examining data/z3-4.8.9/src/smt/theory_array_bapa.cpp
Examining data/z3-4.8.9/src/smt/theory_array_bapa.h
Examining data/z3-4.8.9/src/smt/theory_array_base.cpp
Examining data/z3-4.8.9/src/smt/theory_array_base.h
Examining data/z3-4.8.9/src/smt/theory_array_full.cpp
Examining data/z3-4.8.9/src/smt/theory_array_full.h
Examining data/z3-4.8.9/src/smt/theory_bv.cpp
Examining data/z3-4.8.9/src/smt/theory_bv.h
Examining data/z3-4.8.9/src/smt/theory_datatype.cpp
Examining data/z3-4.8.9/src/smt/theory_datatype.h
Examining data/z3-4.8.9/src/smt/theory_dense_diff_logic.cpp
Examining data/z3-4.8.9/src/smt/theory_dense_diff_logic.h
Examining data/z3-4.8.9/src/smt/theory_dense_diff_logic_def.h
Examining data/z3-4.8.9/src/smt/theory_diff_logic.cpp
Examining data/z3-4.8.9/src/smt/theory_diff_logic.h
Examining data/z3-4.8.9/src/smt/theory_diff_logic_def.h
Examining data/z3-4.8.9/src/smt/theory_dl.cpp
Examining data/z3-4.8.9/src/smt/theory_dl.h
Examining data/z3-4.8.9/src/smt/theory_dummy.cpp
Examining data/z3-4.8.9/src/smt/theory_dummy.h
Examining data/z3-4.8.9/src/smt/theory_fpa.cpp
Examining data/z3-4.8.9/src/smt/theory_fpa.h
Examining data/z3-4.8.9/src/smt/theory_lra.cpp
Examining data/z3-4.8.9/src/smt/theory_lra.h
Examining data/z3-4.8.9/src/smt/theory_opt.cpp
Examining data/z3-4.8.9/src/smt/theory_opt.h
Examining data/z3-4.8.9/src/smt/theory_pb.cpp
Examining data/z3-4.8.9/src/smt/theory_pb.h
Examining data/z3-4.8.9/src/smt/theory_recfun.cpp
Examining data/z3-4.8.9/src/smt/theory_recfun.h
Examining data/z3-4.8.9/src/smt/theory_seq.cpp
Examining data/z3-4.8.9/src/smt/theory_seq.h
Examining data/z3-4.8.9/src/smt/theory_seq_empty.h
Examining data/z3-4.8.9/src/smt/theory_special_relations.cpp
Examining data/z3-4.8.9/src/smt/theory_special_relations.h
Examining data/z3-4.8.9/src/smt/theory_str.cpp
Examining data/z3-4.8.9/src/smt/theory_str.h
Examining data/z3-4.8.9/src/smt/theory_str_mc.cpp
Examining data/z3-4.8.9/src/smt/theory_str_regex.cpp
Examining data/z3-4.8.9/src/smt/theory_utvpi.cpp
Examining data/z3-4.8.9/src/smt/theory_utvpi.h
Examining data/z3-4.8.9/src/smt/theory_utvpi_def.h
Examining data/z3-4.8.9/src/smt/theory_wmaxsat.cpp
Examining data/z3-4.8.9/src/smt/theory_wmaxsat.h
Examining data/z3-4.8.9/src/smt/user_propagator.cpp
Examining data/z3-4.8.9/src/smt/user_propagator.h
Examining data/z3-4.8.9/src/smt/uses_theory.cpp
Examining data/z3-4.8.9/src/smt/uses_theory.h
Examining data/z3-4.8.9/src/smt/watch_list.cpp
Examining data/z3-4.8.9/src/smt/watch_list.h
Examining data/z3-4.8.9/src/solver/check_sat_result.cpp
Examining data/z3-4.8.9/src/solver/check_sat_result.h
Examining data/z3-4.8.9/src/solver/combined_solver.cpp
Examining data/z3-4.8.9/src/solver/combined_solver.h
Examining data/z3-4.8.9/src/solver/mus.cpp
Examining data/z3-4.8.9/src/solver/mus.h
Examining data/z3-4.8.9/src/solver/parallel_tactic.cpp
Examining data/z3-4.8.9/src/solver/parallel_tactic.h
Examining data/z3-4.8.9/src/solver/progress_callback.h
Examining data/z3-4.8.9/src/solver/smt_logics.cpp
Examining data/z3-4.8.9/src/solver/smt_logics.h
Examining data/z3-4.8.9/src/solver/solver.cpp
Examining data/z3-4.8.9/src/solver/solver.h
Examining data/z3-4.8.9/src/solver/solver2tactic.cpp
Examining data/z3-4.8.9/src/solver/solver2tactic.h
Examining data/z3-4.8.9/src/solver/solver_na2as.cpp
Examining data/z3-4.8.9/src/solver/solver_na2as.h
Examining data/z3-4.8.9/src/solver/solver_pool.cpp
Examining data/z3-4.8.9/src/solver/solver_pool.h
Examining data/z3-4.8.9/src/solver/tactic2solver.cpp
Examining data/z3-4.8.9/src/solver/tactic2solver.h
Examining data/z3-4.8.9/src/tactic/aig/aig.cpp
Examining data/z3-4.8.9/src/tactic/aig/aig.h
Examining data/z3-4.8.9/src/tactic/aig/aig_tactic.cpp
Examining data/z3-4.8.9/src/tactic/aig/aig_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/add_bounds_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/add_bounds_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/arith_bounds_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/arith_bounds_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/bound_manager.cpp
Examining data/z3-4.8.9/src/tactic/arith/bound_manager.h
Examining data/z3-4.8.9/src/tactic/arith/bound_propagator.cpp
Examining data/z3-4.8.9/src/tactic/arith/bound_propagator.h
Examining data/z3-4.8.9/src/tactic/arith/bv2int_rewriter.cpp
Examining data/z3-4.8.9/src/tactic/arith/bv2int_rewriter.h
Examining data/z3-4.8.9/src/tactic/arith/bv2real_rewriter.cpp
Examining data/z3-4.8.9/src/tactic/arith/bv2real_rewriter.h
Examining data/z3-4.8.9/src/tactic/arith/card2bv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/card2bv_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/degree_shift_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/degree_shift_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/diff_neq_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/diff_neq_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/eq2bv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/eq2bv_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/factor_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/factor_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/fix_dl_var_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/fix_dl_var_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/fm_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/fm_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/lia2card_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/lia2card_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/lia2pb_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/lia2pb_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/linear_equation.cpp
Examining data/z3-4.8.9/src/tactic/arith/linear_equation.h
Examining data/z3-4.8.9/src/tactic/arith/nla2bv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/nla2bv_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/normalize_bounds_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/normalize_bounds_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/pb2bv_model_converter.cpp
Examining data/z3-4.8.9/src/tactic/arith/pb2bv_model_converter.h
Examining data/z3-4.8.9/src/tactic/arith/pb2bv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/pb2bv_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/probe_arith.cpp
Examining data/z3-4.8.9/src/tactic/arith/probe_arith.h
Examining data/z3-4.8.9/src/tactic/arith/propagate_ineqs_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/propagate_ineqs_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/purify_arith_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/purify_arith_tactic.h
Examining data/z3-4.8.9/src/tactic/arith/recover_01_tactic.cpp
Examining data/z3-4.8.9/src/tactic/arith/recover_01_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/bit_blaster_model_converter.cpp
Examining data/z3-4.8.9/src/tactic/bv/bit_blaster_model_converter.h
Examining data/z3-4.8.9/src/tactic/bv/bit_blaster_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/bit_blaster_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/bv1_blaster_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/bv1_blaster_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/bv_bound_chk_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/bv_bound_chk_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/bv_bounds_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/bv_bounds_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/bv_size_reduction_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/bv_size_reduction_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/bvarray2uf_rewriter.cpp
Examining data/z3-4.8.9/src/tactic/bv/bvarray2uf_rewriter.h
Examining data/z3-4.8.9/src/tactic/bv/bvarray2uf_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/bvarray2uf_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/dt2bv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/dt2bv_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/elim_small_bv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/elim_small_bv_tactic.h
Examining data/z3-4.8.9/src/tactic/bv/max_bv_sharing_tactic.cpp
Examining data/z3-4.8.9/src/tactic/bv/max_bv_sharing_tactic.h
Examining data/z3-4.8.9/src/tactic/converter.h
Examining data/z3-4.8.9/src/tactic/core/blast_term_ite_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/blast_term_ite_tactic.h
Examining data/z3-4.8.9/src/tactic/core/cofactor_elim_term_ite.cpp
Examining data/z3-4.8.9/src/tactic/core/cofactor_elim_term_ite.h
Examining data/z3-4.8.9/src/tactic/core/cofactor_term_ite_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/cofactor_term_ite_tactic.h
Examining data/z3-4.8.9/src/tactic/core/collect_occs.cpp
Examining data/z3-4.8.9/src/tactic/core/collect_occs.h
Examining data/z3-4.8.9/src/tactic/core/collect_statistics_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/collect_statistics_tactic.h
Examining data/z3-4.8.9/src/tactic/core/ctx_simplify_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/ctx_simplify_tactic.h
Examining data/z3-4.8.9/src/tactic/core/der_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/der_tactic.h
Examining data/z3-4.8.9/src/tactic/core/distribute_forall_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/distribute_forall_tactic.h
Examining data/z3-4.8.9/src/tactic/core/dom_simplify_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/dom_simplify_tactic.h
Examining data/z3-4.8.9/src/tactic/core/elim_term_ite_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/elim_term_ite_tactic.h
Examining data/z3-4.8.9/src/tactic/core/elim_uncnstr_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/elim_uncnstr_tactic.h
Examining data/z3-4.8.9/src/tactic/core/injectivity_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/injectivity_tactic.h
Examining data/z3-4.8.9/src/tactic/core/nnf_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/nnf_tactic.h
Examining data/z3-4.8.9/src/tactic/core/occf_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/occf_tactic.h
Examining data/z3-4.8.9/src/tactic/core/pb_preprocess_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/pb_preprocess_tactic.h
Examining data/z3-4.8.9/src/tactic/core/propagate_values_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/propagate_values_tactic.h
Examining data/z3-4.8.9/src/tactic/core/reduce_args_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/reduce_args_tactic.h
Examining data/z3-4.8.9/src/tactic/core/reduce_invertible_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/reduce_invertible_tactic.h
Examining data/z3-4.8.9/src/tactic/core/simplify_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/simplify_tactic.h
Examining data/z3-4.8.9/src/tactic/core/solve_eqs_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/solve_eqs_tactic.h
Examining data/z3-4.8.9/src/tactic/core/special_relations_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/special_relations_tactic.h
Examining data/z3-4.8.9/src/tactic/core/split_clause_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/split_clause_tactic.h
Examining data/z3-4.8.9/src/tactic/core/symmetry_reduce_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/symmetry_reduce_tactic.h
Examining data/z3-4.8.9/src/tactic/core/tseitin_cnf_tactic.cpp
Examining data/z3-4.8.9/src/tactic/core/tseitin_cnf_tactic.h
Examining data/z3-4.8.9/src/tactic/dependency_converter.cpp
Examining data/z3-4.8.9/src/tactic/dependency_converter.h
Examining data/z3-4.8.9/src/tactic/equiv_proof_converter.cpp
Examining data/z3-4.8.9/src/tactic/equiv_proof_converter.h
Examining data/z3-4.8.9/src/tactic/fd_solver/bounded_int2bv_solver.cpp
Examining data/z3-4.8.9/src/tactic/fd_solver/bounded_int2bv_solver.h
Examining data/z3-4.8.9/src/tactic/fd_solver/enum2bv_solver.cpp
Examining data/z3-4.8.9/src/tactic/fd_solver/enum2bv_solver.h
Examining data/z3-4.8.9/src/tactic/fd_solver/fd_solver.cpp
Examining data/z3-4.8.9/src/tactic/fd_solver/fd_solver.h
Examining data/z3-4.8.9/src/tactic/fd_solver/pb2bv_solver.cpp
Examining data/z3-4.8.9/src/tactic/fd_solver/pb2bv_solver.h
Examining data/z3-4.8.9/src/tactic/fd_solver/smtfd_solver.cpp
Examining data/z3-4.8.9/src/tactic/fd_solver/smtfd_solver.h
Examining data/z3-4.8.9/src/tactic/filter_model_converter.h
Examining data/z3-4.8.9/src/tactic/fpa/fpa2bv_model_converter.cpp
Examining data/z3-4.8.9/src/tactic/fpa/fpa2bv_model_converter.h
Examining data/z3-4.8.9/src/tactic/fpa/fpa2bv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/fpa/fpa2bv_tactic.h
Examining data/z3-4.8.9/src/tactic/fpa/qffp_tactic.cpp
Examining data/z3-4.8.9/src/tactic/fpa/qffp_tactic.h
Examining data/z3-4.8.9/src/tactic/fpa/qffplra_tactic.cpp
Examining data/z3-4.8.9/src/tactic/fpa/qffplra_tactic.h
Examining data/z3-4.8.9/src/tactic/generic_model_converter.cpp
Examining data/z3-4.8.9/src/tactic/generic_model_converter.h
Examining data/z3-4.8.9/src/tactic/goal.cpp
Examining data/z3-4.8.9/src/tactic/goal.h
Examining data/z3-4.8.9/src/tactic/goal_num_occurs.cpp
Examining data/z3-4.8.9/src/tactic/goal_num_occurs.h
Examining data/z3-4.8.9/src/tactic/goal_shared_occs.cpp
Examining data/z3-4.8.9/src/tactic/goal_shared_occs.h
Examining data/z3-4.8.9/src/tactic/goal_util.cpp
Examining data/z3-4.8.9/src/tactic/goal_util.h
Examining data/z3-4.8.9/src/tactic/horn_subsume_model_converter.cpp
Examining data/z3-4.8.9/src/tactic/horn_subsume_model_converter.h
Examining data/z3-4.8.9/src/tactic/model_converter.cpp
Examining data/z3-4.8.9/src/tactic/model_converter.h
Examining data/z3-4.8.9/src/tactic/portfolio/default_tactic.cpp
Examining data/z3-4.8.9/src/tactic/portfolio/default_tactic.h
Examining data/z3-4.8.9/src/tactic/portfolio/smt_strategic_solver.cpp
Examining data/z3-4.8.9/src/tactic/portfolio/solver2lookahead.cpp
Examining data/z3-4.8.9/src/tactic/portfolio/solver2lookahead.h
Examining data/z3-4.8.9/src/tactic/probe.cpp
Examining data/z3-4.8.9/src/tactic/probe.h
Examining data/z3-4.8.9/src/tactic/proof_converter.cpp
Examining data/z3-4.8.9/src/tactic/proof_converter.h
Examining data/z3-4.8.9/src/tactic/replace_proof_converter.cpp
Examining data/z3-4.8.9/src/tactic/replace_proof_converter.h
Examining data/z3-4.8.9/src/tactic/sine_filter.cpp
Examining data/z3-4.8.9/src/tactic/sine_filter.h
Examining data/z3-4.8.9/src/tactic/sls/bvsls_opt_engine.cpp
Examining data/z3-4.8.9/src/tactic/sls/bvsls_opt_engine.h
Examining data/z3-4.8.9/src/tactic/sls/sls_engine.cpp
Examining data/z3-4.8.9/src/tactic/sls/sls_engine.h
Examining data/z3-4.8.9/src/tactic/sls/sls_evaluator.h
Examining data/z3-4.8.9/src/tactic/sls/sls_powers.h
Examining data/z3-4.8.9/src/tactic/sls/sls_tactic.cpp
Examining data/z3-4.8.9/src/tactic/sls/sls_tactic.h
Examining data/z3-4.8.9/src/tactic/sls/sls_tracker.h
Examining data/z3-4.8.9/src/tactic/smtlogics/nra_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/nra_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfaufbv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfaufbv_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfauflia_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfauflia_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfbv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfbv_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfidl_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfidl_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qflia_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qflia_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qflra_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qflra_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfnia_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfnia_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfnra_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfnra_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfuf_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfuf_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfufbv_ackr_model_converter.h
Examining data/z3-4.8.9/src/tactic/smtlogics/qfufbv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/qfufbv_tactic.h
Examining data/z3-4.8.9/src/tactic/smtlogics/quant_tactics.cpp
Examining data/z3-4.8.9/src/tactic/smtlogics/quant_tactics.h
Examining data/z3-4.8.9/src/tactic/tactic.cpp
Examining data/z3-4.8.9/src/tactic/tactic.h
Examining data/z3-4.8.9/src/tactic/tactic_exception.h
Examining data/z3-4.8.9/src/tactic/tactical.cpp
Examining data/z3-4.8.9/src/tactic/tactical.h
Examining data/z3-4.8.9/src/tactic/ufbv/macro_finder_tactic.cpp
Examining data/z3-4.8.9/src/tactic/ufbv/macro_finder_tactic.h
Examining data/z3-4.8.9/src/tactic/ufbv/quasi_macros_tactic.cpp
Examining data/z3-4.8.9/src/tactic/ufbv/quasi_macros_tactic.h
Examining data/z3-4.8.9/src/tactic/ufbv/ufbv_rewriter.cpp
Examining data/z3-4.8.9/src/tactic/ufbv/ufbv_rewriter.h
Examining data/z3-4.8.9/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
Examining data/z3-4.8.9/src/tactic/ufbv/ufbv_rewriter_tactic.h
Examining data/z3-4.8.9/src/tactic/ufbv/ufbv_tactic.cpp
Examining data/z3-4.8.9/src/tactic/ufbv/ufbv_tactic.h
Examining data/z3-4.8.9/src/test/algebraic.cpp
Examining data/z3-4.8.9/src/test/api.cpp
Examining data/z3-4.8.9/src/test/api_bug.cpp
Examining data/z3-4.8.9/src/test/arith_rewriter.cpp
Examining data/z3-4.8.9/src/test/arith_simplifier_plugin.cpp
Examining data/z3-4.8.9/src/test/ast.cpp
Examining data/z3-4.8.9/src/test/bdd.cpp
Examining data/z3-4.8.9/src/test/bit_blaster.cpp
Examining data/z3-4.8.9/src/test/bit_vector.cpp
Examining data/z3-4.8.9/src/test/bits.cpp
Examining data/z3-4.8.9/src/test/buffer.cpp
Examining data/z3-4.8.9/src/test/chashtable.cpp
Examining data/z3-4.8.9/src/test/check_assumptions.cpp
Examining data/z3-4.8.9/src/test/cnf_backbones.cpp
Examining data/z3-4.8.9/src/test/cube_clause.cpp
Examining data/z3-4.8.9/src/test/datalog_parser.cpp
Examining data/z3-4.8.9/src/test/ddnf.cpp
Examining data/z3-4.8.9/src/test/diff_logic.cpp
Examining data/z3-4.8.9/src/test/dl_context.cpp
Examining data/z3-4.8.9/src/test/dl_product_relation.cpp
Examining data/z3-4.8.9/src/test/dl_query.cpp
Examining data/z3-4.8.9/src/test/dl_relation.cpp
Examining data/z3-4.8.9/src/test/dl_table.cpp
Examining data/z3-4.8.9/src/test/dl_util.cpp
Examining data/z3-4.8.9/src/test/doc.cpp
Examining data/z3-4.8.9/src/test/egraph.cpp
Examining data/z3-4.8.9/src/test/escaped.cpp
Examining data/z3-4.8.9/src/test/ex.cpp
Examining data/z3-4.8.9/src/test/expr_rand.cpp
Examining data/z3-4.8.9/src/test/expr_substitution.cpp
Examining data/z3-4.8.9/src/test/ext_numeral.cpp
Examining data/z3-4.8.9/src/test/f2n.cpp
Examining data/z3-4.8.9/src/test/factor_rewriter.cpp
Examining data/z3-4.8.9/src/test/finder.cpp
Examining data/z3-4.8.9/src/test/fixed_bit_vector.cpp
Examining data/z3-4.8.9/src/test/for_each_file.cpp
Examining data/z3-4.8.9/src/test/for_each_file.h
Examining data/z3-4.8.9/src/test/fuzzing/expr_delta.cpp
Examining data/z3-4.8.9/src/test/fuzzing/expr_delta.h
Examining data/z3-4.8.9/src/test/fuzzing/expr_rand.cpp
Examining data/z3-4.8.9/src/test/fuzzing/expr_rand.h
Examining data/z3-4.8.9/src/test/get_consequences.cpp
Examining data/z3-4.8.9/src/test/get_implied_equalities.cpp
Examining data/z3-4.8.9/src/test/hashtable.cpp
Examining data/z3-4.8.9/src/test/heap.cpp
Examining data/z3-4.8.9/src/test/heap_trie.cpp
Examining data/z3-4.8.9/src/test/hilbert_basis.cpp
Examining data/z3-4.8.9/src/test/horn_subsume_model_converter.cpp
Examining data/z3-4.8.9/src/test/hwf.cpp
Examining data/z3-4.8.9/src/test/im_float_config.h
Examining data/z3-4.8.9/src/test/inf_rational.cpp
Examining data/z3-4.8.9/src/test/interval.cpp
Examining data/z3-4.8.9/src/test/karr.cpp
Examining data/z3-4.8.9/src/test/list.cpp
Examining data/z3-4.8.9/src/test/lp/argument_parser.h
Examining data/z3-4.8.9/src/test/lp/gomory_test.h
Examining data/z3-4.8.9/src/test/lp/lp.cpp
Examining data/z3-4.8.9/src/test/lp/lp_main.cpp
Examining data/z3-4.8.9/src/test/lp/nla_solver_test.cpp
Examining data/z3-4.8.9/src/test/lp/smt_reader.h
Examining data/z3-4.8.9/src/test/lp/test_file_reader.h
Examining data/z3-4.8.9/src/test/main.cpp
Examining data/z3-4.8.9/src/test/map.cpp
Examining data/z3-4.8.9/src/test/matcher.cpp
Examining data/z3-4.8.9/src/test/memory.cpp
Examining data/z3-4.8.9/src/test/model2expr.cpp
Examining data/z3-4.8.9/src/test/model_based_opt.cpp
Examining data/z3-4.8.9/src/test/model_evaluator.cpp
Examining data/z3-4.8.9/src/test/model_retrieval.cpp
Examining data/z3-4.8.9/src/test/mpbq.cpp
Examining data/z3-4.8.9/src/test/mpf.cpp
Examining data/z3-4.8.9/src/test/mpff.cpp
Examining data/z3-4.8.9/src/test/mpfx.cpp
Examining data/z3-4.8.9/src/test/mpq.cpp
Examining data/z3-4.8.9/src/test/mpz.cpp
Examining data/z3-4.8.9/src/test/nlarith_util.cpp
Examining data/z3-4.8.9/src/test/nlsat.cpp
Examining data/z3-4.8.9/src/test/no_overflow.cpp
Examining data/z3-4.8.9/src/test/object_allocator.cpp
Examining data/z3-4.8.9/src/test/old_interval.cpp
Examining data/z3-4.8.9/src/test/optional.cpp
Examining data/z3-4.8.9/src/test/parray.cpp
Examining data/z3-4.8.9/src/test/pb2bv.cpp
Examining data/z3-4.8.9/src/test/pdd.cpp
Examining data/z3-4.8.9/src/test/pdd_solver.cpp
Examining data/z3-4.8.9/src/test/permutation.cpp
Examining data/z3-4.8.9/src/test/polynomial.cpp
Examining data/z3-4.8.9/src/test/polynorm.cpp
Examining data/z3-4.8.9/src/test/prime_generator.cpp
Examining data/z3-4.8.9/src/test/proof_checker.cpp
Examining data/z3-4.8.9/src/test/qe_arith.cpp
Examining data/z3-4.8.9/src/test/quant_elim.cpp
Examining data/z3-4.8.9/src/test/quant_solve.cpp
Examining data/z3-4.8.9/src/test/random.cpp
Examining data/z3-4.8.9/src/test/rational.cpp
Examining data/z3-4.8.9/src/test/rcf.cpp
Examining data/z3-4.8.9/src/test/region.cpp
Examining data/z3-4.8.9/src/test/sat_local_search.cpp
Examining data/z3-4.8.9/src/test/sat_lookahead.cpp
Examining data/z3-4.8.9/src/test/sat_user_scope.cpp
Examining data/z3-4.8.9/src/test/simple_parser.cpp
Examining data/z3-4.8.9/src/test/simplex.cpp
Examining data/z3-4.8.9/src/test/simplifier.cpp
Examining data/z3-4.8.9/src/test/small_object_allocator.cpp
Examining data/z3-4.8.9/src/test/smt2print_parse.cpp
Examining data/z3-4.8.9/src/test/smt_context.cpp
Examining data/z3-4.8.9/src/test/solver_pool.cpp
Examining data/z3-4.8.9/src/test/sorting_network.cpp
Examining data/z3-4.8.9/src/test/stack.cpp
Examining data/z3-4.8.9/src/test/string_buffer.cpp
Examining data/z3-4.8.9/src/test/substitution.cpp
Examining data/z3-4.8.9/src/test/symbol.cpp
Examining data/z3-4.8.9/src/test/symbol_table.cpp
Examining data/z3-4.8.9/src/test/tbv.cpp
Examining data/z3-4.8.9/src/test/test_util.h
Examining data/z3-4.8.9/src/test/theory_dl.cpp
Examining data/z3-4.8.9/src/test/theory_pb.cpp
Examining data/z3-4.8.9/src/test/timeout.cpp
Examining data/z3-4.8.9/src/test/total_order.cpp
Examining data/z3-4.8.9/src/test/trigo.cpp
Examining data/z3-4.8.9/src/test/udoc_relation.cpp
Examining data/z3-4.8.9/src/test/uint_set.cpp
Examining data/z3-4.8.9/src/test/upolynomial.cpp
Examining data/z3-4.8.9/src/test/value_generator.cpp
Examining data/z3-4.8.9/src/test/value_sweep.cpp
Examining data/z3-4.8.9/src/test/var_subst.cpp
Examining data/z3-4.8.9/src/test/vector.cpp
Examining data/z3-4.8.9/src/util/approx_nat.cpp
Examining data/z3-4.8.9/src/util/approx_nat.h
Examining data/z3-4.8.9/src/util/approx_set.cpp
Examining data/z3-4.8.9/src/util/approx_set.h
Examining data/z3-4.8.9/src/util/array.h
Examining data/z3-4.8.9/src/util/array_map.h
Examining data/z3-4.8.9/src/util/backtrackable_set.h
Examining data/z3-4.8.9/src/util/basic_interval.h
Examining data/z3-4.8.9/src/util/bit_util.cpp
Examining data/z3-4.8.9/src/util/bit_util.h
Examining data/z3-4.8.9/src/util/bit_vector.cpp
Examining data/z3-4.8.9/src/util/bit_vector.h
Examining data/z3-4.8.9/src/util/buffer.h
Examining data/z3-4.8.9/src/util/cancel_eh.h
Examining data/z3-4.8.9/src/util/chashtable.h
Examining data/z3-4.8.9/src/util/checked_int64.h
Examining data/z3-4.8.9/src/util/cmd_context_types.cpp
Examining data/z3-4.8.9/src/util/cmd_context_types.h
Examining data/z3-4.8.9/src/util/common_msgs.cpp
Examining data/z3-4.8.9/src/util/common_msgs.h
Examining data/z3-4.8.9/src/util/container_util.h
Examining data/z3-4.8.9/src/util/debug.cpp
Examining data/z3-4.8.9/src/util/debug.h
Examining data/z3-4.8.9/src/util/dec_ref_util.h
Examining data/z3-4.8.9/src/util/dependency.h
Examining data/z3-4.8.9/src/util/dictionary.h
Examining data/z3-4.8.9/src/util/dlist.h
Examining data/z3-4.8.9/src/util/double_manager.h
Examining data/z3-4.8.9/src/util/ema.h
Examining data/z3-4.8.9/src/util/env_params.cpp
Examining data/z3-4.8.9/src/util/env_params.h
Examining data/z3-4.8.9/src/util/error_codes.h
Examining data/z3-4.8.9/src/util/event_handler.h
Examining data/z3-4.8.9/src/util/ext_gcd.h
Examining data/z3-4.8.9/src/util/ext_numeral.h
Examining data/z3-4.8.9/src/util/f2n.h
Examining data/z3-4.8.9/src/util/file_path.h
Examining data/z3-4.8.9/src/util/fixed_bit_vector.cpp
Examining data/z3-4.8.9/src/util/fixed_bit_vector.h
Examining data/z3-4.8.9/src/util/gparams.cpp
Examining data/z3-4.8.9/src/util/gparams.h
Examining data/z3-4.8.9/src/util/hash.cpp
Examining data/z3-4.8.9/src/util/hash.h
Examining data/z3-4.8.9/src/util/hashtable.h
Examining data/z3-4.8.9/src/util/heap.h
Examining data/z3-4.8.9/src/util/hwf.h
Examining data/z3-4.8.9/src/util/id_gen.h
Examining data/z3-4.8.9/src/util/id_var_list.h
Examining data/z3-4.8.9/src/util/inf_eps_rational.h
Examining data/z3-4.8.9/src/util/inf_int_rational.cpp
Examining data/z3-4.8.9/src/util/inf_int_rational.h
Examining data/z3-4.8.9/src/util/inf_rational.cpp
Examining data/z3-4.8.9/src/util/inf_rational.h
Examining data/z3-4.8.9/src/util/inf_s_integer.cpp
Examining data/z3-4.8.9/src/util/inf_s_integer.h
Examining data/z3-4.8.9/src/util/lbool.cpp
Examining data/z3-4.8.9/src/util/lbool.h
Examining data/z3-4.8.9/src/util/list.h
Examining data/z3-4.8.9/src/util/luby.cpp
Examining data/z3-4.8.9/src/util/luby.h
Examining data/z3-4.8.9/src/util/machine.h
Examining data/z3-4.8.9/src/util/map.h
Examining data/z3-4.8.9/src/util/max_cliques.h
Examining data/z3-4.8.9/src/util/memory_manager.cpp
Examining data/z3-4.8.9/src/util/memory_manager.h
Examining data/z3-4.8.9/src/util/min_cut.cpp
Examining data/z3-4.8.9/src/util/min_cut.h
Examining data/z3-4.8.9/src/util/mpbq.cpp
Examining data/z3-4.8.9/src/util/mpbq.h
Examining data/z3-4.8.9/src/util/mpbqi.h
Examining data/z3-4.8.9/src/util/mpf.cpp
Examining data/z3-4.8.9/src/util/mpf.h
Examining data/z3-4.8.9/src/util/mpff.cpp
Examining data/z3-4.8.9/src/util/mpff.h
Examining data/z3-4.8.9/src/util/mpfx.cpp
Examining data/z3-4.8.9/src/util/mpfx.h
Examining data/z3-4.8.9/src/util/mpn.cpp
Examining data/z3-4.8.9/src/util/mpn.h
Examining data/z3-4.8.9/src/util/mpq.cpp
Examining data/z3-4.8.9/src/util/mpq.h
Examining data/z3-4.8.9/src/util/mpq_inf.cpp
Examining data/z3-4.8.9/src/util/mpq_inf.h
Examining data/z3-4.8.9/src/util/mpz.h
Examining data/z3-4.8.9/src/util/mpzzp.h
Examining data/z3-4.8.9/src/util/mutex.h
Examining data/z3-4.8.9/src/util/nat_set.h
Examining data/z3-4.8.9/src/util/numeral_buffer.h
Examining data/z3-4.8.9/src/util/obj_hashtable.h
Examining data/z3-4.8.9/src/util/obj_mark.h
Examining data/z3-4.8.9/src/util/obj_pair_hashtable.h
Examining data/z3-4.8.9/src/util/obj_pair_set.h
Examining data/z3-4.8.9/src/util/obj_ref.h
Examining data/z3-4.8.9/src/util/obj_ref_hashtable.h
Examining data/z3-4.8.9/src/util/obj_triple_hashtable.h
Examining data/z3-4.8.9/src/util/object_allocator.h
Examining data/z3-4.8.9/src/util/optional.h
Examining data/z3-4.8.9/src/util/page.cpp
Examining data/z3-4.8.9/src/util/page.h
Examining data/z3-4.8.9/src/util/params.cpp
Examining data/z3-4.8.9/src/util/params.h
Examining data/z3-4.8.9/src/util/parray.h
Examining data/z3-4.8.9/src/util/permutation.cpp
Examining data/z3-4.8.9/src/util/permutation.h
Examining data/z3-4.8.9/src/util/plugin_manager.h
Examining data/z3-4.8.9/src/util/pool.h
Examining data/z3-4.8.9/src/util/prime_generator.cpp
Examining data/z3-4.8.9/src/util/prime_generator.h
Examining data/z3-4.8.9/src/util/ptr_scoped_buffer.h
Examining data/z3-4.8.9/src/util/queue.h
Examining data/z3-4.8.9/src/util/rational.cpp
Examining data/z3-4.8.9/src/util/rational.h
Examining data/z3-4.8.9/src/util/ref.h
Examining data/z3-4.8.9/src/util/ref_buffer.h
Examining data/z3-4.8.9/src/util/ref_pair_vector.h
Examining data/z3-4.8.9/src/util/ref_util.h
Examining data/z3-4.8.9/src/util/ref_vector.h
Examining data/z3-4.8.9/src/util/region.cpp
Examining data/z3-4.8.9/src/util/region.h
Examining data/z3-4.8.9/src/util/rlimit.cpp
Examining data/z3-4.8.9/src/util/rlimit.h
Examining data/z3-4.8.9/src/util/s_integer.cpp
Examining data/z3-4.8.9/src/util/s_integer.h
Examining data/z3-4.8.9/src/util/scoped_ctrl_c.cpp
Examining data/z3-4.8.9/src/util/scoped_ctrl_c.h
Examining data/z3-4.8.9/src/util/scoped_limit_trail.h
Examining data/z3-4.8.9/src/util/scoped_numeral.h
Examining data/z3-4.8.9/src/util/scoped_numeral_buffer.h
Examining data/z3-4.8.9/src/util/scoped_numeral_vector.h
Examining data/z3-4.8.9/src/util/scoped_ptr_vector.h
Examining data/z3-4.8.9/src/util/scoped_timer.cpp
Examining data/z3-4.8.9/src/util/scoped_timer.h
Examining data/z3-4.8.9/src/util/scoped_vector.h
Examining data/z3-4.8.9/src/util/sexpr.cpp
Examining data/z3-4.8.9/src/util/sexpr.h
Examining data/z3-4.8.9/src/util/sign.h
Examining data/z3-4.8.9/src/util/small_object_allocator.cpp
Examining data/z3-4.8.9/src/util/small_object_allocator.h
Examining data/z3-4.8.9/src/util/smt2_util.cpp
Examining data/z3-4.8.9/src/util/smt2_util.h
Examining data/z3-4.8.9/src/util/sorting_network.h
Examining data/z3-4.8.9/src/util/sstream.h
Examining data/z3-4.8.9/src/util/stack.cpp
Examining data/z3-4.8.9/src/util/stack.h
Examining data/z3-4.8.9/src/util/stacked_value.h
Examining data/z3-4.8.9/src/util/state_graph.cpp
Examining data/z3-4.8.9/src/util/state_graph.h
Examining data/z3-4.8.9/src/util/statistics.cpp
Examining data/z3-4.8.9/src/util/statistics.h
Examining data/z3-4.8.9/src/util/stats.h
Examining data/z3-4.8.9/src/util/stopwatch.h
Examining data/z3-4.8.9/src/util/str_hashtable.h
Examining data/z3-4.8.9/src/util/stream_buffer.h
Examining data/z3-4.8.9/src/util/string_buffer.h
Examining data/z3-4.8.9/src/util/symbol.cpp
Examining data/z3-4.8.9/src/util/symbol.h
Examining data/z3-4.8.9/src/util/symbol_table.h
Examining data/z3-4.8.9/src/util/timeit.cpp
Examining data/z3-4.8.9/src/util/timeit.h
Examining data/z3-4.8.9/src/util/timeout.cpp
Examining data/z3-4.8.9/src/util/timeout.h
Examining data/z3-4.8.9/src/util/timer.h
Examining data/z3-4.8.9/src/util/top_sort.h
Examining data/z3-4.8.9/src/util/total_order.h
Examining data/z3-4.8.9/src/util/tptr.h
Examining data/z3-4.8.9/src/util/trace.cpp
Examining data/z3-4.8.9/src/util/trace.h
Examining data/z3-4.8.9/src/util/trail.h
Examining data/z3-4.8.9/src/util/uint_map.h
Examining data/z3-4.8.9/src/util/uint_set.h
Examining data/z3-4.8.9/src/util/union_find.h
Examining data/z3-4.8.9/src/util/util.cpp
Examining data/z3-4.8.9/src/util/util.h
Examining data/z3-4.8.9/src/util/vector.h
Examining data/z3-4.8.9/src/util/warning.cpp
Examining data/z3-4.8.9/src/util/warning.h
Examining data/z3-4.8.9/src/util/z3_exception.cpp
Examining data/z3-4.8.9/src/util/z3_exception.h
Examining data/z3-4.8.9/src/util/hwf.cpp
Examining data/z3-4.8.9/src/util/mpz.cpp

FINAL RESULTS:

data/z3-4.8.9/examples/tptp/tptp5.tab.c:1587:21:  [4] (format) fprintf:
  If format strings can be influenced by an attacker, they can be exploited
  (CWE-134). Use a constant for the format specification.
#  define YYFPRINTF fprintf
data/z3-4.8.9/src/muz/base/dl_util.cpp:636:25:  [4] (buffer) sscanf:
  The scanf() family's %s operation, without a limit specification, permits
  buffer overflows (CWE-120, CWE-20). Specify a limit to %s, or use a
  different input function. If the scanf format is influenceable by an
  attacker, it's exploitable.
        int converted = sscanf(s, "%" SCNu64, &res);
data/z3-4.8.9/src/muz/rel/dl_product_relation.cpp:403:30:  [4] (race) access:
  This usually indicates a security flaw. If an attacker can change anything
  along the path between the call to access() and the file's actual use
  (e.g., by moving files), the attacker can exploit the race condition
  (CWE-362/CWE-367!). Set up the correct permissions (e.g., using setuid())
  and try to open the file directly.
        relation_base const& access(unsigned idx, relation_base const& r) {
data/z3-4.8.9/src/muz/rel/dl_product_relation.cpp:458:90:  [4] (race) access:
  This usually indicates a security flaw. If an attacker can change anything
  along the path between the call to access() and the file's actual use
  (e.g., by moving files), the attacker can exploit the race condition
  (CWE-362/CWE-367!). Set up the correct permissions (e.g., using setuid())
  and try to open the file directly.
                relation_base const& r1 = (m_kind1[i] == T_FULL)?(*m_full[m_offset1[i]]):access(m_offset1[i], _r1);
data/z3-4.8.9/src/muz/rel/dl_product_relation.cpp:459:90:  [4] (race) access:
  This usually indicates a security flaw. If an attacker can change anything
  along the path between the call to access() and the file's actual use
  (e.g., by moving files), the attacker can exploit the race condition
  (CWE-362/CWE-367!). Set up the correct permissions (e.g., using setuid())
  and try to open the file directly.
                relation_base const& r2 = (m_kind2[i] == T_FULL)?(*m_full[m_offset2[i]]):access(m_offset2[i], _r2);
data/z3-4.8.9/src/qe/qe_datatypes.cpp:166:25:  [4] (race) access:
  This usually indicates a security flaw. If an attacker can change anything
  along the path between the call to access() and the file's actual use
  (e.g., by moving files), the attacker can exploit the race condition
  (CWE-362/CWE-367!). Set up the correct permissions (e.g., using setuid())
  and try to open the file directly.
                    r = access(c, i, acc, b);
data/z3-4.8.9/src/qe/qe_datatypes.cpp:170:55:  [4] (race) access:
  This usually indicates a security flaw. If an attacker can change anything
  along the path between the call to access() and the file's actual use
  (e.g., by moving files), the attacker can exploit the race condition
  (CWE-362/CWE-367!). Set up the correct permissions (e.g., using setuid())
  and try to open the file directly.
                                eqs.push_back(m.mk_eq(access(c, j, acc, b), a->get_arg(j)));
data/z3-4.8.9/src/qe/qe_datatypes.cpp:185:15:  [4] (race) access:
  This usually indicates a security flaw. If an attacker can change anything
  along the path between the call to access() and the file's actual use
  (e.g., by moving files), the attacker can exploit the race condition
  (CWE-362/CWE-367!). Set up the correct permissions (e.g., using setuid())
  and try to open the file directly.
        expr* access(func_decl* c, unsigned i, ptr_vector<func_decl> const& acc, expr* e) {
data/z3-4.8.9/src/qe/qe_datatypes.cpp:239:63:  [4] (race) access:
  This usually indicates a security flaw. If an attacker can change anything
  along the path between the call to access() and the file's actual use
  (e.g., by moving files), the attacker can exploit the race condition
  (CWE-362/CWE-367!). Set up the correct permissions (e.g., using setuid())
  and try to open the file directly.
                lits.push_back(m.mk_eq(to_app(l)->get_arg(i), access(c, i, acc, r)));
data/z3-4.8.9/src/sat/sat_lookahead.cpp:919:13:  [4] (format) printf:
  If format strings can be influenced by an attacker, they can be exploited
  (CWE-134). Use a constant for the format specification.
            printf((0 != (q & (1ull << i)))? "1" : "0");
data/z3-4.8.9/src/test/bit_blaster.cpp:32:9:  [4] (buffer) sprintf:
  Does not check for buffer overflows (CWE-120). Use sprintf_s, snprintf, or
  vsnprintf.
        sprintf(buffer, "%s%d.smt", prefix, i);
data/z3-4.8.9/src/test/lp/lp.cpp:2349:12:  [4] (shell) system:
  This causes a new program to execute and is difficult to use safely
  (CWE-78). try using a library call that implements the same functionality
  if available.
    return system(command_line.c_str());
data/z3-4.8.9/src/util/debug.cpp:105:17:  [4] (shell) system:
  This causes a new program to execute and is difficult to use safely
  (CWE-78). try using a library call that implements the same functionality
  if available.
            if (system(buffer) == 0) {
data/z3-4.8.9/src/util/warning.cpp:60:14:  [4] (format) vsnprintf:
  If format strings can be influenced by an attacker, they can be exploited,
  and note that sprintf variations do not always \0-terminate (CWE-134). Use
  a constant for the format specification.
#define VPRF vsnprintf
data/z3-4.8.9/src/util/warning.cpp:95:22:  [4] (format) vsnprintf:
  If format strings can be influenced by an attacker, they can be exploited,
  and note that sprintf variations do not always \0-terminate (CWE-134). Use
  a constant for the format specification.
    size_t msg_len = vsnprintf(nullptr, 0, msg, args_copy);
data/z3-4.8.9/src/util/warning.cpp:120:9:  [4] (format) vfprintf:
  If format strings can be influenced by an attacker, they can be exploited
  (CWE-134). Use a constant for the format specification.
        vfprintf(f, msg, args);
data/z3-4.8.9/examples/tptp/tptp5.cpp:1071:30:  [3] (buffer) getenv:
  Environment variables are untrustable input if they can be set by an
  attacker. They can have any content and length, and the same variable can
  be set more than once (CWE-807, CWE-20). Check environment variables
  carefully before using them.
        char const* buffer = getenv("$TPTP");
data/z3-4.8.9/src/math/lp/cross_nested.h:48:45:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
                 std::function<unsigned ()> random,
data/z3-4.8.9/src/math/lp/cross_nested.h:52:18:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        m_random(random),
data/z3-4.8.9/src/math/lp/gomory.cpp:420:76:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
            if (min_range > 2*new_range || ((5*min_range > 4*new_range && (random() % (++n)) == 0))) { 
data/z3-4.8.9/src/math/lp/gomory.cpp:432:51:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
            (4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) {
data/z3-4.8.9/src/math/lp/horner.cpp:93:31:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        [this]() { return c().random(); }, m_nex_creator);
data/z3-4.8.9/src/math/lp/horner.cpp:120:22:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned r = c().random();
data/z3-4.8.9/src/math/lp/int_branch.cpp:39:27:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        lia.m_upper = lia.random() % 2;
data/z3-4.8.9/src/math/lp/int_branch.cpp:43:27:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        lia.m_upper = lia.random() % 2;
data/z3-4.8.9/src/math/lp/int_branch.cpp:82:48:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        } else if (usage == prev_usage && (lia.random() % (++n) == 0)) {
data/z3-4.8.9/src/math/lp/int_branch.cpp:99:47:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        } else if (new_range == range && (lia.random() % (++n) == 0)) {
data/z3-4.8.9/src/math/lp/int_solver.cpp:241:22:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
unsigned int_solver::random() {
data/z3-4.8.9/src/math/lp/int_solver.cpp:529:33:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        impq new_val = m * impq(random() % (range + 1)) + x;
data/z3-4.8.9/src/math/lp/int_solver.cpp:546:37:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        impq new_val = x + m * impq(random() % (range + 1));
data/z3-4.8.9/src/math/lp/int_solver.cpp:553:37:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
        impq new_val = x - m * impq(random() % (range + 1));
data/z3-4.8.9/src/math/lp/int_solver.cpp:572:21:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    mpq s = b + mpq(random() % (range + 1));
data/z3-4.8.9/src/math/lp/int_solver.h:122:14:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned random();
data/z3-4.8.9/src/math/lp/nla_basics_lemmas.cpp:95:26:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned start = c().random();
data/z3-4.8.9/src/math/lp/nla_basics_lemmas.cpp:249:26:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned start = c().random();
data/z3-4.8.9/src/math/lp/nla_common.cpp:58:18:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
unsigned common::random() {
data/z3-4.8.9/src/math/lp/nla_common.cpp:59:16:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    return c().random();
data/z3-4.8.9/src/math/lp/nla_common.h:81:14:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned random();
data/z3-4.8.9/src/math/lp/nla_core.cpp:682:16:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
unsigned core::random() { return lp_settings().random_next(); }
data/z3-4.8.9/src/math/lp/nla_core.cpp:829:18:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned r = random(), sz = m_emons.number_of_monics();
data/z3-4.8.9/src/math/lp/nla_core.cpp:1002:18:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned r = random(), sz = m_to_refine.size();
data/z3-4.8.9/src/math/lp/nla_core.cpp:1401:22:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned start = random();
data/z3-4.8.9/src/math/lp/nla_core.h:387:14:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned random();
data/z3-4.8.9/src/math/lp/nla_monotone_lemmas.cpp:16:22:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned shift = random();
data/z3-4.8.9/src/math/lp/nla_order_lemmas.cpp:28:18:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    unsigned r = random();
data/z3-4.8.9/src/test/lp/lp.cpp:1722:5:  [3] (random) srand:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    srand(i);
data/z3-4.8.9/src/test/lp/lp.cpp:1743:22:  [3] (buffer) getenv:
  Environment variables are untrustable input if they can be set by an
  attacker. They can have any content and length, and the same variable can
  be set more than once (CWE-807, CWE-20). Check environment variables
  carefully before using them.
    char *home_dir = getenv("HOME");
data/z3-4.8.9/src/test/lp/lp.cpp:2284:25:  [3] (buffer) getenv:
  Environment variables are untrustable input if they can be set by an
  attacker. They can have any content and length, and the same variable can
  be set more than once (CWE-807, CWE-20). Check environment variables
  carefully before using them.
    char * home_dir =   getenv("HOME");
data/z3-4.8.9/src/test/main.cpp:150:9:  [3] (random) random:
  This function is not sufficiently random for security-related functions
  such as key and nonce creation (CWE-327). Use a more secure technique for
  acquiring random values.
    TST(random);
data/z3-4.8.9/contrib/qprofdiff/main.cpp:85:36:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
            entry.num_instances += atoi(tokens[1].c_str());
data/z3-4.8.9/contrib/qprofdiff/main.cpp:86:72:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
            entry.max_generation = max(entry.max_generation, (unsigned)atoi(tokens[2].c_str()));
data/z3-4.8.9/contrib/qprofdiff/main.cpp:87:60:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
            entry.max_cost = max(entry.max_cost, (unsigned)atoi(tokens[3].c_str()));
data/z3-4.8.9/examples/maxsat/maxsat.c:229:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(aux_1, lits, sizeof(Z3_ast) * n);
data/z3-4.8.9/examples/tptp/tptp5.cpp:123:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(result, s, l);
data/z3-4.8.9/examples/tptp/tptp5.cpp:998:14:  [2] (misc) fopen:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        fp = fopen(filename, "r");
data/z3-4.8.9/examples/tptp/tptp5.cpp:1061:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char buffer[1024];
data/z3-4.8.9/examples/tptp/tptp5.cpp:2148:29:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
                g_timeout = atoi(opt_arg);
data/z3-4.8.9/examples/tptp/tptp5.lex.cpp:654:1:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
char yytext[YYLMAX];
data/z3-4.8.9/examples/tptp/tptp5.tab.c:157:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char c1[4] = "%", c2[4] = "/*";
data/z3-4.8.9/examples/tptp/tptp5.tab.c:1887:7:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
      char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM];
data/z3-4.8.9/examples/tptp/tptp5.tab.c:1904:7:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
      char yyformat[sizeof yyunexpected
data/z3-4.8.9/examples/tptp/tptp5.tab.c:2096:3:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
  char yymsgbuf[128];
data/z3-4.8.9/src/api/z3_logger.h:61:22:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
            unsigned char str[4] = {'0', '0', '0', 0};
data/z3-4.8.9/src/ast/ast.cpp:329:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(const_cast<sort **>(get_domain()), domain, sizeof(sort *) * arity);
data/z3-4.8.9/src/ast/ast.cpp:390:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(const_cast<sort **>(get_decl_sorts()), decl_sorts, sizeof(sort *) * num_decls);
data/z3-4.8.9/src/ast/ast.cpp:391:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(const_cast<symbol*>(get_decl_names()), decl_names, sizeof(symbol) * num_decls);
data/z3-4.8.9/src/ast/ast.cpp:393:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(const_cast<expr **>(get_patterns()), patterns, sizeof(expr *) * num_patterns);
data/z3-4.8.9/src/ast/ast.cpp:395:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(const_cast<expr **>(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns);
data/z3-4.8.9/src/ast/ast.cpp:412:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(const_cast<sort **>(get_decl_sorts()), decl_sorts, sizeof(sort *) * num_decls);
data/z3-4.8.9/src/ast/ast.cpp:413:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(const_cast<symbol*>(get_decl_names()), decl_names, sizeof(symbol) * num_decls);   
data/z3-4.8.9/src/ast/ast.h:841:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char                m_patterns_decls[0];
data/z3-4.8.9/src/ast/format.cpp:154:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char buffer[128];
data/z3-4.8.9/src/ast/format.cpp:160:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char buffer[128];
data/z3-4.8.9/src/ast/proofs/proof_checker.cpp:1249:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char buffer[128];
data/z3-4.8.9/src/ast/proofs/proof_checker.cpp:1253:5:  [2] (buffer) sprintf:
  Does not check for buffer overflows (CWE-120). Use sprintf_s, snprintf, or
  vsnprintf. Risk is low because the source has a constant maximum length.
    sprintf(buffer, "proof_lemma_%d.smt2", m_proof_lemma_id);
data/z3-4.8.9/src/ast/seq_decl_plugin.cpp:236:14:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
static const char esc_table[32][6] =
data/z3-4.8.9/src/ast/seq_decl_plugin.cpp:243:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char buffer[100];
data/z3-4.8.9/src/math/interval/interval_def.h:1472:34:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            set_lower_is_open(x, open);
data/z3-4.8.9/src/math/interval/interval_def.h:1473:34:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            set_upper_is_open(x, open);
data/z3-4.8.9/src/math/realclosure/realclosure.cpp:1143:61:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        void set_lower_core(mpbqi & a, mpbq const & k, bool open, bool inf) {
data/z3-4.8.9/src/math/realclosure/realclosure.cpp:1145:33:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            a.set_lower_is_open(open);
data/z3-4.8.9/src/math/realclosure/realclosure.cpp:1153:34:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            set_lower_core(a, k, open, false);
data/z3-4.8.9/src/math/realclosure/realclosure.cpp:1177:61:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        void set_upper_core(mpbqi & a, mpbq const & k, bool open, bool inf) {
data/z3-4.8.9/src/math/realclosure/realclosure.cpp:1179:33:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            a.set_upper_is_open(open);
data/z3-4.8.9/src/math/realclosure/realclosure.cpp:1187:34:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            set_upper_core(a, k, open, false);
data/z3-4.8.9/src/math/subpaving/subpaving.cpp:81:63:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) override {
data/z3-4.8.9/src/math/subpaving/subpaving.cpp:82:71:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, k, lower, open)); 
data/z3-4.8.9/src/math/subpaving/subpaving.cpp:128:63:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) override {
data/z3-4.8.9/src/math/subpaving/subpaving.cpp:136:77:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
                return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, m_c, lower, open));
data/z3-4.8.9/src/math/subpaving/subpaving.cpp:185:63:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) override {
data/z3-4.8.9/src/math/subpaving/subpaving.cpp:193:77:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
                return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, m_c, lower, open));
data/z3-4.8.9/src/math/subpaving/subpaving.cpp:244:63:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) override {
data/z3-4.8.9/src/math/subpaving/subpaving.cpp:252:83:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
                return reinterpret_cast<ineq*>(this->m_ctx.mk_ineq(x, m_c, lower, open));
data/z3-4.8.9/src/math/subpaving/subpaving.h:82:67:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    virtual ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) = 0;
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:443:79:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        bound * mk_decided_bound(var x, numeral const & val, bool lower, bool open, node * n) { 
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:444:51:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            return ctx()->mk_bound(x, val, lower, open, n, justification());
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:541:67:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    bound * mk_bound(var x, numeral const & val, bool lower, bool open, node * n, justification jst);
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:544:71:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    void propagate_bound(var x, numeral const & val, bool lower, bool open, node * n, justification jst);
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:553:135:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    static void display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc, var x, numeral & k, bool lower, bool open);
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:636:67:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    void normalize_bound(var x, numeral & val, bool lower, bool & open);
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:642:72:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    bool relevant_new_bound(var x, numeral const & k, bool lower, bool open, node * n);
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:801:63:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    ineq * mk_ineq(var x, numeral const & k, bool lower, bool open);
data/z3-4.8.9/src/math/subpaving/subpaving_t.h:816:62:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    void add_ineq(var x, numeral const & k, bool lower, bool open, bool axiom);
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:255:138:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
void context_t<C>::display(std::ostream & out, numeral_manager & nm, display_var_proc const & proc, var x, numeral & k, bool lower, bool open) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:258:14:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        if (!open)
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:266:14:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        if (!open)
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:525:100:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
typename context_t<C>::bound * context_t<C>::mk_bound(var x, numeral const & val, bool lower, bool open, node * n, justification jst) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:541:13:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        if (open) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:557:22:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    r->m_open      = open;
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:575:81:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
void context_t<C>::propagate_bound(var x, numeral const & val, bool lower, bool open, node * n, justification jst) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:576:41:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    bound * b = mk_bound(x, val, lower, open, n, jst);
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:582:13:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    SASSERT(open || !nm().is_int(val) || !lower || nm().eq(n->lower(x)->value(), val));
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:583:13:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    SASSERT(open || !nm().is_int(val) || lower  || nm().eq(n->upper(x)->value(), val));
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:754:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(p->m_xs, xs, sizeof(var)*sz);
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:773:96:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
typename context_t<C>::ineq * context_t<C>::mk_ineq(var x, numeral const & k, bool lower, bool open) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:780:22:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    r->m_open      = open;
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:872:72:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
void context_t<C>::add_ineq(var x, numeral const & k, bool lower, bool open, bool axiom) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:873:40:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    ineq * unit = mk_ineq(x, k, lower, open);
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:1178:77:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
void context_t<C>::normalize_bound(var x, numeral & val, bool lower, bool & open) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:1189:13:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        if (open) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:1204:82:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
bool context_t<C>::relevant_new_bound(var x, numeral const & k, bool lower, bool open, node * n) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:1211:72:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
              display(tout, x); tout << " " << (lower ? ">" : "<") << (open ? "" : "=") << " "; nm().display(tout, k); tout << "\n";
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:1217:69:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            if (curr_upper && (nm().gt(k, curr_upper->value()) || ((open || curr_upper->is_open()) && nm().eq(k, curr_upper->value())))) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:1222:124:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            if (m_zero_epsilon && curr_lower != nullptr && (nm().lt(k, curr_lower->value()) || ((curr_lower->is_open() || !open) && nm().eq(k, curr_lower->value())))) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:1267:69:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            if (curr_lower && (nm().gt(curr_lower->value(), k) || ((open || curr_lower->is_open()) && nm().eq(k, curr_lower->value())))) {
data/z3-4.8.9/src/math/subpaving/subpaving_t_def.h:1272:124:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            if (m_zero_epsilon && curr_upper != nullptr && (nm().lt(curr_upper->value(), k) || ((curr_upper->is_open() || !open) && nm().eq(k, curr_upper->value())))) {
data/z3-4.8.9/src/math/subpaving/tactic/subpaving_tactic.cpp:145:26:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
                open  = !open;
data/z3-4.8.9/src/math/subpaving/tactic/subpaving_tactic.cpp:158:87:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            TRACE("subpaving_tactic", tout << x << " " << k << " " << lower << " " << open << "\n";);
data/z3-4.8.9/src/math/subpaving/tactic/subpaving_tactic.cpp:159:48:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
            return m_ctx->mk_ineq(x, k, lower, open);
data/z3-4.8.9/src/muz/fp/datalog_parser.cpp:106:18:  [2] (misc) fopen:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        m_file = fopen(fname, "rb");
data/z3-4.8.9/src/muz/fp/datalog_parser.cpp:629:24:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        unsigned num = atoi(m_lexer->get_token_data());
data/z3-4.8.9/src/muz/rel/dl_sparse_table.cpp:74:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(base+ofs, base+last_ofs, m_entry_size);
data/z3-4.8.9/src/muz/rel/dl_sparse_table.h:267:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(get_reserve_ptr(), data, m_entry_size);
data/z3-4.8.9/src/muz/rel/dl_sparse_table.h:353:17:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
                memcpy(rec + m_big_offset, &cell, sizeof(cell));
data/z3-4.8.9/src/muz/spacer/spacer_context.cpp:3333:12:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        of.open(m_params.spacer_print_json().bare_str());
data/z3-4.8.9/src/muz/spacer/spacer_iuc_solver.cpp:318:33:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
                            ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot");
data/z3-4.8.9/src/muz/spacer/spacer_iuc_solver.cpp:370:25:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
                    ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot");
data/z3-4.8.9/src/nlsat/nlsat_interval_set.cpp:273:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(new_set->m_intervals, buf.c_ptr(), sizeof(interval)*sz);
data/z3-4.8.9/src/nlsat/nlsat_justification.h:41:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char     m_data[0];
data/z3-4.8.9/src/nlsat/nlsat_justification.h:49:17:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
                memcpy(m_data + 0,                         clss, sizeof(nlsat::clause*)*nc);
data/z3-4.8.9/src/nlsat/nlsat_justification.h:52:17:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
                memcpy(m_data + sizeof(nlsat::clause*)*nc, lits, sizeof(literal)*nl);
data/z3-4.8.9/src/parsers/smt2/smt2scanner.h:46:16:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        signed char        m_normalized[256];
data/z3-4.8.9/src/parsers/smt2/smt2scanner.h:48:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char               m_buffer[SCANNER_BUFFER_SIZE];
data/z3-4.8.9/src/parsers/util/scanner.h:65:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char        m_normalized[256];
data/z3-4.8.9/src/sat/sat_allocator.h:31:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char    m_data[CHUNK_SIZE];
data/z3-4.8.9/src/sat/sat_clause.cpp:38:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(m_lits, lits, sizeof(literal) * sz);
data/z3-4.8.9/src/sat/sat_clause.cpp:151:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(m_clause->m_lits, lits, sizeof(literal) * num_lits);
data/z3-4.8.9/src/sat/sat_drat.cpp:91:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char buffer[10000];
data/z3-4.8.9/src/sat/sat_drat.cpp:92:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char digits[20];     // enough for storing unsigned
data/z3-4.8.9/src/sat/sat_drat.cpp:131:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(buffer + len, d, lastd - d);
data/z3-4.8.9/src/sat/sat_drat.cpp:160:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char buffer[10000];
data/z3-4.8.9/src/sat/sat_solver.cpp:2154:13:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
            char const* tag[9]  = { ":conflicts ", ":decisions ", ":restarts ", ":clauses/bin ", ":learned/bin ", ":units ", ":gc ", ":memory ", ":time" };
data/z3-4.8.9/src/smt/fingerprints.cpp:30:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(m_args, args, sizeof(enode*) * n);
data/z3-4.8.9/src/smt/mam.cpp:726:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(r->m_iregs, iregs, sizeof(unsigned) * num_args);
data/z3-4.8.9/src/smt/mam.cpp:736:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(r->m_iregs, iregs, sizeof(unsigned) * num_args);
data/z3-4.8.9/src/smt/mam.cpp:747:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(y->m_bindings, bindings, sizeof(unsigned) * num_bindings);
data/z3-4.8.9/src/smt/mam.cpp:759:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(r->m_joints, joints, num_args * sizeof(enode *));
data/z3-4.8.9/src/smt/old_interval.cpp:210:73:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
interval::interval(v_dependency_manager & m, rational const & val, bool open, bool lower, v_dependency * d):
data/z3-4.8.9/src/smt/old_interval.cpp:214:24:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        m_lower_open = open;
data/z3-4.8.9/src/smt/old_interval.cpp:225:24:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        m_upper_open = open;
data/z3-4.8.9/src/smt/old_interval.h:81:80:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    explicit old_interval(v_dependency_manager & m, rational const & val, bool open, bool lower, v_dependency * d);
data/z3-4.8.9/src/smt/smt_clause.cpp:46:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(cls->m_lits, lits, sizeof(literal) * num_lits);
data/z3-4.8.9/src/smt/smt_context.cpp:2749:13:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
            char const* tag[9] = { ":restarts ", ":conflicts ", ":decisions ", ":propagations ", ":clauses/bin ", ":lemmas ", ":simplify ", ":deletions", ":memory" };
data/z3-4.8.9/src/smt/smt_enode.cpp:366:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(get_enode()->m_args, args, sizeof(enode*)*num_args);
data/z3-4.8.9/src/smt/smt_justification.cpp:51:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(m_literals, lits, sizeof(literal) * num_lits);
data/z3-4.8.9/src/smt/smt_justification.cpp:64:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(m_literals, lits, sizeof(literal) * num_lits);
data/z3-4.8.9/src/smt/smt_justification.cpp:242:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(m_literals, lits, sizeof(literal) * num_lits);
data/z3-4.8.9/src/smt/theory_arith_pp.h:547:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char buffer[128];
data/z3-4.8.9/src/smt/theory_arith_pp.h:552:9:  [2] (buffer) sprintf:
  Does not check for buffer overflows (CWE-120). Use sprintf_s, snprintf, or
  vsnprintf. Risk is low because the source has a constant maximum length.
        sprintf(buffer, "arith_%d.smt", id);
data/z3-4.8.9/src/smt/theory_bv.h:127:18:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        unsigned char            m_eq_activity[256];
data/z3-4.8.9/src/smt/theory_bv.h:130:18:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        unsigned char            m_diseq_activity[256];
data/z3-4.8.9/src/smt/theory_str.cpp:8179:31:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
                    int val = atoi(sDigit.c_str());
data/z3-4.8.9/src/smt/watch_list.cpp:75:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(mem, m_data, curr_end_cls);
data/z3-4.8.9/src/smt/watch_list.cpp:76:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(reinterpret_cast<char *>(mem) + new_begin_bin, m_data + curr_begin_bin, bin_bytes);
data/z3-4.8.9/src/test/bit_blaster.cpp:28:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char buffer[128];
data/z3-4.8.9/src/test/expr_rand.cpp:97:30:  [2] (integer) atol:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        unsigned num_files = atol(argv[i+1]);
data/z3-4.8.9/src/test/expr_rand.cpp:100:25:  [2] (integer) atol:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
            rand_seed = atol(argv[i+1]+4);
data/z3-4.8.9/src/test/for_each_file.cpp:33:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char buffer[MAX_PATH];
data/z3-4.8.9/src/test/interval.cpp:201:8:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
static char g_buffer[BUFFER_SZ];
data/z3-4.8.9/src/test/interval.cpp:207:5:  [2] (buffer) sprintf:
  Does not check for buffer overflows (CWE-120). Use sprintf_s, snprintf, or
  vsnprintf. Risk is low because the source has a constant maximum length.
    sprintf(g_buffer, "interval_lemma_%d.smt2", g_problem_id);
data/z3-4.8.9/src/test/lp/lp.cpp:1346:13:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        n = atoi(s.c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2321:21:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        max_iters = atoi(s.c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2328:22:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        time_limit = atoi(time_limit_string.c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2648:76:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        solver->settings().max_number_of_iterations_with_no_improvements = atoi(maxng.c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2656:61:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        solver->settings().max_total_number_of_iterations = atoi(iter.c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2798:9:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
    m = atoi(r[1].c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2801:9:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
    n = atoi(r[1].c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2812:22:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        unsigned j = atoi(r[1].c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2826:18:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
    unsigned i = atoi(r[1].c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2844:22:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        unsigned j = atoi(line.c_str());
data/z3-4.8.9/src/test/lp/lp.cpp:2857:22:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
        unsigned i = atoi(r[0].c_str());
data/z3-4.8.9/src/test/lp/smt_reader.h:209:20:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
            return atoi(s.c_str()) != 0 || isdigit(s.c_str()[0]);
data/z3-4.8.9/src/test/lp/smt_reader.h:254:20:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
            return atoi(s.c_str());
data/z3-4.8.9/src/test/lp/smt_reader.h:262:25:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
                int v = atoi(el.m_head.c_str());
data/z3-4.8.9/src/test/nlsat.cpp:192:39:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        r = ism.mk(true, true, lower, open, false, upper, lit, nullptr);
data/z3-4.8.9/src/test/nlsat.cpp:214:23:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
        curr = ism.mk(open, false, lower, true, true, upper, lit, nullptr);
data/z3-4.8.9/src/test/sat_local_search.cpp:9:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char  line[16383];
data/z3-4.8.9/src/test/sat_local_search.cpp:94:21:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
                v = atoi(argv[i + 2]);
data/z3-4.8.9/src/test/sat_local_search.cpp:98:21:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
                v = atoi(argv[i + 2]);
data/z3-4.8.9/src/test/sat_local_search.cpp:102:21:  [2] (integer) atoi:
  Unless checked, the resulting number can exceed the expected range
  (CWE-190). If source untrusted, check both minimum and maximum, even if the
  input had no minus sign (large numbers can roll over into negative number;
  consider saving to an unsigned value if that is intended).
                v = atoi(argv[i + 2]);
data/z3-4.8.9/src/util/bit_vector.h:80:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(m_data, source.m_data, m_capacity * sizeof(unsigned));
data/z3-4.8.9/src/util/bit_vector.h:88:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(m_data, source, m_capacity * sizeof(unsigned));
data/z3-4.8.9/src/util/bit_vector.h:200:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(m_data, source.m_data, source.m_capacity * sizeof(unsigned));
data/z3-4.8.9/src/util/buffer.h:33:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char     m_initial_buffer[INITIAL_SIZE * sizeof(T)];
data/z3-4.8.9/src/util/debug.cpp:79:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char buffer[1024];
data/z3-4.8.9/src/util/debug.cpp:103:13:  [2] (buffer) sprintf:
  Does not check for buffer overflows (CWE-120). Use sprintf_s, snprintf, or
  vsnprintf. Risk is low because the source has a constant maximum length.
            sprintf(buffer, "gdb -nw /proc/%d/exe %d", getpid(), getpid());
data/z3-4.8.9/src/util/fixed_bit_vector.cpp:85:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(dst.m_data, src.m_data, num_bytes());
data/z3-4.8.9/src/util/gparams.cpp:157:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(r, s, strlen(s)+1);
data/z3-4.8.9/src/util/hash.cpp:26:3:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
  memcpy(&n, s, sizeof(unsigned));
data/z3-4.8.9/src/util/hwf.cpp:96:40:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
uint64_t RAW(double X) { uint64_t tmp; memcpy(&tmp, &(X), sizeof(uint64_t)); return tmp; }
data/z3-4.8.9/src/util/hwf.cpp:97:38:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
double DBL(uint64_t X) { double tmp; memcpy(&tmp, &(X), sizeof(double)); return tmp; }
data/z3-4.8.9/src/util/hwf.cpp:177:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(&o.value, &raw, sizeof(double));
data/z3-4.8.9/src/util/hwf.h:33:7:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
      memcpy(&n, &value, sizeof(value));
data/z3-4.8.9/src/util/mpf.cpp:120:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(&raw, &value, sizeof(double));
data/z3-4.8.9/src/util/mpf.cpp:156:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(&raw, &value, sizeof(float));
data/z3-4.8.9/src/util/mpf.cpp:1736:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(&ret, &raw, sizeof(double));
data/z3-4.8.9/src/util/mpf.cpp:1768:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(&ret, &raw, sizeof(float));
data/z3-4.8.9/src/util/mpfx.cpp:206:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(&_v, &_vp, sizeof(unsigned*));
data/z3-4.8.9/src/util/mpfx.cpp:690:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(&r, w, sizeof(uint64_t));
data/z3-4.8.9/src/util/mpfx.cpp:705:5:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
    memcpy(&r, w, sizeof(uint64_t));
data/z3-4.8.9/src/util/mpn.cpp:405:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char char_buf[4096];
data/z3-4.8.9/src/util/mpn.cpp:414:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char char_buf[4096];
data/z3-4.8.9/src/util/mpn.cpp:421:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char char_buf[4096];
data/z3-4.8.9/src/util/mpz.cpp:457:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(target.m_ptr->m_digits, digits, sizeof(digit_t) * sz);
data/z3-4.8.9/src/util/mpz.cpp:462:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(ptr->m_digits, digits, sizeof(digit_t) * sz);
data/z3-4.8.9/src/util/mpz.cpp:474:17:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
                memcpy(target.m_ptr->m_digits, digits, sizeof(digit_t) * sz);
data/z3-4.8.9/src/util/mpz.cpp:1499:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source));
data/z3-4.8.9/src/util/mpz.cpp:1508:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source));
data/z3-4.8.9/src/util/mpz.cpp:1512:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source));
data/z3-4.8.9/src/util/mpz.h:126:14:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    unsigned char m_bytes[sizeof(mpz_cell) + sizeof(digit_t) * capacity];
data/z3-4.8.9/src/util/mpz.h:298:18:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        unsigned char m_bytes[sizeof(mpz_cell) + sizeof(digit_t) * capacity];
data/z3-4.8.9/src/util/small_object_allocator.h:32:9:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
        char    m_data[CHUNK_SIZE];
data/z3-4.8.9/src/util/string_buffer.h:30:5:  [2] (buffer) char:
  Statically-sized arrays can be improperly restricted, leading to potential
  overflows or other issues (CWE-119!/CWE-120). Perform bounds checking, use
  functions that limit length, or ensure that the size is larger than the
  maximum possible length.
    char   m_initial_buffer[INITIAL_SIZE];
data/z3-4.8.9/src/util/string_buffer.h:38:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(new_buffer, m_buffer, m_pos);
data/z3-4.8.9/src/util/string_buffer.h:77:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(m_buffer + m_pos, str, len);
data/z3-4.8.9/src/util/string_buffer.h:87:9:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
        memcpy(m_buffer + m_pos, str.c_str(), len);
data/z3-4.8.9/src/util/symbol.cpp:65:13:  [2] (buffer) memcpy:
  Does not check for buffer overflows when copying to destination (CWE-120).
  Make sure destination can always hold the source data.
            memcpy(mem, d, l+1);
data/z3-4.8.9/src/util/trace.cpp:63:10:  [2] (misc) open:
  Check when opening files - can an attacker redirect it (via symlinks),
  force the opening of special file type (e.g., device files), move things
  around to create a race condition, control its ancestors, or change its
  contents? (CWE-362).
    tout.open(".z3-trace");
data/z3-4.8.9/src/util/util.h:53:34:  [2] (buffer) sprintf:
  Does not check for buffer overflows (CWE-120). Use sprintf_s, snprintf, or
  vsnprintf. Risk is low because the source has a constant maximum length.
#define SPRINTF_D(_buffer_, _i_) sprintf(_buffer_, "%d", _i_)
data/z3-4.8.9/src/util/util.h:54:34:  [2] (buffer) sprintf:
  Does not check for buffer overflows (CWE-120). Use sprintf_s, snprintf, or
  vsnprintf. Risk is low because the source has a constant maximum length.
#define SPRINTF_U(_buffer_, _u_) sprintf(_buffer_, "%u", _u_)
data/z3-4.8.9/examples/tptp/tptp5.cpp:121:16:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
    size_t l = strlen(s) + 1;
data/z3-4.8.9/examples/tptp/tptp5.cpp:1029:22:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        size_t len = strlen(m_filename);
data/z3-4.8.9/examples/tptp/tptp5.cpp:2195:18:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
    size_t len = strlen(filename);
data/z3-4.8.9/examples/tptp/tptp5.lex.cpp:832:14:  [1] (buffer) getc:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
			     (c = getc( yyin )) != EOF && c != '\n'; ++n ) \
data/z3-4.8.9/examples/tptp/tptp5.lex.cpp:2420:34:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
	return yy_scan_bytes(yystr,(int)strlen(yystr) );
data/z3-4.8.9/examples/tptp/tptp5.tab.c:1768:21:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
#   define yystrlen strlen
data/z3-4.8.9/src/ast/ast_smt2_pp.cpp:51:37:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        len = static_cast<unsigned>(strlen(s.bare_str()));
data/z3-4.8.9/src/ast/ast_smt2_pp.cpp:593:64:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                          mk_indent(m(), static_cast<unsigned>(strlen(attr)), f));
data/z3-4.8.9/src/ast/ast_smt_pp.cpp:676:49:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                sz += 3 + static_cast<unsigned>(strlen(s.bare_str()));
data/z3-4.8.9/src/ast/format.h:94:49:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        unsigned indent = static_cast<unsigned>(strlen(lp) + strlen(header) + 1);
data/z3-4.8.9/src/ast/format.h:94:62:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        unsigned indent = static_cast<unsigned>(strlen(lp) + strlen(header) + 1);
data/z3-4.8.9/src/ast/format.h:130:74:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                                      mk_indent(m, static_cast<unsigned>(strlen(lp)),
data/z3-4.8.9/src/ast/format.h:160:83:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                                   mk_group(m, mk_indent(m, static_cast<unsigned>(strlen(header) + strlen(lp) + 1),
data/z3-4.8.9/src/ast/format.h:160:100:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                                   mk_group(m, mk_indent(m, static_cast<unsigned>(strlen(header) + strlen(lp) + 1),
data/z3-4.8.9/src/ast/format.h:178:50:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        unsigned indent1 = static_cast<unsigned>(strlen(lp));
data/z3-4.8.9/src/ast/format.h:198:67:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        return mk_seq4(m, begin, end, proc, static_cast<unsigned>(strlen(lp)), lp, rp);
data/z3-4.8.9/src/ast/pp.cpp:89:41:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
            len = static_cast<unsigned>(strlen(f->get_decl()->get_parameter(0).get_symbol().bare_str()));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:164:37:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            r = make_node(level(a), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:164:46:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            r = make_node(level(a), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:169:37:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            r = make_node(level(a), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:169:46:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            r = make_node(level(a), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:174:37:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            r = make_node(level(b), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:174:46:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            r = make_node(level(b), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:191:35:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    bdd_manager::BDD bdd_manager::read(unsigned index) {
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:569:37:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        BDD r = make_node(level(b), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:569:46:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        BDD r = make_node(level(b), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:630:28:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        r = make_node(lvl, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:630:37:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        r = make_node(lvl, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:677:36:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(lvl, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.cpp:677:45:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(lvl, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_bdd.h:147:13:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        BDD read(unsigned index);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:215:40:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(1), hi(p));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:221:40:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(2), read(1));                           
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:221:49:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(2), read(1));                           
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:226:40:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(1), hi(p));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:235:40:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_q, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:235:49:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_q, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:240:40:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(1), hi(p));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:248:40:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(2), read(1));                           
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:248:49:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(2), read(1));                           
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:256:40:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:256:49:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:266:35:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    unsigned bd = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:269:36:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    push(apply_rec(read(1), read(2), pdd_mul_op));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:269:45:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    push(apply_rec(read(1), read(2), pdd_mul_op));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:270:36:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    push(apply_rec(read(1), bd, pdd_sub_op));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:271:48:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    r = make_node(level_p, bd, read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:287:35:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    unsigned ac = read(4), ad = read(3), bc = read(2), bd = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:287:49:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    unsigned ac = read(4), ad = read(3), bc = read(2), bd = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:287:63:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    unsigned ac = read(4), ad = read(3), bc = read(2), bd = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:287:77:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    unsigned ac = read(4), ad = read(3), bc = read(2), bd = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:289:34:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    unsigned n = read(1); // n = ad + bc
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:292:56:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                        push(make_node(level_p, lo(n), read(1)));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:293:52:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                        r = make_node(level_p, bd, read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:297:52:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                        r = make_node(level_p, bd, read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:307:40:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:307:49:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                r = make_node(level_p, read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:314:27:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                PDD plo = read(2), phi = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:314:42:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                PDD plo = read(2), phi = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:323:36:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    push(apply_rec(read(1), plo, pdd_add_op));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:324:25:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
                    r = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:340:35:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            push(apply_rec(lo(q), read(1), pdd_mul_op));       // hi := hi*s[var(p)]
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:341:27:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            r = apply_rec(read(1), read(3), pdd_add_op);       // r := hi + lo := subst(lo(p),s) + s[var(p)]*subst(hi(p),s)
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:341:36:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            r = apply_rec(read(1), read(3), pdd_add_op);       // r := hi + lo := subst(lo(p),s) + s[var(p)]*subst(hi(p),s)
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:386:37:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        PDD r = make_node(level(a), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:386:46:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        PDD r = make_node(level(a), read(2), read(1));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:403:28:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            push(apply_rec(read(1), b, pdd_mul_op));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:404:31:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            push(apply_rec(a, read(1), pdd_add_op));
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:405:17:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            a = read(1);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:469:46:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        PDD r = apply_rec(m_var2pdd[var(q)], read(1), pdd_mul_op);
data/z3-4.8.9/src/math/dd/dd_pdd.cpp:697:35:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    pdd_manager::PDD pdd_manager::read(unsigned index) {
data/z3-4.8.9/src/math/dd/dd_pdd.h:190:13:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        PDD read(unsigned index);
data/z3-4.8.9/src/math/lp/cross_nested.h:259:38:  [1] (buffer) equal:
  Function does not check the second iterator for over-read conditions
  (CWE-126). This function is often discouraged by most C++ coding standards
  in favor of its safer alternatives provided since C++14. Consider using a
  form of this function that checks the second iterator before potentially
  overflowing it.
                SASSERT(nex_creator::equal(m_e, m_e_clone));
data/z3-4.8.9/src/math/lp/cross_nested.h:289:34:  [1] (buffer) equal:
  Function does not check the second iterator for over-read conditions
  (CWE-126). This function is often discouraged by most C++ coding standards
  in favor of its safer alternatives provided since C++14. Consider using a
  form of this function that checks the second iterator before potentially
  overflowing it.
            SASSERT(nex_creator::equal(m_e, m_e_clone));
data/z3-4.8.9/src/math/lp/mps_reader.h:769:10:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    void read() {
data/z3-4.8.9/src/math/lp/nex_creator.cpp:649:19:  [1] (buffer) equal:
  Function does not check the second iterator for over-read conditions
  (CWE-126). This function is often discouraged by most C++ coding standards
  in favor of its safer alternatives provided since C++14. Consider using a
  form of this function that checks the second iterator before potentially
  overflowing it.
bool nex_creator::equal(const nex* a, const nex* b) {
data/z3-4.8.9/src/math/lp/nex_creator.h:284:17:  [1] (buffer) equal:
  Function does not check the second iterator for over-read conditions
  (CWE-126). This function is often discouraged by most C++ coding standards
  in favor of its safer alternatives provided since C++14. Consider using a
  form of this function that checks the second iterator before potentially
  overflowing it.
    static bool equal(const nex*, const nex* );
data/z3-4.8.9/src/model/model_pp.cpp:47:62:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        unsigned indent = static_cast<unsigned>(n.length() + strlen(d) + 1);
data/z3-4.8.9/src/model/model_smt2_pp.cpp:46:38:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        return static_cast<unsigned>(strlen(s.bare_str()));
data/z3-4.8.9/src/model/model_v2_pp.cpp:29:51:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
    unsigned else_indent  = static_cast<unsigned>(strlen(else_str));
data/z3-4.8.9/src/model/model_v2_pp.cpp:74:65:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        unsigned indent = static_cast<unsigned>(name.length() + strlen(arrow));
data/z3-4.8.9/src/muz/base/dl_util.cpp:578:30:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                size_t len = strlen(name);
data/z3-4.8.9/src/muz/fp/datalog_parser.cpp:70:15:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        m_stm.read(m_data.begin()+start, should_read);
data/z3-4.8.9/src/params/context_params.cpp:45:17:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
    size_t sz = strlen(value);
data/z3-4.8.9/src/parsers/smt2/smt2parser.cpp:451:25:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                if (msg[strlen(msg)-1] != '\n')
data/z3-4.8.9/src/parsers/smt2/smt2parser.cpp:474:25:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                if (msg[strlen(msg)-1] != '\n')
data/z3-4.8.9/src/parsers/smt2/smt2scanner.cpp:39:22:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
            m_stream.read(m_buffer, SCANNER_BUFFER_SIZE);
data/z3-4.8.9/src/parsers/util/scanner.cpp:29:18:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        m_stream.read(m_buffer.c_ptr()+1, m_buffer.size()-1);
data/z3-4.8.9/src/sat/sat_solver.cpp:2165:27:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                    p2 += strlen(tag[i]);
data/z3-4.8.9/src/sat/sat_solver.cpp:2171:27:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                    p1 += strlen(tag[i]);
data/z3-4.8.9/src/shell/lp_frontend.cpp:68:12:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    reader.read();
data/z3-4.8.9/src/smt/smt_context.cpp:2761:27:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                    p2 += strlen(tag[i]);
data/z3-4.8.9/src/smt/smt_context.cpp:2767:27:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                    p1 += strlen(tag[i]);
data/z3-4.8.9/src/smt/smt_quantifier.cpp:635:26:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
            size_t len = strlen(m_fparams->m_mbqi_id);
data/z3-4.8.9/src/smt/theory_str_regex.cpp:951:22:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
            rational strlen(str.length());
data/z3-4.8.9/src/smt/theory_str_regex.cpp:952:71:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
            expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_numeral(strlen, true)), m);
data/z3-4.8.9/src/smt/theory_str_regex.cpp:1074:18:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        expr_ref strlen(mk_strlen(str), m);
data/z3-4.8.9/src/smt/theory_str_regex.cpp:1083:46:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                expr_ref rhs1(ctx.mk_eq_atom(strlen, m_autil.mk_numeral(rational::zero(), true)), m);
data/z3-4.8.9/src/smt/theory_str_regex.cpp:1084:45:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                expr_ref rhs2(m_autil.mk_ge(strlen, m_autil.mk_numeral(nonzero_lower_bound, true)), m);
data/z3-4.8.9/src/smt/theory_str_regex.cpp:1088:46:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                expr_ref rhs1(ctx.mk_eq_atom(strlen, m_autil.mk_numeral(rational::zero(), true)), m);
data/z3-4.8.9/src/smt/theory_str_regex.cpp:1095:45:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
                expr_ref rhs2(m_autil.mk_ge(strlen, m_autil.mk_numeral(nonzero_lower_bound, true)), m);
data/z3-4.8.9/src/test/lp/lp.cpp:115:25:  [1] (buffer) equal:
  Function does not check the second iterator for over-read conditions
  (CWE-126). This function is often discouraged by most C++ coding standards
  in favor of its safer alternatives provided since C++14. Consider using a
  form of this function that checks the second iterator before potentially
  overflowing it.
    ENSURE(nex_creator::equal(ab, ba));
data/z3-4.8.9/src/test/lp/lp.cpp:150:25:  [1] (buffer) equal:
  Function does not check the second iterator for over-read conditions
  (CWE-126). This function is often discouraged by most C++ coding standards
  in favor of its safer alternatives provided since C++14. Consider using a
  form of this function that checks the second iterator before potentially
  overflowing it.
    ENSURE(nex_creator::equal(simp_two_a_plus_bc, two_a_plus_bc));
data/z3-4.8.9/src/test/lp/lp.cpp:1434:12:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    reader.read();
data/z3-4.8.9/src/test/lp/lp.cpp:1494:12:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    reader.read();
data/z3-4.8.9/src/test/lp/lp.cpp:1546:12:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    reader.read();
data/z3-4.8.9/src/test/lp/lp.cpp:1634:12:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    reader.read();
data/z3-4.8.9/src/test/lp/lp.cpp:1646:12:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    reader.read();
data/z3-4.8.9/src/test/lp/lp.cpp:2703:16:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        reader.read();
data/z3-4.8.9/src/test/lp/lp.cpp:2711:12:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    reader.read();
data/z3-4.8.9/src/test/lp/lp.cpp:2723:12:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
    reader.read();
data/z3-4.8.9/src/test/lp/smt_reader.h:300:14:  [1] (buffer) read:
  Check buffer boundaries if used in a loop including recursive loops
  (CWE-120, CWE-20).
        void read() {
data/z3-4.8.9/src/test/string_buffer.cpp:37:10:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
  ENSURE(strlen(b.c_str()) == 10000);
data/z3-4.8.9/src/util/gparams.cpp:156:40:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        char * r = new (m_region) char[strlen(s)+1];
data/z3-4.8.9/src/util/gparams.cpp:157:22:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        memcpy(r, s, strlen(s)+1);
data/z3-4.8.9/src/util/params.cpp:174:48:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
            unsigned n = static_cast<unsigned>(strlen(s));
data/z3-4.8.9/src/util/smt2_util.cpp:36:42:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
    unsigned len = static_cast<unsigned>(strlen(s));
data/z3-4.8.9/src/util/statistics.cpp:95:47:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        unsigned curr = static_cast<unsigned>(strlen(k));
data/z3-4.8.9/src/util/statistics.cpp:121:46:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        unsigned len = static_cast<unsigned>(strlen(k));        \
data/z3-4.8.9/src/util/statistics.cpp:154:46:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        unsigned len = static_cast<unsigned>(strlen(k));        \
data/z3-4.8.9/src/util/str_hashtable.h:27:93:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
    unsigned operator()(char const * s) const { return string_hash(s, static_cast<unsigned>(strlen(s)), 17); } 
data/z3-4.8.9/src/util/string_buffer.h:72:28:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        size_t len       = strlen(str);
data/z3-4.8.9/src/util/symbol.cpp:59:26:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
            size_t l   = strlen(d);
data/z3-4.8.9/src/util/symbol.cpp:94:67:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        auto* table = tables[string_hash(d, static_cast<unsigned>(strlen(d)), 251) % sz];
data/z3-4.8.9/src/util/symbol.cpp:159:38:  [1] (buffer) strlen:
  Does not handle strings that are not \0-terminated; if given one it may
  perform an over-read (it could cause a crash if unprotected) (CWE-126).
        return static_cast<unsigned>(strlen(m_data));

ANALYSIS SUMMARY:

Hits = 365
Lines analyzed = 610393 in approximately 13.85 seconds (44086 lines/second)
Physical Source Lines of Code (SLOC) = 464394
Hits@level = [0] 236 [1] 125 [2] 191 [3]  33 [4]  16 [5]   0
Hits@level+ = [0+] 601 [1+] 365 [2+] 240 [3+]  49 [4+]  16 [5+]   0
Hits/KSLOC@level+ = [0+] 1.29416 [1+] 0.785971 [2+] 0.516803 [3+] 0.105514 [4+] 0.0344535 [5+]   0
Dot directories skipped = 1 (--followdotdir overrides)
Minimum risk level = 1
Not every hit is necessarily a security vulnerability.
There may be other security vulnerabilities; review your code!
See 'Secure Programming HOWTO'
(https://dwheeler.com/secure-programs) for more information.