fix #6687

Z3Prover · Apr 13, 2023 · 1a70ac7 · 1a70ac7
1 parent b783879
commit 1a70ac7
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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);