diff --git a/pkgs/applications/science/logic/verifast/default.nix b/pkgs/applications/science/logic/verifast/default.nix
index 71c5faf4bc81..a2959892ddb9 100644
--- a/pkgs/applications/science/logic/verifast/default.nix
+++ b/pkgs/applications/science/logic/verifast/default.nix
@@ -40,7 +40,7 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Verification for C and Java programs via separation logic";
     homepage    = "http://people.cs.kuleuven.be/~bart.jacobs/verifast/";
-    license     = stdenv.lib.licenses.unfreeRedistributable;
+    license     = stdenv.lib.licenses.msrla;
     platforms   = [ "i686-linux" ];
     maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
   };
diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix
index eeef03eb1619..7a87cb5e8be0 100644
--- a/pkgs/applications/science/logic/z3/default.nix
+++ b/pkgs/applications/science/logic/z3/default.nix
@@ -39,7 +39,7 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Z3 is a high-performance theorem prover and SMT solver";
     homepage    = "http://z3.codeplex.com";
-    license     = stdenv.lib.licenses.unfreeRedistributable;
+    license     = stdenv.lib.licenses.msrla;
     platforms   = stdenv.lib.platforms.unix;
     maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
   };