add_subdirectory(fuzzing)
add_subdirectory(lp)
################################################################################
# z3-test executable
################################################################################
set(z3_test_deps api fuzzing simplex)
add_executable(test-z3
  EXCLUDE_FROM_ALL
  ackermannize.cpp
  algebraic.cpp
  algebraic_numbers.cpp
  api_ast_map.cpp
  api_bug.cpp
  api_special_relations.cpp
  api.cpp
  api_algebraic.cpp
  api_polynomial.cpp
  api_pb.cpp
  api_datalog.cpp
  parametric_datatype.cpp
  arith_rewriter.cpp
  arith_simplifier_plugin.cpp
  ast.cpp
  bdd.cpp
  bit_blaster.cpp
  bits.cpp
  bit_vector.cpp
  buffer.cpp
  chashtable.cpp
  check_assumptions.cpp
  cnf_backbones.cpp
  context_params.cpp
  cube_clause.cpp
  datalog_parser.cpp
  ddnf.cpp
  deep_api_bugs.cpp
  diff_logic.cpp
  distribution.cpp
  dl_context.cpp
  dl_product_relation.cpp
  dl_query.cpp
  dl_relation.cpp
  dl_table.cpp
  dl_util.cpp
  doc.cpp  
  dlist.cpp
  egraph.cpp
  escaped.cpp
  euf_assoc_plugin.cpp
  euf_bv_plugin.cpp
  euf_seq_plugin.cpp
  euf_arith_plugin.cpp
  ex.cpp
  expr_rand.cpp
  expr_substitution.cpp
  ext_numeral.cpp
  f2n.cpp
  fpa.cpp
  finite_set.cpp
  finite_set_rewriter.cpp
  factor_rewriter.cpp
  finder.cpp
  fixed_bit_vector.cpp
  for_each_file.cpp
  get_consequences.cpp
  get_implied_equalities.cpp
  grobner.cpp
  hashtable.cpp
  heap.cpp
  heap_trie.cpp
  hilbert_basis.cpp
  ho_matcher.cpp
  ho_qsolver.cpp
  horn_subsume_model_converter.cpp
  horner.cpp
  hwf.cpp
  inf_rational.cpp
  interval.cpp
  karr.cpp
  lcube.cpp
  len_abs.cpp
  list.cpp
  main.cpp
  map.cpp
  matcher.cpp
  memory.cpp
  model2expr.cpp
  model_based_opt.cpp
  mod_factor.cpp
  model_evaluator.cpp
  model_retrieval.cpp
  monomial_bounds.cpp
  nla_transcendentals.cpp
  mpbq.cpp
  mpf.cpp
  mpff.cpp
  mpfx.cpp
  mpq.cpp
  mpz.cpp
  nlarith_util.cpp
  nla_intervals.cpp
  nlsat.cpp
  no_overflow.cpp
  object_allocator.cpp
  old_interval.cpp
  opt_bounds.cpp
  opt_nlsat.cpp
  opt_pareto.cpp
  opt_value.cpp
  optional.cpp
  parray.cpp
  pb2bv.cpp
  pdd.cpp
  pdd_solver.cpp
  permutation.cpp
  ff_domain.cpp
  ff_solver.cpp
  finite_field.cpp
  polynomial.cpp
  polynomial_factorization.cpp
  polynorm.cpp
  prime_generator.cpp
  psmt.cpp
  seq_regex_bisim.cpp
  proof_checker.cpp
  proof_replay.cpp
  qe_arith.cpp
  qe_lite.cpp
  mbp_qel.cpp
  quant_elim.cpp
  quant_solve.cpp
  random.cpp
  range_predicate.cpp
  rational.cpp
  rcf.cpp
  region.cpp
  regex_range_collapse.cpp
  sat_local_search.cpp
  sat_lookahead.cpp
  sat_user_scope.cpp
  scoped_timer.cpp
  scoped_vector.cpp
  seq_power.cpp
  seq_rewriter.cpp
  seq_parikh.cpp
  seq_eq_approx.cpp
  seq_regex_witness.cpp
  seq_monadic.cpp
  seq_monadic_bench.cpp
  seq_profile_abs.cpp
  simple_parser.cpp
  scanner_io.cpp
  simplex.cpp
  simplifier.cpp
  sls_test.cpp
  sls_seq_plugin.cpp
  small_object_allocator.cpp
  smt2print_parse.cpp
  smt_context.cpp
  solver_pool.cpp
  sorting_network.cpp
  stack.cpp
  string_buffer.cpp
  substitution.cpp
  symbol.cpp
  symbol_table.cpp
  tbv.cpp
  term_enumeration.cpp
  theory_dl.cpp
  theory_pb.cpp
  timeout.cpp
  tptp.cpp
  tptp_crashes.cpp
  total_order.cpp
  totalizer.cpp
  trigo.cpp
  udoc_relation.cpp
  uint_set.cpp
  upolynomial.cpp
  value_generator.cpp
  value_sweep.cpp
  var_subst.cpp
  vector.cpp
  lp/bound_propagation.cpp
  lp/lp.cpp
  lp/nla_solver_test.cpp
  zstring.cpp
)
target_link_libraries(test-z3 PRIVATE
  z3_common ${z3_test_deps})

# External finite-field regressions live in z3test. The dedicated CI job pins
# its checkout and supplies this path; ordinary Z3 builds need no test checkout.
set(Z3_FF_TEST_DIR "" CACHE PATH "z3test/regressions/finite_field directory")
if (Z3_FF_TEST_DIR)
  if (NOT EXISTS "${Z3_FF_TEST_DIR}/api_smoke.cpp")
    message(FATAL_ERROR "Z3_FF_TEST_DIR must contain api_smoke.cpp")
  endif()
  add_executable(test-ff-api EXCLUDE_FROM_ALL "${Z3_FF_TEST_DIR}/api_smoke.cpp")
  target_link_libraries(test-ff-api PRIVATE libz3)
  if (MSVC)
    target_compile_options(test-ff-api PRIVATE /UNDEBUG)
  else()
    target_compile_options(test-ff-api PRIVATE -UNDEBUG)
  endif()
endif()
