config BR2_PACKAGE_Z3
	bool "z3"
	depends on BR2_INSTALL_LIBSTDCPP
	depends on BR2_TOOLCHAIN_GCC_AT_LEAST_7 # c++17
	# z3 needs fenv.h which is not provided by uclibc
	depends on !BR2_TOOLCHAIN_USES_UCLIBC
	# fenv.h lacks FE_INVALID, FE_OVERFLOW & FE_UNDERFLOW on nios2
	depends on !BR2_nios2
	help
	  Z3, also known as the Z3 Theorem Prover, is a cross-platform
	  satisfiability modulo theories (SMT) solver.

	  https://github.com/Z3Prover/z3

if BR2_PACKAGE_Z3

config BR2_PACKAGE_Z3_PYTHON
	bool "Python bindings"
	depends on BR2_PACKAGE_PYTHON3
	select BR2_PACKAGE_PYTHON3_PYEXPAT # runtime
	select BR2_PACKAGE_PYTHON_SETUPTOOLS # runtime

endif