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);