From 4e8ae94aba8dd5cd613223b88e8b96df2a9537e4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Jan 2016 17:30:31 -0800
Subject: [PATCH] chore(tests/lean/run/blast_cc_noconfusion): make sure
 simp/subst are not used in the test

---
 tests/lean/run/blast_cc_noconfusion.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/lean/run/blast_cc_noconfusion.lean b/tests/lean/run/blast_cc_noconfusion.lean
index 462dc49af..0e8c51c74 100644
--- a/tests/lean/run/blast_cc_noconfusion.lean
+++ b/tests/lean/run/blast_cc_noconfusion.lean
@@ -1,6 +1,8 @@
 import data.list
 open nat
 
+set_option blast.strategy "cc"
+
 constant f : nat → nat
 
 example (a b c d : nat) : f d = f b → succ a = f b → f d = succ c → a = c :=