diff --git a/src/library/blast/strategies/portfolio.cpp b/src/library/blast/strategies/portfolio.cpp
index 11fd177da1..aa56a30f88 100644
--- a/src/library/blast/strategies/portfolio.cpp
+++ b/src/library/blast/strategies/portfolio.cpp
@@ -10,6 +10,8 @@ Author: Leonardo de Moura
 #include "library/blast/simplifier/simplifier_strategies.h"
 #include "library/blast/unit/unit_actions.h"
 #include "library/blast/forward/ematch.h"
+#include "library/blast/backward/backward_action.h"
+#include "library/blast/backward/backward_strategy.h"
 #include "library/blast/strategies/simple_strategy.h"
 #include "library/blast/strategies/preprocess_strategy.h"
 #include "library/blast/strategies/debug_action_strategy.h"
@@ -46,6 +48,14 @@ static optional<expr> apply_ematch() {
                                     ematch_action)();
 }
 
+static optional<expr> apply_constructor() {
+    return mk_debug_action_strategy([]() { return constructor_action(); })();
+}
+
+static optional<expr> apply_backward() {
+    return preprocess_and_then(mk_backward_strategy())();
+}
+
 static optional<expr> apply_unit() {
     return mk_debug_action_strategy(unit_preprocess,
                                     unit_propagate,
@@ -69,8 +79,12 @@ optional<expr> apply_strategy() {
         return apply_cc();
     } else if (s_name == "ematch") {
         return apply_ematch();
+    } else if (s_name == "constructor") {
+        return apply_constructor();
     } else if (s_name == "unit") {
         return apply_unit();
+    } else if (s_name == "backward") {
+        return apply_backward();
     } else {
         throw exception(sstream() << "unknown blast strategy '" << s_name << "'");
     }
diff --git a/tests/lean/run/blast10.lean b/tests/lean/run/blast10.lean
index 97fab26485..ec0073890f 100644
--- a/tests/lean/run/blast10.lean
+++ b/tests/lean/run/blast10.lean
@@ -1,6 +1,6 @@
 import data.list
 
-set_option blast.trace true
+set_option blast.strategy "unit"
 
 definition lemma1 : true :=
 by blast
diff --git a/tests/lean/run/blast11.lean b/tests/lean/run/blast11.lean
index c344517133..08b1da392d 100644
--- a/tests/lean/run/blast11.lean
+++ b/tests/lean/run/blast11.lean
@@ -2,11 +2,11 @@ import data.nat
 open algebra nat
 
 definition lemma1 (a b : nat) : a + b + 0 = b + a :=
-by blast
+by simp
 
 print lemma1
 
 definition lemma2 (a b c : nat) : a + b + 0 + c + a + a + b = 0 + 0 + c + a + b + a + a + b :=
-by blast
+by simp
 
 print lemma2
diff --git a/tests/lean/run/blast12.lean b/tests/lean/run/blast12.lean
index 7aa7746bde..56405ebfea 100644
--- a/tests/lean/run/blast12.lean
+++ b/tests/lean/run/blast12.lean
@@ -1,5 +1,5 @@
 import data.nat
-open algebra nat
+open nat
 
 example (a b : nat) : 0 + a + b + 1 = 1 + a + b :=
-by blast
+by simp
diff --git a/tests/lean/run/blast13.lean b/tests/lean/run/blast13.lean
index 26cd8bca3c..8d27fffb7c 100644
--- a/tests/lean/run/blast13.lean
+++ b/tests/lean/run/blast13.lean
@@ -1,5 +1,6 @@
 import data.list
 open perm
+set_option blast.strategy "cc"
 
 example (p : Prop) (l : list nat) : ¬ l ~ l → p :=
 by blast
diff --git a/tests/lean/run/blast17.lean b/tests/lean/run/blast17.lean
index fc9325f9da..a36d49e39b 100644
--- a/tests/lean/run/blast17.lean
+++ b/tests/lean/run/blast17.lean
@@ -1,2 +1,4 @@
+set_option blast.strategy "preprocess"
+
 example (p q r : Prop) (a b : nat) : true → a = a → q → q → p → p :=
 by blast
diff --git a/tests/lean/run/blast18.lean b/tests/lean/run/blast18.lean
index 935ad4e89e..6bd84f2eb7 100644
--- a/tests/lean/run/blast18.lean
+++ b/tests/lean/run/blast18.lean
@@ -1,4 +1,5 @@
 -- Backward chaining with tagged rules
+set_option blast.strategy "backward"
 constants {P Q R S T U : Prop} (Hpq : P → Q) (Hqr : Q → R) (Hrs : R → S) (Hst : S → T)
 constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
 attribute Hpq [backward]
diff --git a/tests/lean/run/blast19.lean b/tests/lean/run/blast19.lean
index 08e3d07e77..870f16b7a1 100644
--- a/tests/lean/run/blast19.lean
+++ b/tests/lean/run/blast19.lean
@@ -1,4 +1,5 @@
 -- Backward chaining with hypotheses
+set_option blast.strategy "backward"
 constants {P Q R S T U : Prop}
 constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
 attribute Huq [backward]
diff --git a/tests/lean/run/blast21.lean b/tests/lean/run/blast21.lean
index d840fef2f1..c897154a91 100644
--- a/tests/lean/run/blast21.lean
+++ b/tests/lean/run/blast21.lean
@@ -1,4 +1,5 @@
 namespace ex
+set_option blast.strategy "backward"
 
 constant typ : Type₁
 
diff --git a/tests/lean/run/blast3.lean b/tests/lean/run/blast3.lean
index c08596fd16..72ddcf967f 100644
--- a/tests/lean/run/blast3.lean
+++ b/tests/lean/run/blast3.lean
@@ -1,6 +1,5 @@
 -- TODO(Leo): use better strategy
-set_option blast.strategy "simple"
-set_option blast.cc false
+set_option blast.strategy "constructor"
 
 example (a b c : Prop) : b → c → b ∧ c :=
 by blast