diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 47c002de8..3420a3f99 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -168,6 +168,73 @@ private:
         if (mc && !(*mc)) *mc = alloc(generic_model_converter, m, "reduce-invertible");        
     }
 
+    bool is_full_domain_var(expr* v, rational& model) {
+        auto f = is_app(v) ? to_app(v)->get_decl() : nullptr;
+        if (!f || f->get_family_id() != m_bv.get_family_id() || f->get_arity() == 0)
+            return false;
+
+        switch (f->get_decl_kind()) {
+        case OP_BADD:
+        case OP_BSUB:
+        case OP_BSHL:
+        case OP_BASHR:
+        case OP_BLSHR:
+        case OP_BOR:
+            model = rational::zero();
+            return true;
+
+        case OP_BAND:
+            model = rational::power_of_two(m_bv.get_bv_size(v)) - rational::one();
+            return true;
+
+        case OP_BMUL:
+        case OP_BSDIV:
+        case OP_BSDIV0:
+        case OP_BSDIV_I:
+        case OP_BUDIV:
+        case OP_BUDIV0:
+        case OP_BUDIV_I:
+            model = rational::one();
+            return true;
+
+        default:
+            return false;
+        }
+    }
+
+    bool rewrite_unconstr(expr* v, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var) {
+        rational mdl;
+        if (!is_full_domain_var(v, mdl))
+            return false;
+
+        rational r;
+        app* a = to_app(v);
+        expr* fst_arg = a->get_arg(0);
+        bool fst_is_var = is_var(fst_arg);
+
+        for (unsigned i = 0, n = a->get_num_args(); i != n; ++i) {
+            auto arg = a->get_arg(i);
+            if (!m_parents[arg->get_id()].get() || is_var(arg) != fst_is_var)
+                return false;
+
+            if (fst_is_var && to_var(arg)->get_idx() >= max_var)
+                return false;
+
+            if (m_bv.is_numeral(arg, r) && r != mdl)
+                return false;
+        }
+
+        if (mc) {
+            ensure_mc(mc);
+            expr_ref num(m_bv.mk_numeral(mdl, get_sort(fst_arg)), m);
+            for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) {
+                (*mc)->add(a->get_arg(i), num);
+            }
+        }
+        new_v = fst_arg;
+        return true;
+    }
+
     // TBD: could be made to be recursive, by walking multiple layers of parents.
     
     bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) {
@@ -176,6 +243,20 @@ private:
         if (m_inverted.is_marked(p)) return false;
         if (mc && !is_ground(p)) return false;
 
+        if (m_bv.is_bv_xor(p) ||
+            m_bv.is_bv_not(p) ||
+            m_bv.is_bv_neg(p)) {
+            if (mc) {
+                ensure_mc(mc);
+                (*mc)->add(v, p);
+            }
+            new_v = v;
+            return true;
+        }
+
+        if (rewrite_unconstr(p, new_v, mc, max_var))
+            return true;
+
         if (m_bv.is_bv_add(p)) {
             if (mc) {
                 ensure_mc(mc);
@@ -191,25 +272,6 @@ private:
             return true;
         }
 
-        expr *a, *b;
-        // shift(a, b), where both a,b are single use. Set b = 0 and return a
-        if (m_bv.is_bv_shl(p, a, b) ||
-            m_bv.is_bv_ashr(p, a, b) ||
-            m_bv.is_bv_lshr(p, a, b)) {
-            if (!m_parents[(v == a ? b : a)->get_id()].get() || is_var(a) != is_var(b))
-                return false;
-
-            if (is_var(a) && to_var(v == a ? b : a)->get_idx() >= max_var)
-                return false;
-
-            if (mc) {
-                ensure_mc(mc);
-                (*mc)->add(b, m_bv.mk_numeral(rational::zero(), get_sort(b)));
-            }
-            new_v = a;
-            return true;
-        }
-
         if (m_bv.is_bv_mul(p)) {
             expr_ref rest(m);
             for (expr* arg : *to_app(p)) {
@@ -264,20 +326,9 @@ private:
             }
             return true;
         }
-        if (m_bv.is_bv_xor(p)) {
-            if (mc) {
-                ensure_mc(mc);
-                (*mc)->add(v, p);
-            }
-            new_v = v;
-            return true;
-        }
         if (m_bv.is_bv_sub(p)) {
             // TBD
         }
-        if (m_bv.is_bv_neg(p)) {
-            // TBD
-        }
         if (m_bv.is_bv_udivi(p)) {
             // TBD
         }