From 60861d7deab99e5f3790ca82ba08550a7a5f5485 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Jan 2016 22:13:04 -0800
Subject: [PATCH] chore(tests/lean/run/blast_cc_heq9): make sure that only
 congruence closure module is used

---
 tests/lean/run/blast_cc_heq9.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tests/lean/run/blast_cc_heq9.lean b/tests/lean/run/blast_cc_heq9.lean
index fe4a2b8ec..15c78b09f 100644
--- a/tests/lean/run/blast_cc_heq9.lean
+++ b/tests/lean/run/blast_cc_heq9.lean
@@ -1,4 +1,5 @@
 open subtype
+set_option blast.strategy "cc"
 
 example (f g : Π {A : Type₁}, A → A → A) (h : nat → nat) (a b : nat) :
         h = f a → h b = f a b :=