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()