diff --git a/pkgs/applications/science/logic/yices/default.nix b/pkgs/applications/science/logic/yices/default.nix
new file mode 100644
index 000000000000..5a1a4ef19922
--- /dev/null
+++ b/pkgs/applications/science/logic/yices/default.nix
@@ -0,0 +1,40 @@
+{ stdenv, fetchurl }:
+
+let
+  libPath = stdenv.lib.makeLibraryPath [ stdenv.gcc.libc ];
+in
+stdenv.mkDerivation rec {
+  name    = "yices-${version}";
+  version = "2.2.1";
+
+  src =
+    if stdenv.system == "i686-linux"
+    then fetchurl {
+      url = "http://yices.csl.sri.com/cgi-bin/yices2-newdownload.cgi?file=yices-2.2.1-i686-pc-linux-gnu-static-gmp.tar.gz&accept=I+accept";
+      name = "yices-${version}-i686.tar.gz";
+      sha256 = "12jzk3kqlbqa5x6rl92cpzj7dch7gm7fnbj72wifvwgdj4zyhrra";
+    }
+    else fetchurl {
+      url = "http://yices.csl.sri.com/cgi-bin/yices2-newdownload.cgi?file=yices-2.2.1-x86_64-unknown-linux-gnu-static-gmp.tar.gz&accept=I+accept";
+      name = "yices-${version}-x86_64.tar.gz";
+      sha256 = "0fpmihf6ykcg4qbsimkamgcwp4sl1xyxmz7q28ily91rd905ijaj";
+    };
+
+  buildPhase = false;
+  installPhase = ''
+    mkdir -p $out/bin $out/lib $out/include
+    cd bin     && mv * $out/bin     && cd ..
+    cd lib     && mv * $out/lib     && cd ..
+    cd include && mv * $out/include && cd ..
+
+    patchelf --set-rpath ${libPath} $out/lib/libyices.so.${version}
+  '';
+
+  meta = {
+    description = "Yices is a high-performance theorem prover and SMT solver";
+    homepage    = "http://yices.csl.sri.com";
+    license     = stdenv.lib.licenses.unfreeRedistributable;
+    platforms   = stdenv.lib.platforms.linux;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 45ba490702e7..06f5211d9b95 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -10356,6 +10356,8 @@ let
 
   tptp = callPackage ../applications/science/logic/tptp {};
 
+  yices = callPackage ../applications/science/logic/yices {};
+
   z3 = callPackage ../applications/science/logic/z3 {};
 
   boolector   = boolector15;