diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index bbe07f625..cd0f54503 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -126,7 +126,7 @@ struct enum2bv_rewriter::imp {
                 unsigned nc = m_dt.get_datatype_num_constructors(s);
                 result = m.mk_fresh_const(f->get_name().str().c_str(), m_bv.mk_sort(bv_size));
                 f_fresh = to_app(result)->get_decl();
-                if (!is_power_of_two(nc)) {
+                if (!is_power_of_two(nc) || nc == 1) {
                     m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size)));
                 }                
                 expr_ref f_def(m);
@@ -168,7 +168,7 @@ struct enum2bv_rewriter::imp {
                     unsigned bv_size = get_bv_size(s);
                     m_sorts.push_back(m_bv.mk_sort(bv_size));
                     unsigned nc = m_dt.get_datatype_num_constructors(s);
-                    if (!is_power_of_two(nc)) {
+                    if (!is_power_of_two(nc) || nc == 1) {
                         bounds.push_back(m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_bv.mk_numeral(nc-1, bv_size)));
                     }                
                     found = true;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 027790da8..fed6e71bc 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1111,8 +1111,8 @@ namespace smt {
 
         if (r1 == r2) {
             TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
-            return true;
-            // return false; // context is inconsistent
+            theory_id  t1 = r1->m_th_var_list.get_th_id();
+            return get_theory(t1)->use_diseqs();
         }
 
         // Propagate disequalities to theories
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index df3428ef3..33c4f8b61 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -251,15 +251,6 @@ Notes:
             return result;
         }
 
-#if 0
-        literal mk_and(literal_vector const& lits) {
-            if (lits.size() == 1) {
-                return lits[0];
-            }
-            
-        }
-#endif
-
         void mk_implies_or(literal l, unsigned n, literal const* xs) {
             literal_vector lits(n, xs);
             lits.push_back(ctx.mk_not(l));
@@ -346,28 +337,12 @@ Notes:
             ors.push_back(ex);                
             
             // result => xs[0] + ... + xs[n-1] <= 1
-#if 1
             for (unsigned i = 0; i < n; ++i) {
                 for (unsigned j = i + 1; j < n; ++j) {
                     add_clause(ctx.mk_not(result), ctx.mk_not(xs[i]), ctx.mk_not(xs[j]));
                 }
             }            
-#else
-            literal_vector atm;
-            for (unsigned i = 0; i < n; ++i) {
-                // at => !xs[1] & .. & !xs[i-1] & !xs[i+1] & ... & !xs[n-1] 
-                literal at = fresh();
-                for (unsigned j = 0; j < n; ++j) {
-                    if (i != j) {
-                        add_clause(ctx.mk_not(at), ctx.mk_not(xs[j]));
-                    }
-                }
-                atm.push_back(at);
-            }            
-            atm.push_back(ctx.mk_not(result));
-            add_clause(atm);
 
-#endif
             // xs[0] + ... + xs[n-1] <= 1 => and_x
             if (full) {
                 literal and_i = fresh();