diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix
index 9f5f18ca6a5..22a4310eee2 100644
--- a/maintainers/maintainer-list.nix
+++ b/maintainers/maintainer-list.nix
@@ -11326,6 +11326,12 @@
     githubId = 1151264;
     name = "Sebastian Graf";
   };
+  shadaj = {
+    email = "shadaj@users.noreply.github.com";
+    github = "shadaj";
+    githubId = 543055;
+    name = "Shadaj Laddad";
+  };
   shahrukh330 = {
     email = "shahrukh330@gmail.com";
     github = "shahrukh330";
diff --git a/pkgs/applications/science/logic/cvc5/default.nix b/pkgs/applications/science/logic/cvc5/default.nix
new file mode 100644
index 00000000000..c1bf56b45d5
--- /dev/null
+++ b/pkgs/applications/science/logic/cvc5/default.nix
@@ -0,0 +1,34 @@
+{ lib, stdenv, fetchFromGitHub, pkg-config, cmake, cadical, symfpu, gmp, git, python3, gtest, libantlr3c, antlr3_4, boost, jdk }:
+
+stdenv.mkDerivation rec {
+  pname = "cvc5";
+  version = "1.0.0";
+
+  src = fetchFromGitHub {
+    owner  = "cvc5";
+    repo   = "cvc5";
+    rev    = "cvc5-${version}";
+    sha256 = "03sxqwmlajffmv7lncqs1bx8gyihkpnikk87q9wjrd4776n13ign";
+  };
+
+  nativeBuildInputs = [ pkg-config cmake ];
+  buildInputs = [ cadical.dev symfpu gmp git python3 python3.pkgs.toml gtest libantlr3c antlr3_4 boost jdk ];
+
+  preConfigure = ''
+    patchShebangs ./src/
+  '';
+
+  cmakeFlags = [
+    "-DCMAKE_BUILD_TYPE=Production"
+    "-DBUILD_SHARED_LIBS=1"
+    "-DANTLR3_JAR=${antlr3_4}/lib/antlr/antlr-3.4-complete.jar"
+  ];
+
+  meta = with lib; {
+    description = "A high-performance theorem prover and SMT solver";
+    homepage    = "https://cvc5.github.io";
+    license     = licenses.gpl3Only;
+    platforms   = platforms.unix;
+    maintainers = with maintainers; [ shadaj ];
+  };
+}
diff --git a/pkgs/applications/science/logic/symfpu/default.nix b/pkgs/applications/science/logic/symfpu/default.nix
new file mode 100644
index 00000000000..af61b7c617c
--- /dev/null
+++ b/pkgs/applications/science/logic/symfpu/default.nix
@@ -0,0 +1,26 @@
+{ lib, stdenv, fetchFromGitHub }:
+
+stdenv.mkDerivation rec {
+  pname = "symfpu";
+  version = "unstable-2019-05-17";
+
+  src = fetchFromGitHub {
+    owner  = "martin-cs";
+    repo   = "symfpu";
+    rev    = "8fbe139bf0071cbe0758d2f6690a546c69ff0053";
+    sha256 = "1jf5lkn67q136ppfacw3lsry369v7mdr1rhidzjpbz18jfy9zl9q";
+  };
+
+  installPhase = ''
+    mkdir -p $out/symfpu
+    cp -r * $out/symfpu/
+  '';
+
+  meta = with lib; {
+    description = "A (concrete or symbolic) implementation of IEEE-754 / SMT-LIB floating-point";
+    homepage    = "https://github.com/martin-cs/symfpu";
+    license     = licenses.gpl3Only;
+    platforms   = platforms.unix;
+    maintainers = with maintainers; [ shadaj ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index b744d5c7079..29dc030eae1 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -32649,6 +32649,8 @@ with pkgs;
     jdk = jdk8; # TODO: remove override https://github.com/NixOS/nixpkgs/pull/89731
   };
 
+  cvc5 = callPackage ../applications/science/logic/cvc5 { };
+
   drat-trim = callPackage ../applications/science/logic/drat-trim {};
 
   ekrhyper = callPackage ../applications/science/logic/ekrhyper {
@@ -32812,6 +32814,8 @@ with pkgs;
 
   symbiyosys = callPackage ../applications/science/logic/symbiyosys {};
 
+  symfpu = callPackage ../applications/science/logic/symfpu {};
+
   mcy = callPackage ../applications/science/logic/mcy {};
 
   lingeling = callPackage ../applications/science/logic/lingeling {};