diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp
index dd4be53f45..c4a710cbd0 100644
--- a/src/library/blast/strategy.cpp
+++ b/src/library/blast/strategy.cpp
@@ -93,4 +93,13 @@ optional<expr> strategy_fn::search() {
         trace_curr_state_if(r);
     }
 }
+
+strategy operator|(strategy const & s1, strategy const & s2) {
+    return [=]() {
+        if (auto r = s1())
+            return r;
+        else
+            return s2();
+    }
+}
 }}
diff --git a/src/library/blast/strategy.h b/src/library/blast/strategy.h
index a542657578..55c46166ce 100644
--- a/src/library/blast/strategy.h
+++ b/src/library/blast/strategy.h
@@ -41,4 +41,6 @@ public:
     }
 
 typedef std::function<optional<expr>()> strategy;
+
+strategy operator|(strategy const & s1, strategy const & s2);
 }}