chore(tests/lean/try_for_heap): disable expensive test

tests/lean/try_for_heap.lean

@@ -43,6 +43,11 @@ example
 : is_def (h₁ ∙ (x₁ ↣ v₁ ∙ x₂ ↣ v₂) ∙ h₂ ∙ (x₃ ↣ v₃)) → x₁ ≠ x₃ ∧ x₁ ≠ x₂ ∧ x₂ ≠ x₃ :=
 by try_for 100 $ my_tac -- should timeout
 
+/-
+Remark: disable this test because it was too slow.
+TODO(Leo): enable again after we resolve the cache issues, and re-implement the SMT
+tactic framework
+
 example
 (h₁ h₂ : heap) (x₁ x₂ x₃ x₄ : ptr) (v₁ v₂ v₃ : val)
 (hcomm    : ∀ x y, x ∙ y = y ∙ x)
@@ -50,3 +55,4 @@ example
 (hnoalias : ∀ h y₁ y₂ w₁ w₂, is_def (h ∙ y₁ ↣ w₁ ∙ y₂ ↣ w₂) → y₁ ≠ y₂)
 : is_def (h₁ ∙ (x₁ ↣ v₁ ∙ x₂ ↣ v₂) ∙ h₂ ∙ (x₃ ↣ v₃)) → x₁ ≠ x₃ ∧ x₁ ≠ x₂ ∧ x₂ ≠ x₃ :=
 by try_for 100000 $ my_tac -- should work
+-/