From 1a70ac75df70fb02229d3eebd496721e9d7844e5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Apr 2023 09:01:17 -0700 Subject: [PATCH] fix #6687 --- src/ast/converters/expr_inverter.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp index 4d435f7e8f0..0ee3e130d30 100644 --- a/src/ast/converters/expr_inverter.cpp +++ b/src/ast/converters/expr_inverter.cpp @@ -757,6 +757,7 @@ class seq_expr_inverter : public iexpr_inverter { expr* x, *y; if (uncnstr(args[0]) && num == 2 && + args[1]->get_ref_count() == 1 && seq.str.is_concat(args[1], x, y) && uncnstr(x)) { mk_fresh_uncnstr_var_for(f, r);