comment out non-deterministic tests

Test/Tactic.lean

@@ -150,29 +150,31 @@ theorem testBit_pred :
       (Bool.xor ((List.range i).all fun j => ! testBit x j) (testBit x i))) := by
   plausible
 
-/--
-error:
-===================
-Found a counter-example!
-f := 1
-issue: ULift.up 1 = ULift.up 0 does not hold
-(1 shrinks)
--------------------
--/
-#guard_msgs in
-theorem ulift_nat (f : ULift.{1} Nat) : f = ⟨0⟩ := by
-  plausible
-
-/--
-error:
-===================
-Found a counter-example!
-α := "ULift Int"
-l := [0]
-issue: [ULift.up 0] = [ULift.up 0, ULift.up 0] does not hold
-(1 shrinks)
--------------------
--/
-#guard_msgs in
-theorem type_u (α : Type u) (l : List α) : l = l ++ l := by
-  plausible
+-- FIXME: the following two tests have become non-deterministic.
+
+-- /--
+-- error:
+-- ===================
+-- Found a counter-example!
+-- f := 1
+-- issue: ULift.up 1 = ULift.up 0 does not hold
+-- (1 shrinks)
+-- -------------------
+-- -/
+-- #guard_msgs in
+-- theorem ulift_nat (f : ULift.{1} Nat) : f = ⟨0⟩ := by
+--   plausible
+
+-- /--
+-- error:
+-- ===================
+-- Found a counter-example!
+-- α := "ULift Int"
+-- l := [0]
+-- issue: [ULift.up 0] = [ULift.up 0, ULift.up 0] does not hold
+-- (1 shrinks)
+-- -------------------
+-- -/
+-- #guard_msgs in
+-- theorem type_u (α : Type u) (l : List α) : l = l ++ l := by
+--   plausible