{
  lib,
  pkgs,
  mkCoqDerivation,
  coq,
  zchaff,
  cvc5,
  stdlib,
  trakt,
  version ? null,
}:

# Broken since https://github.com/NixOS/nixpkgs/pull/354627, temporarily disactivated
# let
#   # version of veriT that works with SMTCoq
#   veriT' = veriT.overrideAttrs {
#     src = fetchurl {
#       url = "https://www.lri.fr/~keller/Documents-recherche/Smtcoq/veriT9f48a98.tar.gz";
#       hash = "sha256-Pe46PxQVHWwWwx5Ei4Bl95A0otCiXZuUZ2nXuZPYnhY=";
#     };
#     meta.broken = false;
#   };
# in

let
  derivation = mkCoqDerivation {
    pname = "smtcoq";
    owner = "smtcoq";
    opam-name = "rocq-smtcoq";

    release."SMTCoq-2.3+8.20".hash = "sha256-ScWtdwSpFBf/PryPuvI/SkhgqWyYhcX3FCOqoXNho7Q=";
    release."SMTCoq-2.2+8.19".hash = "sha256-9Wv8AXRRyOHG/cjA/V9tSK55R/bofDMLTkDpuwYWkks=";
    release."SMTCoq-2.2+8.18".hash = "sha256-1iJAruI5Qn9nTZcUDjk8t/1Q+eFkYLOe9Ee0DmK03w8=";
    release."SMTCoq-2.2+8.17".hash = "sha256-kaodsyVUl1+QQagzoBTIjxbdD4X3IaaH0x2AsVUL+Z0=";
    release."SMTCoq-2.2+8.16".hash = "sha256-Hwm8IFlw97YiOY6H63HyJlwIXvQHr9lqc1+PgTnBtkw=";
    release."SMTCoq-2.2+8.15".hash = "sha256-+GYOasJ32KJyOfqJlTtFmsJ2exd6gdueKwHdeMPErTo=";
    release."SMTCoq-2.2+8.14".hash = "sha256-jqnF33E/4CqR1HSrLmUmLVCKslw9h3bbWi4YFmFYrhY=";
    release."SMTCoq-2.2+8.13".hash = "sha256-AVpKU/SLaLYnCnx6GOEPGJjwbRrp28Fs5O50kJqdclI=";
    release."SMTCoq-2.1+8.16".rev = "4996c00b455bfe98400e96c954839ceea93efdf7";
    release."SMTCoq-2.1+8.16".hash = "sha256-k53e+frUjwq+ZZKbbOKd/EfVC40QeAzB2nCsGkCKnHA=";
    release."SMTCoq-2.1+8.14".rev = "e11d9b424b0113f32265bcef0ddc962361da4dae";
    release."SMTCoq-2.1+8.14".hash = "sha256-4a01/CRHUon2OfpagAnMaEVkBFipPX3MCVmSFS1Bnt4=";
    release."SMTCoq-2.1+8.13".rev = "d02269c43739f4559d83873563ca00daad9faaf1";
    release."SMTCoq-2.1+8.13".hash = "sha256-VZetGghdr5uJWDwZWSlhYScoNEoRHIbwqwJKSQyfKKg=";

    releaseRev = v: v;

    inherit version;
    defaultVersion =
      let
        case = case: out: { inherit case out; };
      in
      with lib.versions;
      lib.switch coq.coq-version [
        (case (isEq "8.20") "SMTCoq-2.3+${coq.coq-version}")
        (case (range "8.13" "8.19") "SMTCoq-2.2+${coq.coq-version}")
      ] null;

    propagatedBuildInputs = [
      cvc5
      # veriT'  # c.f. comment above
      zchaff
      stdlib
    ]
    ++ (with coq.ocamlPackages; [
      findlib
      num
      zarith
    ]);
    useDuneifVersion = v: v != null && (v == "dev" || lib.versions.isGt "SMTCoq-2.3+8.20" v);
    mlPlugin = true;
    nativeBuildInputs = (with pkgs; [ gnumake42 ]) ++ (with coq.ocamlPackages; [ ocamlbuild ]);

    # This is meant to ease future troubleshooting of cvc5 build failures
    passthru = { inherit cvc5; };

    meta = {
      description = "Communication between Coq and SAT/SMT solvers";
      maintainers = with lib.maintainers; [ siraben ];
      license = lib.licenses.cecill-b;
      platforms = lib.platforms.unix;
    };
  };
  patched-derivation1 = derivation.overrideAttrs (
    o:
    lib.optionalAttrs
      (o.version != null && (o.version == "dev" || lib.versions.isGt "SMTCoq-2.3+8.20" o.version))
      {
        propagatedBuildInputs = o.propagatedBuildInputs ++ [ trakt ];
      }
  );
in
patched-derivation1