diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
index e2d6f0255..8bb316dfc 100644
--- a/src/ast/converters/expr_inverter.cpp
+++ b/src/ast/converters/expr_inverter.cpp
@@ -790,17 +790,16 @@ public:
                 r = m.mk_or(r, emp);
                 return true;
             }
-            if (uncnstr(args[1])) {
+            if (uncnstr(args[1]) && seq.is_string(args[0]->get_sort())) {
                 // x contains y -> r
-                // y -> if r then x else x + x
+                // y -> if r then x else x + x + a
                 mk_fresh_uncnstr_var_for(f, r);
                 if (m_mc)
-                    add_def(args[1], m.mk_ite(r, args[0], seq.str.mk_concat(args[0], args[0])));
+                    add_def(args[1], m.mk_ite(r, args[0], seq.str.mk_concat(args[0], args[0], seq.str.mk_string(zstring("a")))));
                 return true;
             }
             return false;
         default:
-            verbose_stream() << f->get_name() << "\n";
             return false;                
             
         }
diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
index 073e5bc96..d5d597647 100644
--- a/src/ast/sls/sls_smt_plugin.h
+++ b/src/ast/sls/sls_smt_plugin.h
@@ -33,7 +33,7 @@ namespace sls {
         virtual void set_value(expr* t, expr* v) = 0;
         virtual void force_phase(sat::literal lit) = 0;
         virtual void set_has_new_best_phase(bool b) = 0;
-        virtual bool get_value(expr* v, expr_ref& val) = 0;
+        virtual bool get_smt_value(expr* v, expr_ref& val) = 0;
         virtual bool get_best_phase(sat::bool_var v) = 0;
         virtual expr* bool_var2expr(sat::bool_var v) = 0;
         virtual void inc_activity(sat::bool_var v, double inc) = 0;
diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h
index 0378f5845..a9fedf4d1 100644
--- a/src/sat/smt/sls_solver.h
+++ b/src/sat/smt/sls_solver.h
@@ -101,10 +101,10 @@ namespace sls {
         void inc_activity(sat::bool_var v, double inc) override {}
         unsigned get_num_bool_vars() const override;
         bool parallel_mode() const override { return false; }
-        bool get_value(expr* v, expr_ref& value) override { return false; }
+        bool get_smt_value(expr* v, expr_ref& value) override { return false; }
         
     };
 
 }
 
-#endif
\ No newline at end of file
+#endif
diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
index d57b35945..db1aa204d 100644
--- a/src/smt/theory_sls.h
+++ b/src/smt/theory_sls.h
@@ -110,8 +110,9 @@ namespace smt {
         void set_finished() override;
         unsigned get_num_bool_vars() const override;
         void inc_activity(sat::bool_var v, double inc) override;
-        bool parallel_mode() const { return m_parallel_mode; }
-        bool get_value(expr* v, expr_ref& value) override;
+        bool parallel_mode() const override { return m_parallel_mode; }
+        bool get_smt_value(expr* v, expr_ref& value) override;
+
     };
 
 }