diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 370e639b9..63092b2cf 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -277,7 +277,9 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_NON_NULL(f, 0);
         expr * e = to_func_interp_ref(f)->get_else();
-        mk_c(c)->save_ast_trail(e);
+        if (e) {
+            mk_c(c)->save_ast_trail(e);
+        }
         RETURN_Z3(of_expr(e));
         Z3_CATCH_RETURN(0);
     }
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h
index ea8209c61..b812de941 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h
@@ -121,8 +121,11 @@ public:
     void mk_comp(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
 
     void mk_carry_save_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr * const * c_bits, expr_ref_vector & sum_bits, expr_ref_vector & carry_bits);
-    void mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
+    bool mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
+    bool mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
+    void mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits);
 
+    bool is_bool_const(expr* e) const { return m().is_true(e) || m().is_false(e); }
     void mk_abs(unsigned sz, expr * const * a_bits, expr_ref_vector & out_bits);
 };
 
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 38a608f5f..942f97e93 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -38,7 +38,7 @@ void bit_blaster_tpl<Cfg>::checkpoint() {
 template<typename Cfg>
 bool bit_blaster_tpl<Cfg>::is_numeral(unsigned sz, expr * const * bits) const {
     for (unsigned i = 0; i < sz; i++)
-        if (!m().is_true(bits[i]) && !m().is_false(bits[i]))
+        if (!is_bool_const(bits[i])) 
             return false;
     return true;
 }
@@ -158,30 +158,24 @@ void bit_blaster_tpl<Cfg>::mk_subtracter(unsigned sz, expr * const * a_bits, exp
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
     SASSERT(sz > 0);
-    
-    if (!m_use_bcm) {
-        numeral n_a, n_b;
-        if (is_numeral(sz, a_bits, n_b))
-            std::swap(a_bits, b_bits);
-        if (is_minus_one(sz, b_bits)) {
-            mk_neg(sz, a_bits, out_bits);
-            return;
-        }
-        if (is_numeral(sz, a_bits, n_a)) {
-            n_a *= n_b;
-            num2bits(n_a, sz, out_bits);
-            return;
-        }
+    numeral n_a, n_b;
+    if (is_numeral(sz, a_bits, n_b))
+        std::swap(a_bits, b_bits);
+    if (is_minus_one(sz, b_bits)) {
+        mk_neg(sz, a_bits, out_bits);
+        return;
     }
-    else {
-        numeral n_a, n_b;
-        if (is_numeral(sz, a_bits, n_a)) {
-            mk_const_multiplier(sz, a_bits, b_bits, out_bits);
-            return;
-        } else if (is_numeral(sz, b_bits, n_b)) {
-            mk_const_multiplier(sz, b_bits, a_bits, out_bits);
-            return;
-        }
+    if (is_numeral(sz, a_bits, n_a)) {
+        n_a *= n_b;
+        num2bits(n_a, sz, out_bits);
+        return;
+    }
+    
+    if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
+        return;
+    }
+    if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) {
+        return;
     }
 
     if (!m_use_wtm) {
@@ -1171,13 +1165,74 @@ void bit_blaster_tpl<Cfg>::mk_carry_save_adder(unsigned sz, expr * const * a_bit
 }
 
 template<typename Cfg>
-void bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
-    DEBUG_CODE({
-        numeral x;
-        SASSERT(is_numeral(sz, a_bits, x));
-        SASSERT(out_bits.empty());        
-    });    
+bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
+    unsigned nb = 0;
+    unsigned case_size = 1;
+    unsigned circuit_size = sz*sz*5;
+    for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) {
+        if (!is_bool_const(a_bits[i])) {
+            case_size *= 2;
+        }
+        if (!is_bool_const(b_bits[i])) {
+            case_size *= 2;
+        }
+    }
+    if (case_size >= circuit_size) {
+        return false;
+    }
+    SASSERT(out_bits.empty());
     
+    ptr_buffer<expr, 128> na_bits;
+    na_bits.append(sz, a_bits);
+    ptr_buffer<expr, 128> nb_bits;
+    nb_bits.append(sz, b_bits);
+    mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits); 
+    return false;
+}
+ 
+template<typename Cfg>
+void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits) {
+    while (is_a && i < sz && is_bool_const(a_bits[i])) ++i;
+    if (is_a && i == sz) { is_a = false; i = 0; }
+    while (!is_a && i < sz && is_bool_const(b_bits[i])) ++i;
+    if (i < sz) {
+        expr_ref_vector out1(m()), out2(m());
+        expr_ref x(m());
+        x = is_a?a_bits[i]:b_bits[i];
+        if (is_a) a_bits[i] = m().mk_true(); else b_bits[i] = m().mk_true();
+        mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out1);
+        if (is_a) a_bits[i] = m().mk_false(); else b_bits[i] = m().mk_false();
+        mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out2);
+        if (is_a) a_bits[i] = x; else b_bits[i] = x;
+        SASSERT(out_bits.empty());
+        for (unsigned j = 0; j < sz; ++j) {
+            out_bits.push_back(m().mk_ite(x, out1[j].get(), out2[j].get()));
+        }        
+    }
+    else {
+        numeral n_a, n_b;
+        SASSERT(i == sz && !is_a);
+        VERIFY(is_numeral(sz, a_bits.c_ptr(), n_a));
+        VERIFY(is_numeral(sz, b_bits.c_ptr(), n_b));
+        n_a *= n_b;
+        num2bits(n_a, sz, out_bits);
+    }
+}
+
+template<typename Cfg>
+bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
+    numeral n_a;
+    if (!is_numeral(sz, a_bits, n_a)) {
+        return false;
+    }
+    SASSERT(out_bits.empty());
+    
+    if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
+        return true;
+    }    
+    if (!m_use_bcm) {
+        return false;
+    }
     expr_ref_vector minus_b_bits(m()), tmp(m());
     mk_neg(sz, b_bits, minus_b_bits);
         
@@ -1255,4 +1310,6 @@ void bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
 
     TRACE("bit_blaster_tpl_booth", for (unsigned i=0; i<out_bits.size(); i++)
                                      tout << "Booth encoding: " << mk_pp(out_bits[i].get(), m()) << "\n"; );
+
+    return true;
 }
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index fd7c60a57..c571a5c56 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1968,7 +1968,63 @@ void bv_rewriter::mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & r
         result = m().mk_eq(t1, m_util.mk_bv_sub(c, t2));
 }
 
+#include "ast_pp.h"
+
+bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) {
+    if (!m_util.is_numeral(lhs) || !is_add(rhs)) {
+        std::swap(lhs, rhs);
+    }
+    if (!m_util.is_numeral(lhs) || !is_add(rhs)) {
+        return false;
+    }
+    unsigned sz = to_app(rhs)->get_num_args();
+    expr_ref t1(m()), t2(m());
+    t1 = to_app(rhs)->get_arg(0);
+    if (sz > 2) {
+        t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1);
+    }
+    else {
+        SASSERT(sz == 2);
+        t2 = to_app(rhs)->get_arg(1);
+    }
+    mk_t1_add_t2_eq_c(t1, t2, lhs, result);
+    return true;
+}
+
+bool bv_rewriter::is_add_mul_const(expr* e) const {
+    if (!m_util.is_bv_add(e)) {
+        return false;
+    }
+    unsigned num = to_app(e)->get_num_args();
+    for (unsigned i = 0; i < num; i++) {
+        expr * arg = to_app(e)->get_arg(i);
+        expr * c2, * x2;
+        if (m_util.is_numeral(arg))
+            continue;
+        if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2))
+            continue;
+        return false;
+    }
+    return true;
+}
+
+bool bv_rewriter::is_concat_target(expr* lhs, expr* rhs) const {
+    return
+        m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs))) ||
+        m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs)));
+}
+
+bool bv_rewriter::has_numeral(app* a) const {
+    for (unsigned i = 0; i < a->get_num_args(); ++i) {
+        if (is_numeral(a->get_arg(i))) {
+            return true;
+        }
+    }
+    return false;
+}
+
 br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
+        
     expr * c, * x;
     numeral c_val, c_inv_val;
     unsigned sz;
@@ -2001,24 +2057,30 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
 
         // c * x =  t_1 + ... + t_n
         // and t_i's have non-unary coefficients (this condition is used to make sure we are actually reducing the number of multipliers).
-        if (m_util.is_bv_add(rhs)) {
+        if (is_add_mul_const(rhs)) {
             // Potential problem: this simplification may increase the number of adders by reducing the amount of sharing.
-            unsigned num = to_app(rhs)->get_num_args();
-            unsigned i;
-            for (i = 0; i < num; i++) {
-                expr * arg = to_app(rhs)->get_arg(i);
-                expr * c2, * x2;
-                if (m_util.is_numeral(arg))
-                    continue;
-                if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2))
-                    continue;
-                break;
-            }
-            if (i == num) {
-                result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs));
-                return BR_REWRITE2;
+            result = m().mk_eq(x, m_util.mk_bv_mul(m_util.mk_numeral(c_inv_val, sz), rhs));
+            return BR_REWRITE2;
+        }
+    }
+    if (m_util.is_numeral(lhs, c_val, sz) && is_add_mul_const(rhs)) {
+        unsigned sz = to_app(rhs)->get_num_args();
+        unsigned i = 0;
+        expr* c2, *x2;
+        numeral c2_val, c2_inv_val;
+        bool found = false;
+        for (; !found && i < sz; ++i) {
+            expr* arg = to_app(rhs)->get_arg(i);
+            if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) &&
+                m_util.mult_inverse(c2_val, sz, c2_inv_val)) {
+                found = true;
             }
         }
+        if (found) {
+            result = m().mk_eq(m_util.mk_numeral(c2_inv_val*c_val, sz), 
+                               m_util.mk_bv_mul(m_util.mk_numeral(c2_inv_val, sz), rhs));
+            return BR_REWRITE3;
+        }
     }
     return BR_FAILED;
 }
@@ -2065,9 +2127,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             return st;
     }
 
+    expr_ref new_lhs(m());
+    expr_ref new_rhs(m());
+
     if (m_util.is_bv_add(lhs) || m_util.is_bv_mul(lhs) || m_util.is_bv_add(rhs) || m_util.is_bv_mul(rhs)) {
-        expr_ref new_lhs(m());
-        expr_ref new_rhs(m());
         st = cancel_monomials(lhs, rhs, false, new_lhs, new_rhs);
         if (st != BR_FAILED) {
             if (is_numeral(new_lhs) && is_numeral(new_rhs)) {
@@ -2080,28 +2143,27 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             new_rhs = rhs;
         }
         
+        lhs = new_lhs;
+        rhs = new_rhs;
         // Try to rewrite t1 + t2 = c --> t1 = c - t2   
         // Reason: it is much cheaper to bit-blast.
-        expr * t1, * t2;
-        if (m_util.is_bv_add(new_lhs, t1, t2) && is_numeral(new_rhs)) {
-            mk_t1_add_t2_eq_c(t1, t2, new_rhs, result);
+        if (isolate_term(lhs, rhs, result)) {
             return BR_REWRITE2;
         }
-        if (m_util.is_bv_add(new_rhs, t1, t2) && is_numeral(new_lhs)) {
-            mk_t1_add_t2_eq_c(t1, t2, new_lhs, result);
-            return BR_REWRITE2;
+        if (is_concat_target(lhs, rhs)) {
+            return mk_eq_concat(lhs, rhs, result);
         }
-        
+
         if (st != BR_FAILED) {
-            result = m().mk_eq(new_lhs, new_rhs); 
+            result = m().mk_eq(lhs, rhs); 
             return BR_DONE;
         }
     }
 
-    if ((m_util.is_concat(lhs) && is_concat_split_target(rhs)) || 
-        (m_util.is_concat(rhs) && is_concat_split_target(lhs)))
+    if (is_concat_target(lhs, rhs)) {
         return mk_eq_concat(lhs, rhs, result);
-   
+    }
+
     if (swapped) {
         result = m().mk_eq(lhs, rhs);
         return BR_DONE;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 1c9b44b52..78d3fb4f1 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -137,6 +137,10 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool is_concat_split_target(expr * t) const;
 
     br_status mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result);
+    bool is_add_mul_const(expr* e) const;
+    bool isolate_term(expr* lhs, expr* rhs, expr_ref & result);
+    bool has_numeral(app* e) const;
+    bool is_concat_target(expr* lhs, expr* rhs) const;
 
     void updt_local_params(params_ref const & p);
 
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 51b2c1b59..cef8d5fc7 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -424,6 +424,39 @@ namespace smt {
 
     };
 
+    void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) {
+        ++m_stats.m_num_eq_dynamic;
+        if (v1 > v2) {
+            std::swap(v1, v2);
+        }
+        unsigned sz = get_bv_size(v1);
+        ast_manager& m = get_manager();
+        context & ctx = get_context();
+        app* o1 = get_enode(v1)->get_owner();
+        app* o2 = get_enode(v2)->get_owner();
+        literal oeq = mk_eq(o1, o2, true);
+        TRACE("bv", 
+              tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " " 
+              << ctx.get_scope_level() << "\n";);
+        literal_vector eqs;
+        for (unsigned i = 0; i < sz; ++i) {
+            literal l1 = m_bits[v1][i];
+            literal l2 = m_bits[v2][i];
+            expr_ref e1(m), e2(m);
+            e1 = mk_bit2bool(o1, i);
+            e2 = mk_bit2bool(o2, i);
+            literal eq = mk_eq(e1, e2, true);
+            ctx.mk_th_axiom(get_id(),  l1, ~l2, ~eq);
+            ctx.mk_th_axiom(get_id(), ~l1,  l2, ~eq);
+            ctx.mk_th_axiom(get_id(),  l1,  l2,  eq);
+            ctx.mk_th_axiom(get_id(), ~l1, ~l2,  eq);
+            ctx.mk_th_axiom(get_id(), eq, ~oeq);
+            eqs.push_back(~eq);
+        }
+        eqs.push_back(oeq);
+        ctx.mk_th_axiom(get_id(), eqs.size(), eqs.c_ptr());
+    }
+
     void theory_bv::fixed_var_eh(theory_var v) {
         numeral val;
         bool r      = get_fixed_value(v, val);
@@ -443,7 +476,9 @@ namespace smt {
                           display_var(tout, v);
                           display_var(tout, v2););
                     m_stats.m_num_th2core_eq++;
-                    ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
+                    add_fixed_eq(v, v2);
+                    ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));                    
+                    m_fixed_var_table.insert(key, v2);
                 }
             }
             else {
@@ -1177,6 +1212,7 @@ namespace smt {
     }
 
     void theory_bv::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
+
         m_stats.m_num_bit2core++;
         context & ctx = get_context();
         SASSERT(ctx.get_assignment(antecedent) == l_true);
@@ -1192,6 +1228,12 @@ namespace smt {
         }
         else {
             ctx.assign(consequent, mk_bit_eq_justification(v1, v2, consequent, antecedent));
+            literal_vector lits;
+            lits.push_back(~consequent);
+            lits.push_back(antecedent);
+            lits.push_back(~mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false));
+            ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+     
             if (m_wpos[v2] == idx)
                 find_wpos(v2);
             // REMARK: bit_eq_justification is marked as a theory_bv justification.
@@ -1601,6 +1643,7 @@ namespace smt {
         st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
         st.update("bv bit2core", m_stats.m_num_bit2core);
         st.update("bv->core eq", m_stats.m_num_th2core_eq);
+        st.update("bv dynamic eqs", m_stats.m_num_eq_dynamic);
     }
 
 #ifdef Z3DEBUG
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index bb0dcc907..17d03b412 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -34,6 +34,7 @@ namespace smt {
     
     struct theory_bv_stats {
         unsigned   m_num_diseq_static, m_num_diseq_dynamic, m_num_bit2core, m_num_th2core_eq, m_num_conflicts;
+        unsigned   m_num_eq_dynamic;
         void reset() { memset(this, 0, sizeof(theory_bv_stats)); }
         theory_bv_stats() { reset(); }
     };
@@ -124,8 +125,9 @@ namespace smt {
         typedef std::pair<numeral, unsigned> value_sort_pair;
         typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
         typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
-        value2var                m_fixed_var_table;
 
+        value2var                m_fixed_var_table;
+        
         literal_vector           m_tmp_literals;
         svector<var_pos>         m_prop_queue;
         bool                     m_approximates_large_bvs;
@@ -166,6 +168,7 @@ namespace smt {
         void find_wpos(theory_var v);
         friend class fixed_eq_justification;
         void fixed_var_eh(theory_var v);
+        void add_fixed_eq(theory_var v1, theory_var v2);
         bool get_fixed_value(theory_var v, numeral & result) const;
         void internalize_num(app * n);
         void internalize_add(app * n);
diff --git a/src/tactic/bv/bit_blaster_tactic.h b/src/tactic/bv/bit_blaster_tactic.h
index cb7f6f7a9..d840154b9 100644
--- a/src/tactic/bv/bit_blaster_tactic.h
+++ b/src/tactic/bv/bit_blaster_tactic.h
@@ -1,32 +1,33 @@
-/*++
+ /*++
 Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
+ 
+ Module Name:
+ 
     bit_blaster_tactic.h
-
-Abstract:
-
+ 
+ Abstract:
+ 
     Apply bit-blasting to a given goal.
-
-Author:
-
+ 
+ Author:
+ 
     Leonardo (leonardo) 2011-10-25
-
-Notes:
-
---*/
+ 
+ Notes:
+ 
+ --*/
 #ifndef BIT_BLASTER_TACTIC_H_
 #define BIT_BLASTER_TACTIC_H_
-
-#include"params.h"
-#include"bit_blaster_rewriter.h"
-class ast_manager;
-class tactic;
-
+ 
+ #include"params.h"
+ #include"bit_blaster_rewriter.h"
+ class ast_manager;
+ class tactic;
+ 
 tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p = params_ref());
 tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p = params_ref());
-/*
+ /*
   ADD_TACTIC("bit-blast", "reduce bit-vector expressions into SAT.", "mk_bit_blaster_tactic(m, p)")
-*/
-#endif
+ */
+ #endif
+
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index f1ffe4b53..e436d19c4 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -22,7 +22,7 @@ Revision History:
 #include"occurs.h"
 #include"cooperate.h"
 #include"goal_shared_occs.h"
-#include"ast_smt2_pp.h"
+#include"ast_pp.h"
 
 class solve_eqs_tactic : public tactic {
     struct imp {
@@ -92,21 +92,23 @@ class solve_eqs_tactic : public tactic {
         }
         
         // Use: (= x def) and (= def x)
-        bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
+
+        bool trivial_solve1(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) { 
+
             if (is_uninterp_const(lhs) && !m_candidate_vars.is_marked(lhs) && !occurs(lhs, rhs) && check_occs(lhs)) {
                 var = to_app(lhs); 
                 def = rhs;
                 pr  = 0;
                 return true;
             }
-            else if (is_uninterp_const(rhs) && !m_candidate_vars.is_marked(rhs) && !occurs(rhs, lhs) && check_occs(rhs)) {
-                var = to_app(rhs);
-                def = lhs;
-                if (m_produce_proofs)
-                    pr = m().mk_commutativity(m().mk_eq(lhs, rhs));
-                return true;
+            else {
+                return false;
             }
-            return false;
+        }
+        bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
+            return 
+                trivial_solve1(lhs, rhs, var, def, pr) ||
+                trivial_solve1(rhs, lhs, var, def, pr);
         }
         
         // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))