diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp
index 70c8a6ebe..fa0a26f25 100644
--- a/src/ast/str_decl_plugin.cpp
+++ b/src/ast/str_decl_plugin.cpp
@@ -33,6 +33,9 @@ str_decl_plugin::~str_decl_plugin(){
 void str_decl_plugin::finalize(void) {
     #define DEC_REF(decl) if (decl) { m_manager->dec_ref(decl); } ((void) 0)
     DEC_REF(m_str_decl);
+    DEC_REF(m_concat_decl);
+    DEC_REF(m_length_decl);
+    DEC_REF(m_int_sort);
 }
 
 void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
@@ -41,11 +44,19 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m->inc_ref(m_str_decl);
     sort * s = m_str_decl;
 
+    m_arith_fid = m_manager->mk_family_id("arith");
+    m_int_sort = m_manager->mk_sort(m_arith_fid, INT_SORT);
+    SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before str_decl_plugin.
+    m_manager->inc_ref(m_int_sort);
+    sort * i = m_int_sort;
+
 #define MK_OP(FIELD, NAME, KIND, SORT)                                                  \
     FIELD = m->mk_func_decl(symbol(NAME), SORT, SORT, SORT, func_decl_info(id, KIND));  \
     m->inc_ref(FIELD)
 
     MK_OP(m_concat_decl, "Concat", OP_STRCAT, s);
+
+    m_length_decl = m->mk_func_decl(symbol("Length"), s, i); m_manager->inc_ref(m_length_decl);
 }
 
 decl_plugin * str_decl_plugin::mk_fresh() {
@@ -62,6 +73,7 @@ sort * str_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
 func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
     switch(k) {
     case OP_STRCAT: return m_concat_decl;
+    case OP_STRLEN: return m_length_decl;
     default: return 0;
     }
 }
@@ -88,6 +100,7 @@ app * str_decl_plugin::mk_string(const char * val) {
 
 void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
     op_names.push_back(builtin_name("Concat", OP_STRCAT));
+    op_names.push_back(builtin_name("Length", OP_STRLEN));
 }
 
 void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h
index d190e9ff7..3fd5fb7e6 100644
--- a/src/ast/str_decl_plugin.h
+++ b/src/ast/str_decl_plugin.h
@@ -18,6 +18,7 @@ Revision History:
 #define _STR_DECL_PLUGIN_H_
 
 #include"ast.h"
+#include"arith_decl_plugin.h"
 
 enum str_sort_kind {
    STRING_SORT,
@@ -27,6 +28,7 @@ enum str_op_kind {
     OP_STR, /* string constants */
     //
     OP_STRCAT,
+    OP_STRLEN,
     LAST_STR_OP
 };
 
@@ -35,7 +37,11 @@ protected:
     symbol m_strv_sym;
     sort * m_str_decl;
 
+    sort *              m_int_sort;
+    family_id           m_arith_fid;
+
     func_decl * m_concat_decl;
+    func_decl * m_length_decl;
 
     virtual void set_manager(ast_manager * m, family_id id);
 
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index bc1b59551..2bf67ed81 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -31,7 +31,7 @@ theory_str::~theory_str() {
 
 bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
     // TODO I have no idea if this is correct.
-    TRACE("t_str", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
+    TRACE("t_str", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << std::endl;);
     SASSERT(atom->get_family_id() == get_family_id());
 
     ast_manager & m = get_manager();
@@ -54,7 +54,7 @@ bool theory_str::internalize_term(app * term) {
     // TODO I have no idea if this is correct either.
     ast_manager & m = get_manager();
     context & ctx = get_context();
-    TRACE("t_str", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
+    TRACE("t_str", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << std::endl;);
     SASSERT(term->get_family_id() == get_family_id());
     SASSERT(!ctx.e_internalized(term));
 
@@ -80,6 +80,20 @@ void theory_str::attach_new_th_var(enode * n) {
     TRACE("t_str_detail", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);
 }
 
+void theory_str::init_search_eh() {
+    ast_manager & m = get_manager();
+    context & ctx = get_context();
+    TRACE("t_str",
+        tout << "search started, assignments are:" << std::endl;
+        expr_ref_vector assignment(m);
+        ctx.get_assignments(assignment);
+        for (expr_ref_vector::iterator i = assignment.begin(); i != assignment.end(); ++i) {
+            expr * ex = *i;
+            tout << mk_ismt2_pp(ex, m) << std::endl;
+        }
+    );
+}
+
 void theory_str::new_eq_eh(theory_var x, theory_var y) {
     // TODO
     TRACE("t_str", tout << "new eq: " << x << " = " << y << std::endl;);
@@ -94,4 +108,23 @@ void theory_str::new_diseq_eh(theory_var x, theory_var y) {
                                   mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
 }
 
+void theory_str::relevant_eh(app * n) {
+    TRACE("t_str", tout << "relevant: " << mk_ismt2_pp(n, get_manager()) << "\n";);
+}
+
+void theory_str::assign_eh(bool_var v, bool is_true) {
+    context & ctx = get_context();
+    TRACE("t_str", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
+}
+
+void theory_str::push_scope_eh() {
+    TRACE("t_str", tout << "push" << std::endl;);
+}
+
+final_check_status theory_str::final_check_eh() {
+    // TODO
+    TRACE("t_str", tout << "final check" << std::endl;);
+    return FC_DONE;
+}
+
 }; /* namespace smt */
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 7bb5b5148..5ee5502de 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -38,6 +38,14 @@ namespace smt {
         virtual void new_eq_eh(theory_var, theory_var);
         virtual void new_diseq_eh(theory_var, theory_var);
         virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager()); }
+
+        virtual void init_search_eh();
+
+        virtual void relevant_eh(app * n);
+        virtual void assign_eh(bool_var v, bool is_true);
+        virtual void push_scope_eh();
+
+        virtual final_check_status final_check_eh();
     public:
         theory_str(ast_manager& m);
         virtual ~theory_str();