From 398b9c136a65f09b0ce136d1e5dad26ff9a3473a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Feb 2022 11:42:49 -0800 Subject: [PATCH] chore: fix test --- tests/lean/906.lean.expected.out | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/lean/906.lean.expected.out b/tests/lean/906.lean.expected.out index bee17bbe5f..10ea7227c2 100644 --- a/tests/lean/906.lean.expected.out +++ b/tests/lean/906.lean.expected.out @@ -1,2 +1,3 @@ 906.lean:7:14-7:19: warning: declaration uses 'sorry' -906.lean:12:2-12:28: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (50000) has been reached (use 'set_option maxHeartbeats ' to set the limit) +906.lean:12:2-12:28: error: tactic 'simp' failed, nested error: +(deterministic) timeout at 'whnf', maximum number of heartbeats (50000) has been reached (use 'set_option maxHeartbeats ' to set the limit)