From 1ab39a518fc0c928f9e089ba14aa3ffcef89518e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Nov 2015 11:25:45 -0700 Subject: [PATCH] chore(tests/lean/run/blast_ematch5): disable unnecessary options --- tests/lean/run/blast_ematch5.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/tests/lean/run/blast_ematch5.lean b/tests/lean/run/blast_ematch5.lean index 6c40bab8e..a5ab2f053 100644 --- a/tests/lean/run/blast_ematch5.lean +++ b/tests/lean/run/blast_ematch5.lean @@ -3,7 +3,13 @@ constant subt : nat → nat → Prop lemma subt_trans [forward] {a b c : nat} : subt a b → subt b c → subt a c := sorry -set_option blast.ematch true +set_option blast.init_depth 20 +set_option blast.inc_depth 100 +set_option blast.ematch true +set_option blast.simp false +-- TODO(Leo): check if unit propagation is still buggy +-- If I remove the following option, blast fails +set_option blast.backward true -- false example (a b c d : nat) : subt a b → subt b c → subt c d → subt a d := by blast