z3_add_component(smt
  SOURCES
    arith_eq_adapter.cpp
    arith_eq_solver.cpp
    asserted_formulas.cpp
    cached_var_subst.cpp
    cost_evaluator.cpp
    dyn_ack.cpp
    elim_term_ite.cpp
    expr_context_simplifier.cpp
    fingerprints.cpp
    mam.cpp
    old_interval.cpp
    qi_queue.cpp
    smt_almost_cg_table.cpp
    smt_case_split_queue.cpp
    smt_cg_table.cpp
    smt_checker.cpp
    smt_clause.cpp
    smt_conflict_resolution.cpp
    smt_consequences.cpp
    smt_context.cpp
    smt_context_inv.cpp
    smt_context_pp.cpp
    smt_context_stat.cpp
    smt_enode.cpp
    smt_farkas_util.cpp
    smt_for_each_relevant_expr.cpp
    smt_implied_equalities.cpp
    smt_internalizer.cpp
    smt_justification.cpp
    smt_kernel.cpp
    smt_literal.cpp
    smt_model_checker.cpp
    smt_model_finder.cpp
    smt_model_generator.cpp
    smt_quantifier.cpp
    smt_quantifier_stat.cpp
    smt_quick_checker.cpp
    smt_relevancy.cpp
    smt_setup.cpp
    smt_solver.cpp
    smt_statistics.cpp
    smt_theory.cpp
    smt_value_sort.cpp
    smt2_extra_cmds.cpp
    theory_arith.cpp
    theory_array_base.cpp
    theory_array.cpp
    theory_array_full.cpp
    theory_bv.cpp
    theory_datatype.cpp
    theory_dense_diff_logic.cpp
    theory_diff_logic.cpp
    theory_dl.cpp
    theory_dummy.cpp
    theory_fpa.cpp
    theory_opt.cpp
    theory_pb.cpp
    theory_seq.cpp
    theory_str.cpp
    theory_utvpi.cpp
    theory_wmaxsat.cpp
    uses_theory.cpp
    watch_list.cpp
  COMPONENT_DEPENDENCIES
    bit_blaster
    cmd_context
    euclid
    fpa
    grobner
    macros
    normal_forms
    parser_util
    pattern
    proof_checker
    proto_model
    simplex
    substitution
)