diff --git a/opam/opam-repository/packages/z3_tptp/z3_tptp.4.13.3/opam b/opam/opam-repository/packages/z3_tptp/z3_tptp.4.13.3/opam
new file mode 100644
index 0000000000..ff1dd47fbc
--- /dev/null
+++ b/opam/opam-repository/packages/z3_tptp/z3_tptp.4.13.3/opam
@@ -0,0 +1,37 @@
+opam-version: "2.0"
+maintainer: "7895506+MSoegtropIMC@users.noreply.github.com"
+authors: "MSR"
+homepage: "https://github.com/Z3prover/z3"
+bug-reports: "https://github.com/Z3prover/z3/issues"
+license: "MIT"
+dev-repo: "git+https://github.com/Z3prover/z3.git"
+# OK, this is really ugly, but it is quite hard to do this via z3's make system
+# using an already installed opam z3.
+# Also this should be quite robust with just source 2 files and opam knowns the
+# library folder better than any configure script.
+build: [
+  [ "g++"
+    "-I./src/api/c++"
+    "-I./src/api"
+    "-std=c++11"
+    "-L%{lib}%/stublibs"
+    "-o" "z3_tptp"
+    "examples/tptp/tptp5.cpp" "examples/tptp/tptp5.lex.cpp" 
+    "-lz3"
+    "-Wl,-rpath"
+    "-Wl,%{lib}%/stublibs"
+  ]
+]
+install: [ "cp" "z3_tptp" "%{bin}%/z3_tptp" ]
+depends: [
+  "z3" { >= "4.13.3" & < "4.13.4~" }
+  "conf-g++" {build}
+]
+synopsis: "TPTP front end for Z3 solver"
+url {
+  src: "https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.13.3.tar.gz"
+  checksum: [
+    "sha256=f59c9cf600ea57fb64ffeffbffd0f2d2b896854f339e846f48f069d23bc14ba0"
+    "sha512=c899f57d8cb5450801463b07cd651869d766a920e41a4beedc96c4978e940bfadff9af2fbbb5ba10f94f6742bb33f7abaca0a351f3e1803d778e84d735d6829e"
+  ]
+}
diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh
index 01a320be9b..72567949af 100644
--- a/package_picks/package-pick-8.20~2025.01.sh
+++ b/package_picks/package-pick-8.20~2025.01.sh
@@ -73,13 +73,13 @@ then
   
   # Standard library extensions
   PACKAGES="${PACKAGES} coq-bignums.9.0.0+coq8.20"
-  PACKAGES="${PACKAGES} coq-ext-lib.0.12.2"
+  PACKAGES="${PACKAGES} coq-ext-lib.0.13.0"
   PACKAGES="${PACKAGES} coq-stdpp.1.11.0"
 
   # General mathematics
-  PACKAGES="${PACKAGES} elpi.1.19.6 coq-elpi.2.2.3"   # required by coq-hierarchy-builder
-  PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.0"
-  PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.3.0" # Todo: move elpi and hierarchy builder before this
+  PACKAGES="${PACKAGES} elpi.2.0.5 coq-elpi.2.3.0" # This would belong into the "Proof automation" section, but it is required by coq-hierarchy-builder
+  PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.1"
+  PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.3.0"
   PACKAGES="${PACKAGES} coq-mathcomp-fingroup.2.3.0"
   PACKAGES="${PACKAGES} coq-mathcomp-algebra.2.3.0"
   PACKAGES="${PACKAGES} coq-mathcomp-solvable.2.3.0"
@@ -203,12 +203,12 @@ then
     case "$COQ_PLATFORM_FIATCRYPTO" in
       [yY])
         PACKAGES="${PACKAGES} coq-coqutil.0.0.6"
-#       PACKAGES="${PACKAGES} coq-rewriter.0.0.11" # ToDo: fails to build
+        PACKAGES="${PACKAGES} coq-rewriter.0.0.12"
         PACKAGES="${PACKAGES} coq-riscv.0.0.5"
         PACKAGES="${PACKAGES} coq-bedrock2.0.0.8"
         PACKAGES="${PACKAGES} coq-bedrock2-compiler.0.0.8"
         PACKAGES="${PACKAGES} coq-rupicola.0.0.10"
-#       PACKAGES="${PACKAGES} coq-fiat-crypto.0.1.3" # ToDo: there is a 0.1.4 version in git but not in opam, ToDo: requires coq-rewriter
+        PACKAGES="${PACKAGES} coq-fiat-crypto.0.1.3"
         ;;
       [nN]) true ;;
       *) echo "Illegal value for COQ_PLATFORM_FIATCRYPTO - aborting"; false ;;