From a498a64490904bf90050472712fe279d10a4888e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 May 2021 21:27:58 -0700 Subject: [PATCH] chore: disable injectivity theorems generation for big structure tests The test was producing a stack overflow in debug mode in CI. --- tests/compiler/bigctor.lean | 1 + tests/lean/run/bigctor.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/tests/compiler/bigctor.lean b/tests/compiler/bigctor.lean index 1206779290..84bd189bf8 100644 --- a/tests/compiler/bigctor.lean +++ b/tests/compiler/bigctor.lean @@ -1,3 +1,4 @@ +set_option genInjectivity false structure Foo where x1 : Nat := 0 x2 : Nat := 0 diff --git a/tests/lean/run/bigctor.lean b/tests/lean/run/bigctor.lean index b14a8e8b2c..fd8d32b2c0 100644 --- a/tests/lean/run/bigctor.lean +++ b/tests/lean/run/bigctor.lean @@ -1,3 +1,4 @@ +set_option genInjectivity false structure Foo where x1 : Nat := 0 x2 : Nat := 0