diff --git a/.gitignore b/.gitignore
index 7cc289168..cc1c2a754 100644
--- a/.gitignore
+++ b/.gitignore
@@ -86,4 +86,3 @@ src/*/*/CMakeLists.txt
 src/*/*/*/CMakeLists.txt
 src/api/dotnet/cmake_install_gac.cmake.in
 src/api/dotnet/cmake_uninstall_gac.cmake.in
-
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 244594461..f2d177041 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -55,8 +55,8 @@ public:
     virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg);
     virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec);
     virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits);
-    virtual format_ns::format * pp_string_literal(app * t);
     virtual format_ns::format * pp_datalog_literal(app * t);
+    virtual format_ns::format * pp_string_literal(app * t);
     virtual format_ns::format * pp_sort(sort * s);
     virtual format_ns::format * pp_fdecl_ref(func_decl * f);
     format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len) const;
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index f41350dc5..706f65ac4 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -406,7 +406,6 @@ class smt_printer {
 
     void visit_app(app* n) {
         rational val;
-        const char *str;
         bool is_int, pos;
         buffer<symbol> names;
         unsigned bv_size;
diff --git a/src/ast/rewriter/rewriter.txt b/src/ast/rewriter/rewriter.txt
index a7a9e5eff..9eb016af2 100644
--- a/src/ast/rewriter/rewriter.txt
+++ b/src/ast/rewriter/rewriter.txt
@@ -8,7 +8,6 @@ The following classes implement theory specific rewriting rules:
   - datatype_rewriter
   - fpa_rewriter
   - seq_rewriter
-  - str_rewriter
 
 Each of them provide the method
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result)
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 491aca8ba..1486f6e6c 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -66,8 +66,7 @@ namespace smt2 {
 
         scoped_ptr<bv_util>               m_bv_util;
         scoped_ptr<arith_util>            m_arith_util;
-        scoped_ptr<seq_util>              m_seq_util;
-      
+        scoped_ptr<seq_util>              m_seq_util;      
         scoped_ptr<pattern_validator>     m_pattern_validator;
         scoped_ptr<var_shifter>           m_var_shifter;
 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 68a9f980d..535ae3b1e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1714,12 +1714,6 @@ namespace smt {
         for (unsigned i = 0; i < m_th_eq_propagation_queue.size() && !inconsistent(); i++) {
             new_th_eq curr = m_th_eq_propagation_queue[i];
             theory * th = get_theory(curr.m_th_id);
-            TRACE("t_str_eq_bug", tout
-                    << "th->name = " << th->get_name() << std::endl
-                    << "m_th_id = " << curr.m_th_id << std::endl
-                    << "m_lhs = " << curr.m_lhs << std::endl
-                    << "m_rhs = " << curr.m_rhs << std::endl
-                    << std::endl;);
             SASSERT(th);
             th->new_eq_eh(curr.m_lhs, curr.m_rhs);
 #ifdef Z3DEBUG
@@ -3042,6 +3036,7 @@ namespace smt {
         // not counting any literals that get assigned by this method
         // this relies on bcp() to give us its old m_qhead and therefore
         // bcp() should always be called before this method
+	
         unsigned assigned_literal_end = m_assigned_literals.size();
         for (; qhead < assigned_literal_end; ++qhead) {
             literal l = m_assigned_literals[qhead];
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index 7dd2819e4..67091c601 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -185,6 +185,14 @@ namespace smt {
         virtual void add_theory_assumptions(expr_ref_vector & assumptions) {
         }
 
+        /**
+           \brief This method is called from the smt_context when an unsat core is generated.
+           The theory may change the answer to UNKNOWN by returning l_undef from this method.
+        */
+        virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) {
+            return l_false;
+        }
+	
         /**
            \brief This method is invoked before the search starts.
         */
@@ -200,14 +208,6 @@ namespace smt {
             return FC_DONE;
         }
 
-        /**
-           \brief This method is called from the smt_context when an unsat core is generated.
-           The theory may change the answer to UNKNOWN by returning l_undef from this method.
-        */
-        virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) {
-            return l_false;
-        }
-
         /**
            \brief Parametric theories (e.g. Arrays) should implement this method.
            See example in context::is_shared