{
  lib,
  astroid,
  buildPythonPackage,
  fetchFromGitHub,
  flit-core,
  hypothesis,
  pytest-cov-stub,
  pytest-xdist,
  pytestCheckHook,
  z3-solver,
}:

buildPythonPackage rec {
  pname = "deal-solver";
  version = "0.1.2";
  pyproject = true;

  src = fetchFromGitHub {
    owner = "life4";
    repo = "deal-solver";
    tag = version;
    hash = "sha256-DAOeQLFR/JED32uJSW7W9+Xx5f1Et05W8Fp+Vm7sfZo=";
  };

  build-system = [ flit-core ];

  # z3 does not provide a dist-info, so python-runtime-deps-check will fail
  pythonRemoveDeps = [ "z3-solver" ];

  dependencies = [
    z3-solver
    astroid
  ]
  ++ z3-solver.requiredPythonModules;

  nativeCheckInputs = [
    hypothesis
    pytest-cov-stub
    pytest-xdist
    pytestCheckHook
  ];

  pythonImportsCheck = [ "deal_solver" ];

  disabledTests = [
    # Flaky tests, sometimes it works sometimes it doesn't
    "test_expr_asserts_ok"
    "test_fuzz_math_floats"
    "test_model_skip_helpers2"
    # test does not pass on python314 because an error message has changed
    "test_type_error__table"
  ];

  meta = {
    description = "Z3-powered solver (theorem prover) for deal";
    homepage = "https://github.com/life4/deal-solver";
    changelog = "https://github.com/life4/deal-solver/releases/tag/${version}";
    license = lib.licenses.mit;
    maintainers = with lib.maintainers; [ gador ];
  };
}