From b783879752444527a9710fd356c3314bc4d9b1cf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Apr 2023 08:45:11 -0700 Subject: [PATCH] #6687 --- src/tactic/core/elim_uncnstr_tactic.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 869716f59..a372a1f8b 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -804,6 +804,7 @@ class elim_uncnstr_tactic : public tactic { app * r = nullptr; expr* x, *y; if (uncnstr(args[0]) && num == 2 && + args[1]->get_ref_count() == 1 && m_seq_util.str.is_concat(args[1], x, y) && uncnstr(x)) { if (!mk_fresh_uncnstr_var_for(f, num, args, r))