From 431eade89481fe10054be83af27a89c9f4ca3ddb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Apr 2015 16:21:44 -0700 Subject: [PATCH] fix(library/tactic/inversion_tactic): incorrect use of optimization --- src/library/tactic/inversion_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 07fba1c70..a8c909cd8 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -182,8 +182,8 @@ class inversion_tac { for (unsigned i = fidx; i < args.size(); i++) { if (!is_local(args[i])) return false; // the indices must be local constants - for (unsigned j = fidx; j < i; j++) { - if (mlocal_name(args[j]) == mlocal_name(args[i])) + for (unsigned j = 0; j < i; j++) { + if (is_local(args[j]) && mlocal_name(args[j]) == mlocal_name(args[i])) return false; // the indices must be distinct local constants } }