motoko-san: bump z3 solver

Problem: Currently used z3 version abnormally fails on GA macOS
runners.

Solution: Use 'z3_4_12' instead of 'z3' in nix setup.

default.nix

@@ -509,7 +509,7 @@ rec {
       run-deser  = test_subdir "run-deser"  [ deser ];
       perf       = perf_subdir "perf"       [ moc nixpkgs.drun ];
       bench      = perf_subdir "bench"      [ moc nixpkgs.drun ic-wasm ];
-      viper      = test_subdir "viper"      [ moc nixpkgs.which nixpkgs.openjdk nixpkgs.z3 ];
+      viper      = test_subdir "viper"      [ moc nixpkgs.which nixpkgs.openjdk nixpkgs.z3_4_12 ];
       inherit qc lsp unit candid profiling-graphs coverage;
     }) // { recurseForDerivations = true; };
 
@@ -818,7 +818,7 @@ EOF
           niv
           nix-update
           rlwrap # for `rlwrap moc`
-          openjdk z3 # for viper dev
+          openjdk z3_4_12 # for viper dev
           difftastic
         ] ++ lib.optional stdenv.isDarwin darwin.apple_sdk.frameworks.Security
       ));