diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 80d319377..63843d31e 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -323,6 +323,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
     
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
+        TRACE("bit_blaster", tout << f->get_name() << " ";
+              for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
+              tout << "\n";);
         if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) {
             mk_const(f, result);
             return BR_DONE;
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 72c0a447e..b41aa2238 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -828,6 +828,12 @@ void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * cons
 
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_rotate_left(unsigned sz, expr * const * a_bits, unsigned n, expr_ref_vector & out_bits) {
+    TRACE("bit_blaster", tout << n << ": " << sz << " ";
+          for (unsigned i = 0; i < sz; ++i) {
+              tout << mk_pp(a_bits[i], m()) << " ";
+          }
+          tout << "\n";
+          );
     n = n % sz;
     for (unsigned i = sz - n; i < sz; i++) 
         out_bits.push_back(a_bits[i]);
@@ -974,7 +980,7 @@ void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
                 mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
                 out = new_out;
             }
-            TRACE("bit_blaster_tpl<Cfg>", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
+            TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
             out_bits.set(sz - i - 1, out);
         }
     }
@@ -1004,7 +1010,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
             out = a_bits[i];
             for (unsigned j = 1; j < sz; j++) {
                 expr_ref new_out(m());
-                unsigned src = (Left ? (i - j) : (i + j)) % sz;
+                unsigned src = (Left ? (sz + i - j) : (i + j)) % sz;
                 mk_ite(eqs.get(j), a_bits[src], out, new_out);
                 out = new_out;
             }
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 11b09003b..1115663d2 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -21,6 +21,7 @@ Notes:
 #include"poly_rewriter_def.h"
 #include"ast_smt2_pp.h"
 
+
 mk_extract_proc::mk_extract_proc(bv_util & u):
     m_util(u),
     m_high(0),
diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp
index 5e66ab738..3b0ec8e5f 100644
--- a/src/smt/proto_model/datatype_factory.cpp
+++ b/src/smt/proto_model/datatype_factory.cpp
@@ -191,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) {
     // Approach 2)
     // For recursive datatypes.
     // search for constructor...
+    unsigned num_iterations = 0;
     if (m_util.is_recursive(s)) {
         while(true) {
+            ++num_iterations;
             TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
             ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
             ptr_vector<func_decl>::const_iterator it   = constructors->begin();
@@ -212,7 +214,13 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                           << found_sibling << "\n";);
                     if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
                         found_sibling = true;
-                        expr * maybe_new_arg = get_almost_fresh_value(s_arg);
+                        expr * maybe_new_arg = 0;
+                        if (num_iterations <= 1) {
+                            maybe_new_arg = get_almost_fresh_value(s_arg);
+                        }
+                        else {
+                            maybe_new_arg = get_fresh_value(s_arg);
+                        }
                         if (!maybe_new_arg) {
                             TRACE("datatype_factory", 
                                   tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
@@ -231,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                 if (found_sibling) {
                     expr_ref new_value(m_manager);
                     new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
+                    TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
                     m_last_fresh_value.insert(s, new_value);
                     if (!set->contains(new_value)) {
                         register_value(new_value);