diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp
index cf0add6eb..4deab33e0 100644
--- a/src/library/blast/strategies/portfolio.cpp
+++ b/src/library/blast/strategies/portfolio.cpp
@@ -4,16 +4,29 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "library/blast/strategies/simple_strategy.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 
 namespace lean {
 namespace blast {
+static optional<expr> apply_preprocess() {
+    return preprocess_and_then([]() { return none_expr(); })();
+}
+
 static optional<expr> apply_simple() {
     return preprocess_and_then(mk_simple_strategy())();
 }
 
 optional<expr> apply_strategy() {
-    return apply_simple();
+    std::string s_name(get_config().m_strategy);
+    if (s_name == "preprocess") {
+        return apply_preprocess();
+    } else if (s_name == "simple") {
+        return apply_simple();
+    } else {
+        // TODO(Leo): add more builtin strategies
+        return apply_simple();
+    }
 }
 }}
diff --git a/tests/lean/run/blast1.lean b/tests/lean/run/blast1.lean
index 103f0f8da..a7acda4fa 100644
--- a/tests/lean/run/blast1.lean
+++ b/tests/lean/run/blast1.lean
@@ -1,2 +1,4 @@
+set_option blast.strategy "preprocess"
+
 example (a b : Prop) (Ha : a) (Hb : b) : a :=
 by blast
diff --git a/tests/lean/run/blast2.lean b/tests/lean/run/blast2.lean
index 259f07084..d5dd8c2da 100644
--- a/tests/lean/run/blast2.lean
+++ b/tests/lean/run/blast2.lean
@@ -1,3 +1,5 @@
+set_option blast.strategy "preprocess"
+
 example (a b : Prop) : forall (Ha : a) (Hb : b), a :=
 by blast
 
diff --git a/tests/lean/run/blast3.lean b/tests/lean/run/blast3.lean
index 190015b5e..c08596fd1 100644
--- a/tests/lean/run/blast3.lean
+++ b/tests/lean/run/blast3.lean
@@ -1,4 +1,5 @@
-set_option blast.init_depth 10
+-- TODO(Leo): use better strategy
+set_option blast.strategy "simple"
 set_option blast.cc false
 
 example (a b c : Prop) : b → c → b ∧ c :=
diff --git a/tests/lean/run/blast4.lean b/tests/lean/run/blast4.lean
index 2126eec67..3d08abde2 100644
--- a/tests/lean/run/blast4.lean
+++ b/tests/lean/run/blast4.lean
@@ -1,3 +1,5 @@
+set_option blast.strategy "preprocess"
+
 lemma T1 (a b : Prop) : false → a :=
 by blast
 
diff --git a/tests/lean/run/blast5.lean b/tests/lean/run/blast5.lean
index 5886a3d9e..eda312965 100644
--- a/tests/lean/run/blast5.lean
+++ b/tests/lean/run/blast5.lean
@@ -1,4 +1,4 @@
-set_option blast.init_depth 10
+set_option blast.strategy "preprocess"
 
 example (a b : nat) : a = b → b = a :=
 by blast
diff --git a/tests/lean/run/blast6.lean b/tests/lean/run/blast6.lean
index 432c28ab7..c54500534 100644
--- a/tests/lean/run/blast6.lean
+++ b/tests/lean/run/blast6.lean
@@ -1,4 +1,4 @@
-set_option blast.init_depth 10
+set_option blast.strategy "preprocess"
 
 lemma lemma1 (bv : nat → Type) (n m : nat) (H : n = m) (b1 : bv n) (b2 : bv m) (H2 : eq.rec_on H b1 = b2) : b1 = eq.rec_on (eq.symm H) b2 :=
 by blast
diff --git a/tests/lean/run/blast7.lean b/tests/lean/run/blast7.lean
index c39193387..dd49488eb 100644
--- a/tests/lean/run/blast7.lean
+++ b/tests/lean/run/blast7.lean
@@ -1,4 +1,4 @@
-set_option blast.init_depth 10
+set_option blast.strategy "preprocess"
 
 lemma lemma1 (p : Prop) (a b : nat) : a = b → p → p :=
 by blast
diff --git a/tests/lean/run/blast8.lean b/tests/lean/run/blast8.lean
index 0d311deb3..c7879746f 100644
--- a/tests/lean/run/blast8.lean
+++ b/tests/lean/run/blast8.lean
@@ -1,6 +1,5 @@
 open nat
-set_option blast.init_depth 10
-set_option blast.max_depth 10
+set_option blast.strategy "preprocess"
 
 lemma l1 (a : nat) : zero = succ a → a = a → false :=
 by blast
diff --git a/tests/lean/run/blast9.lean b/tests/lean/run/blast9.lean
index 652239b0c..5b5c59e53 100644
--- a/tests/lean/run/blast9.lean
+++ b/tests/lean/run/blast9.lean
@@ -1,5 +1,6 @@
 import data.list
 open list
+set_option blast.strategy "preprocess"
 
 example (p : Prop) (a b c : nat) : [a, b, c] = [] → p :=
 by blast