diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp
index 701e531b1..fe7134c3f 100644
--- a/src/ast/finite_set_decl_plugin.cpp
+++ b/src/ast/finite_set_decl_plugin.cpp
@@ -233,14 +233,25 @@ bool finite_set_decl_plugin::is_value(app * e) const {
             continue;
         }
         
+        bool is_setop = 
+            is_app_of(a, m_family_id, OP_FINITE_SET_UNION) 
+            || is_app_of(a, m_family_id, OP_FINITE_SET_INTERSECT)
+            || is_app_of(a, m_family_id, OP_FINITE_SET_DIFFERENCE);
         // Check if it's a union
-        if (is_app_of(a, m_family_id, OP_FINITE_SET_UNION)) {
+        if (is_setop) {
             // Add arguments to todo list
             for (auto arg : *a) 
                 todo.push_back(arg);            
             continue;
         }
 
+        if (is_app_of(a, m_family_id, OP_FINITE_SET_RANGE)) {
+            for (auto arg : *a)
+                if (!m_manager->is_value(arg))
+                    return false;
+            continue;
+        }
+
         // can add also ranges where lo and hi are values.
         
         // If it's none of the above, it's not a value
@@ -271,3 +282,10 @@ bool finite_set_decl_plugin::are_distinct(app* e1, app* e2) const {
     // that the other doesn't contain. Such as (union (singleton a) (singleton b)) and (singleton c) where c is different from a, b.
     return false;
 }
+
+func_decl *finite_set_util::mk_range_decl() {
+    arith_util a(m_manager);
+    sort *i = a.mk_int();
+    sort *domain[2] = {i, i};
+    return m_manager.mk_func_decl(m_fid, OP_FINITE_SET_RANGE, 0, nullptr, 2, domain, nullptr);
+}
diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h
index 5eec15d27..1c43d0dd0 100644
--- a/src/ast/finite_set_decl_plugin.h
+++ b/src/ast/finite_set_decl_plugin.h
@@ -195,6 +195,8 @@ public:
         return m_manager.mk_app(m_fid, OP_FINITE_SET_FILTER, arr, set);
     }
 
+    func_decl *mk_range_decl();
+
     app * mk_range(expr* low, expr* high) {
         return m_manager.mk_app(m_fid, OP_FINITE_SET_RANGE, low, high);
     }
diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp
index e8a309ed0..db7739f5e 100644
--- a/src/ast/rewriter/finite_set_axioms.cpp
+++ b/src/ast/rewriter/finite_set_axioms.cpp
@@ -19,6 +19,7 @@ Revision History:
 --*/
 
 #include "ast/ast.h"
+#include "ast/ast_pp.h"
 #include "ast/finite_set_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
@@ -38,8 +39,8 @@ void finite_set_axioms::in_empty_axiom(expr *x) {
     expr_ref empty_set(u.mk_empty(elem_sort), m);
     expr_ref x_in_empty(u.mk_in(x, empty_set), m);
     
-    theory_axiom ax(m, "in-empty");
-    ax.clause.push_back(m.mk_not(x_in_empty));
+    theory_axiom* ax = alloc(theory_axiom, m, "in-empty");
+    ax->clause.push_back(m.mk_not(x_in_empty));
     m_add_clause(ax);
 }
 
@@ -50,27 +51,28 @@ void finite_set_axioms::in_union_axiom(expr *x, expr *a) {
     if (!u.is_union(a, b, c))
         return;
 
-    theory_axiom ax(m, "in-union");
+
     expr_ref x_in_a(u.mk_in(x, a), m);
     expr_ref x_in_b(u.mk_in(x, b), m);
     expr_ref x_in_c(u.mk_in(x, c), m);
     
     // (x in a) => (x in b) or (x in c)
-    ax.clause.push_back(m.mk_not(x_in_a));
-    ax.clause.push_back(x_in_b);
-    ax.clause.push_back(x_in_c);
-    m_add_clause(ax);
+    theory_axiom *ax1 = alloc(theory_axiom, m, "in-union");
+    ax1->clause.push_back(m.mk_not(x_in_a));
+    ax1->clause.push_back(x_in_b);
+    ax1->clause.push_back(x_in_c);
+    m_add_clause(ax1);
 
     // (x in b) => (x in a)
-    theory_axiom ax2(m, "in-union");
-    ax2.clause.push_back(m.mk_not(x_in_b));
-    ax2.clause.push_back(x_in_a);
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-union");
+    ax2->clause.push_back(m.mk_not(x_in_b));
+    ax2->clause.push_back(x_in_a);
     m_add_clause(ax2);
 
     // (x in c) => (x in a)
-    theory_axiom ax3(m, "in-union");
-    ax3.clause.push_back(m.mk_not(x_in_c));
-    ax3.clause.push_back(x_in_a);
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-union");
+    ax3->clause.push_back(m.mk_not(x_in_c));
+    ax3->clause.push_back(x_in_a);
     m_add_clause(ax3);
 }
 
@@ -86,22 +88,22 @@ void finite_set_axioms::in_intersect_axiom(expr *x, expr *a) {
     expr_ref x_in_c(u.mk_in(x, c), m);
     
     // (x in a) => (x in b)
-    theory_axiom ax1(m, "in-intersect");
-    ax1.clause.push_back(m.mk_not(x_in_a));
-    ax1.clause.push_back(x_in_b);
+    theory_axiom* ax1 = alloc(theory_axiom, m, "in-intersect");
+    ax1->clause.push_back(m.mk_not(x_in_a));
+    ax1->clause.push_back(x_in_b);
     m_add_clause(ax1);
 
     // (x in a) => (x in c)
-    theory_axiom ax2(m, "in-intersect");
-    ax2.clause.push_back(m.mk_not(x_in_a));
-    ax2.clause.push_back(x_in_c);
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-intersect");
+    ax2->clause.push_back(m.mk_not(x_in_a));
+    ax2->clause.push_back(x_in_c);
     m_add_clause(ax2);
 
     // (x in b) and (x in c) => (x in a)
-    theory_axiom ax3(m, "in-intersect");
-    ax3.clause.push_back(m.mk_not(x_in_b));
-    ax3.clause.push_back(m.mk_not(x_in_c));
-    ax3.clause.push_back(x_in_a);
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-intersect");
+    ax3->clause.push_back(m.mk_not(x_in_b));
+    ax3->clause.push_back(m.mk_not(x_in_c));
+    ax3->clause.push_back(x_in_a);
     m_add_clause(ax3);
 }
 
@@ -117,22 +119,22 @@ void finite_set_axioms::in_difference_axiom(expr *x, expr *a) {
     expr_ref x_in_c(u.mk_in(x, c), m);
     
     // (x in a) => (x in b)
-    theory_axiom ax1(m, "in-difference");
-    ax1.clause.push_back(m.mk_not(x_in_a));
-    ax1.clause.push_back(x_in_b);
+    theory_axiom* ax1 = alloc(theory_axiom, m, "in-difference");
+    ax1->clause.push_back(m.mk_not(x_in_a));
+    ax1->clause.push_back(x_in_b);
     m_add_clause(ax1);
     
     // (x in a) => not (x in c)
-    theory_axiom ax2(m, "in-difference");
-    ax2.clause.push_back(m.mk_not(x_in_a));
-    ax2.clause.push_back(m.mk_not(x_in_c));
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-difference");
+    ax2->clause.push_back(m.mk_not(x_in_a));
+    ax2->clause.push_back(m.mk_not(x_in_c));
     m_add_clause(ax2);
 
     // (x in b) and not (x in c) => (x in a)
-    theory_axiom ax3(m, "in-difference");
-    ax3.clause.push_back(m.mk_not(x_in_b));
-    ax3.clause.push_back(x_in_c);
-    ax3.clause.push_back(x_in_a);
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-difference");
+    ax3->clause.push_back(m.mk_not(x_in_b));
+    ax3->clause.push_back(x_in_c);
+    ax3->clause.push_back(x_in_a);
     m_add_clause(ax3);
 }
 
@@ -145,11 +147,11 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) {
     
     expr_ref x_in_a(u.mk_in(x, a), m);
 
-    theory_axiom ax(m, "in-singleton");
+    theory_axiom* ax = alloc(theory_axiom, m, "in-singleton");
     if (x == b) {
         // If x and b are syntactically identical, then (x in a) is always true
 
-        ax.clause.push_back(x_in_a);
+        ax->clause.push_back(x_in_a);
         m_add_clause(ax);
         return;
     }
@@ -157,17 +159,42 @@ void finite_set_axioms::in_singleton_axiom(expr *x, expr *a) {
     expr_ref x_eq_b(m.mk_eq(x, b), m);
     
     // (x in a) => (x == b)
-    ax.clause.push_back(m.mk_not(x_in_a));
-    ax.clause.push_back(x_eq_b);
+    ax->clause.push_back(m.mk_not(x_in_a));
+    ax->clause.push_back(x_eq_b);
     m_add_clause(ax);
-    ax.clause.reset();
+    ax = alloc(theory_axiom, m, "in-singleton");
 
     // (x == b) => (x in a)
-    ax.clause.push_back(m.mk_not(x_eq_b));
-    ax.clause.push_back(x_in_a);
+    ax->clause.push_back(m.mk_not(x_eq_b));
+    ax->clause.push_back(x_in_a);
     m_add_clause(ax);
 }
 
+void finite_set_axioms::in_singleton_axiom(expr* a) {
+    expr *b = nullptr;
+    if (!u.is_singleton(a, b))
+        return;
+    
+    arith_util arith(m);
+
+    expr_ref b_in_a(u.mk_in(b, a), m);
+
+    auto ax = alloc(theory_axiom, m, "in-singleton");
+    ax->clause.push_back(b_in_a);
+    m_add_clause(ax);
+
+    ax = alloc(theory_axiom, m, "in-singleton");
+    expr_ref bm1_in_a(u.mk_in(arith.mk_add(b, arith.mk_int(-1)), a), m);
+    ax->clause.push_back(m.mk_not(bm1_in_a));
+    m_add_clause(ax);
+    
+    ax = alloc(theory_axiom, m, "in-singleton");
+    expr_ref bp1_in_a(u.mk_in(arith.mk_add(b, arith.mk_int(1)), a), m);
+    ax->clause.push_back(m.mk_not(bp1_in_a));
+}
+
+
+
 // a := set.range(lo, hi)
 // (x in a) <=> (lo <= x <= hi)
 void finite_set_axioms::in_range_axiom(expr *x, expr *a) {
@@ -177,29 +204,58 @@ void finite_set_axioms::in_range_axiom(expr *x, expr *a) {
     
     arith_util arith(m);
     expr_ref x_in_a(u.mk_in(x, a), m);
-    expr_ref lo_le_x(arith.mk_le(lo, x), m);
-    expr_ref x_le_hi(arith.mk_le(x, hi), m);
+    expr_ref lo_le_x(arith.mk_le(arith.mk_sub(lo, x), arith.mk_int(0)), m);
+    expr_ref x_le_hi(arith.mk_le(arith.mk_sub(x, hi), arith.mk_int(0)), m);
+    m_rewriter(lo_le_x);
+    m_rewriter(x_le_hi);
     
     // (x in a) => (lo <= x)
-    theory_axiom ax1(m, "in-range");
-    ax1.clause.push_back(m.mk_not(x_in_a));
-    ax1.clause.push_back(lo_le_x);
+    theory_axiom* ax1 = alloc(theory_axiom, m, "in-range");
+    ax1->clause.push_back(m.mk_not(x_in_a));
+    ax1->clause.push_back(lo_le_x);
     m_add_clause(ax1);
 
     // (x in a) => (x <= hi)
-    theory_axiom ax2(m, "in-range");
-    ax2.clause.push_back(m.mk_not(x_in_a));
-    ax2.clause.push_back(x_le_hi);
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-range");
+    ax2->clause.push_back(m.mk_not(x_in_a));
+    ax2->clause.push_back(x_le_hi);
     m_add_clause(ax2);
 
     // (lo <= x) and (x <= hi) => (x in a)
-    theory_axiom ax3(m, "in-range");
-    ax3.clause.push_back(m.mk_not(lo_le_x));
-    ax3.clause.push_back(m.mk_not(x_le_hi));
-    ax3.clause.push_back(x_in_a);
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-range");
+    ax3->clause.push_back(m.mk_not(lo_le_x));
+    ax3->clause.push_back(m.mk_not(x_le_hi));
+    ax3->clause.push_back(x_in_a);
     m_add_clause(ax3);
 }
 
+// a := set.range(lo, hi)
+// (not (set.in (- lo 1) r))
+// (not (set.in (+ hi 1) r))
+// (set.in lo r)
+// (set.in hi r)
+void finite_set_axioms::in_range_axiom(expr* r) {
+    expr *lo = nullptr, *hi = nullptr;
+    if (!u.is_range(r, lo, hi))
+        return;
+    theory_axiom* ax = alloc(theory_axiom, m, "range-bounds");
+    ax->clause.push_back(u.mk_in(lo, r));
+    m_add_clause(ax);
+
+    ax = alloc(theory_axiom, m, "range-bounds");
+    ax->clause.push_back(u.mk_in(hi, r));
+    m_add_clause(ax);
+
+    arith_util a(m);
+    ax = alloc(theory_axiom, m, "range-bounds");
+    ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(hi, a.mk_int(1)), r)));
+    m_add_clause(ax);
+
+    ax = alloc(theory_axiom, m, "range-bounds");
+    ax->clause.push_back(m.mk_not(u.mk_in(a.mk_add(lo, a.mk_int(-1)), r)));
+    m_add_clause(ax);
+}
+
 // a := set.map(f, b)
 // (x in a) <=> set.map_inverse(f, x, b) in b
 void finite_set_axioms::in_map_axiom(expr *x, expr *a) {
@@ -228,9 +284,9 @@ void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) {
     expr_ref fx_in_a(u.mk_in(fx, a), m);
     
     // (x in b) => f(x) in a
-    theory_axiom ax(m, "in-map-image");
-    ax.clause.push_back(m.mk_not(x_in_b));
-    ax.clause.push_back(fx_in_a);
+    theory_axiom* ax = alloc(theory_axiom, m, "in-map-image");
+    ax->clause.push_back(m.mk_not(x_in_b));
+    ax->clause.push_back(fx_in_a);
     m_add_clause(ax);
 }
 
@@ -249,22 +305,22 @@ void finite_set_axioms::in_filter_axiom(expr *x, expr *a) {
     expr_ref px(autil.mk_select(p, x), m);
     
     // (x in a) => (x in b)
-    theory_axiom ax1(m, "in-filter");
-    ax1.clause.push_back(m.mk_not(x_in_a));
-    ax1.clause.push_back(x_in_b);
+    theory_axiom* ax1 = alloc(theory_axiom, m, "in-filter");
+    ax1->clause.push_back(m.mk_not(x_in_a));
+    ax1->clause.push_back(x_in_b);
     m_add_clause(ax1);
 
     // (x in a) => p(x)
-    theory_axiom ax2(m, "in-filter");
-    ax2.clause.push_back(m.mk_not(x_in_a));
-    ax2.clause.push_back(px);
+    theory_axiom* ax2 = alloc(theory_axiom, m, "in-filter");
+    ax2->clause.push_back(m.mk_not(x_in_a));
+    ax2->clause.push_back(px);
     m_add_clause(ax2);
 
     // (x in b) and p(x) => (x in a)
-    theory_axiom ax3(m, "in-filter");
-    ax3.clause.push_back(m.mk_not(x_in_b));
-    ax3.clause.push_back(m.mk_not(px));
-    ax3.clause.push_back(x_in_a);
+    theory_axiom* ax3 = alloc(theory_axiom, m, "in-filter");
+    ax3->clause.push_back(m.mk_not(x_in_b));
+    ax3->clause.push_back(m.mk_not(px));
+    ax3->clause.push_back(x_in_a);
     m_add_clause(ax3);
 }
 
@@ -280,8 +336,8 @@ void finite_set_axioms::size_singleton_axiom(expr *a) {
     expr_ref one(arith.mk_int(1), m);
     expr_ref eq(m.mk_eq(size_a, one), m);
 
-    theory_axiom ax(m, "size-singleton");
-    ax.clause.push_back(eq);
+    theory_axiom* ax = alloc(theory_axiom, m, "size-singleton");
+    ax->clause.push_back(eq);
     m_add_clause(ax);
 }
 
@@ -293,14 +349,14 @@ void finite_set_axioms::subset_axiom(expr* a) {
     expr_ref intersect_bc(u.mk_intersect(b, c), m);
     expr_ref eq(m.mk_eq(intersect_bc, b), m);
 
-    theory_axiom ax1(m,  "subset");
-    ax1.clause.push_back(m.mk_not(a));
-    ax1.clause.push_back(eq);
+    theory_axiom* ax1 = alloc(theory_axiom, m,  "subset");
+    ax1->clause.push_back(m.mk_not(a));
+    ax1->clause.push_back(eq);
     m_add_clause(ax1);
 
-    theory_axiom ax2(m,  "subset");
-    ax2.clause.push_back(a);
-    ax2.clause.push_back(m.mk_not(eq));
+    theory_axiom* ax2 = alloc(theory_axiom, m,  "subset");
+    ax2->clause.push_back(a);
+    ax2->clause.push_back(m.mk_not(eq));
     m_add_clause(ax2);
 }
 
@@ -313,15 +369,15 @@ void finite_set_axioms::extensionality_axiom(expr *a, expr* b) {
     expr_ref diff_in_b(u.mk_in(diff_ab, b), m);
     
     // (a != b) => (x in diff_ab != x in diff_ba)
-    theory_axiom ax(m, "extensionality");
-    ax.clause.push_back(a_eq_b);
-    ax.clause.push_back(m.mk_not(diff_in_a));
-    ax.clause.push_back(m.mk_not(diff_in_b));
+    theory_axiom* ax = alloc(theory_axiom, m, "extensionality");
+    ax->clause.push_back(a_eq_b);
+    ax->clause.push_back(m.mk_not(diff_in_a));
+    ax->clause.push_back(m.mk_not(diff_in_b));
     m_add_clause(ax);
 
-    theory_axiom ax2(m, "extensionality");
-    ax2.clause.push_back(m.mk_not(a_eq_b));
-    ax2.clause.push_back(diff_in_a);
-    ax2.clause.push_back(diff_in_b);
+    theory_axiom* ax2 = alloc(theory_axiom, m, "extensionality");
+    ax2->clause.push_back(m.mk_not(a_eq_b));
+    ax2->clause.push_back(diff_in_a);
+    ax2->clause.push_back(diff_in_b);
     m_add_clause(ax2);
 }
\ No newline at end of file
diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h
index 85b192cdd..46684373c 100644
--- a/src/ast/rewriter/finite_set_axioms.h
+++ b/src/ast/rewriter/finite_set_axioms.h
@@ -12,6 +12,8 @@ Abstract:
        
 --*/
 
+#include "ast/rewriter/th_rewriter.h"
+
 struct theory_axiom {
     expr_ref_vector   clause;
     vector<parameter> params;
@@ -32,14 +34,15 @@ std::ostream &operator<<(std::ostream &out, theory_axiom const &ax);
 class finite_set_axioms {
     ast_manager&    m;
     finite_set_util u;
+    th_rewriter m_rewriter;
 
-    std::function<void(theory_axiom const &)> m_add_clause;
+    std::function<void(theory_axiom *)> m_add_clause;
 
 public:
 
-    finite_set_axioms(ast_manager &m) : m(m), u(m) {}
+    finite_set_axioms(ast_manager &m) : m(m), u(m), m_rewriter(m) {}
 
-    void set_add_clause(std::function<void(theory_axiom const &)> &ac) {
+    void set_add_clause(std::function<void(theory_axiom*)> &ac) {
         m_add_clause = ac;
     }
 
@@ -62,10 +65,23 @@ public:
     // (x in a) <=> (x == b)
     void in_singleton_axiom(expr *x, expr *a);
 
+    // a := set.singleton(b)
+    // b in a
+    // b-1 not in a
+    // b+1 not in a
+    void in_singleton_axiom(expr *a);
+
     // a := set.range(lo, hi)
     // (x in a) <=> (lo <= x <= hi)
     void in_range_axiom(expr *x, expr *a);
 
+    // a := set.range(lo, hi)
+    // (not (set.in (- lo 1) a))
+    // (not (set.in (+ hi 1) a))
+    // (set.in lo a)
+    // (set.in hi a)
+    void in_range_axiom(expr *a);
+
     // a := set.map(f, b)
     // (x in a) <=> set.map_inverse(f, x, b) in b
     void in_map_axiom(expr *x, expr *a);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index bc7df2ca9..c7ce4801a 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1525,16 +1525,24 @@ namespace smt {
     }
 
     lbool context::find_assignment(expr * n) const {
-        if (m.is_false(n))
-            return l_false;
+
         expr* arg = nullptr;
         if (m.is_not(n, arg)) {
+
             if (b_internalized(arg))
                 return ~get_assignment_core(arg);
+            if (m.is_false(arg))
+                return l_true;
+            if (m.is_true(arg))
+                return l_false;
             return l_undef;
         }
         if (b_internalized(n))
             return get_assignment(n);
+        if (m.is_false(n))
+            return l_false;
+        if (m.is_true(n))
+            return l_true;
         return l_undef;
     }
 
diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index 7badc1c99..9ba9882bb 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/src/smt/theory_finite_set.cpp
@@ -15,6 +15,7 @@ Abstract:
 #include "smt/theory_finite_set.h"
 #include "smt/smt_context.h"
 #include "smt/smt_model_generator.h"
+#include "smt/smt_arith_value.h"
 #include "ast/ast_pp.h"
 
 namespace smt {
@@ -29,8 +30,8 @@ namespace smt {
         m_axioms(m), m_find(*this)
     {
         // Setup the add_clause callback for axioms
-        std::function<void(theory_axiom const &)> add_clause_fn =
-            [this](theory_axiom const &ax) {
+        std::function<void(theory_axiom *)> add_clause_fn =
+            [this](theory_axiom* ax) {
                 this->add_clause(ax);
             };
         m_axioms.set_add_clause(add_clause_fn);
@@ -67,7 +68,7 @@ namespace smt {
         theory_var r = theory::mk_var(n);
         VERIFY(r == static_cast<theory_var>(m_find.mk_var()));
         SASSERT(r == static_cast<int>(m_var_data.size()));
-        m_var_data.push_back(alloc(var_data));
+        m_var_data.push_back(alloc(var_data, m));
         ctx.push_trail(push_back_vector<ptr_vector<var_data>>(m_var_data));
         ctx.push_trail(new_obj_trail(m_var_data.back()));
         expr *e = n->get_expr();
@@ -90,7 +91,8 @@ namespace smt {
             m_var_data[r]->m_setops.push_back(n);
             ctx.push_trail(push_back_trail(m_var_data[r]->m_setops));
             for (auto arg : enode::args(n)) {
-                if (!u.is_finite_set(arg->get_expr()))
+                expr *e = arg->get_expr();
+                if (!u.is_finite_set(e))
                     continue;
                 auto v = arg->get_root()->get_th_var(get_id());
                 SASSERT(v != null_theory_var);
@@ -103,6 +105,9 @@ namespace smt {
         }
         else if (u.is_map(e) || u.is_filter(e)) {
             NOT_IMPLEMENTED_YET();
+        }
+        else if (u.is_range(e)) {
+            
         }
         return r;
     }
@@ -157,6 +162,7 @@ namespace smt {
      *  for each T := (set.op U V) in d2->setops
      *         then S ~ T by construction
      *              add axioms for (set.in x T)
+     * 
     */
 
     void theory_finite_set::add_in_axioms(enode *in, var_data *d) {
@@ -276,6 +282,9 @@ namespace smt {
         if (activate_unasserted_clause())
             return FC_CONTINUE;
 
+        if (false && activate_range_local_axioms())
+            return FC_CONTINUE;
+
         if (assume_eqs())
             return FC_CONTINUE;
         
@@ -293,20 +302,38 @@ namespace smt {
      * - (set.singleton x) -> (set.in x (set.singleton x))
      * - (set.singleton x) -> (set.size (set.singleton x)) = 1
      * - (set.empty)       -> (set.size (set.empty)) = 0
+     * - (set.range lo hi) -> lo-1,hi+1 not in range, lo, hi in range
      */
     void theory_finite_set::add_immediate_axioms(app* term) {
         expr *elem = nullptr, *set = nullptr;
+        expr *lo = nullptr, *hi = nullptr;
         unsigned sz = m_clauses.axioms.size();
         if (u.is_in(term, elem, set) && u.is_empty(set))
             add_membership_axioms(elem, set);
         else if (u.is_subset(term))
             m_axioms.subset_axiom(term);
-        else if (u.is_singleton(term, elem))
-            m_axioms.in_singleton_axiom(elem, term);
+        else if (u.is_singleton(term))
+            m_axioms.in_singleton_axiom(term);
+        else if (u.is_range(term, lo, hi)) {
+            m_axioms.in_range_axiom(term);
+            auto range = ctx.get_enode(term);
+            auto v = range->get_th_var(get_id());
+            // declare lo-1, lo, hi, hi+1 as range local.
+            // we don't have to add additional range local variables for them.
+            auto &range_local = m_var_data[v]->m_range_local;
+            ctx.push_trail(push_back_vector(range_local));
+            arith_util a(m);
+            range_local.push_back(lo);
+            range_local.push_back(hi);
+            range_local.push_back(a.mk_add(lo, a.mk_int(-1)));
+            range_local.push_back(a.mk_add(hi, a.mk_int(1)));
+        }
        
         // Assert all new lemmas as clauses
-        for (unsigned i = sz; i < m_clauses.axioms.size(); ++i)
+        for (unsigned i = sz; i < m_clauses.axioms.size(); ++i) {
             m_clauses.squeue.push_back(i);
+            ctx.push_trail(push_back_vector(m_clauses.squeue));
+        }
     }
 
     void theory_finite_set::assign_eh(bool_var v, bool is_true) {
@@ -322,8 +349,8 @@ namespace smt {
         for (unsigned i = 0; i < m_clauses.watch[idx].size(); ++i) {
             TRACE(finite_set, tout << " watch[" << i << "] size: " << m_clauses.watch[i].size() << "\n";);
             auto clause_idx = m_clauses.watch[idx][i];
-            auto &ax = m_clauses.axioms[clause_idx];
-            auto &clause = ax.clause;
+            auto* ax = m_clauses.axioms[clause_idx];
+            auto &clause = ax->clause;
             if (any_of(clause, [&](expr *lit) { return ctx.find_assignment(lit) == l_true; })) {
                 TRACE(finite_set, tout << "  satisfied\n";);
                 m_clauses.watch[idx][j++] = clause_idx;
@@ -365,6 +392,7 @@ namespace smt {
                 continue;  // the clause is removed from this watch list
             // either all literals are false, or the other watch literal is propagating.
             m_clauses.squeue.push_back(clause_idx);
+            ctx.push_trail(push_back_vector(m_clauses.squeue));
             TRACE(finite_set, tout << "  propagate clause\n";);
             m_clauses.watch[idx][j++] = clause_idx;
             ++i;
@@ -390,21 +418,22 @@ namespace smt {
 
             // empty the propagation queue of clauses to assert
             while (m_clauses.sqhead < m_clauses.squeue.size() && !ctx.inconsistent()) {
-                auto index = m_clauses.squeue[m_clauses.sqhead++];
-                auto const &clause = m_clauses.axioms[index];
-                assert_clause(clause);
+                auto clause_idx = m_clauses.squeue[m_clauses.sqhead++];
+                auto ax = m_clauses.axioms[clause_idx];
+                assert_clause(ax);
             }
         }      
     }
 
     void theory_finite_set::activate_clause(unsigned clause_idx) {
         TRACE(finite_set, tout << "activate_clause: " << clause_idx << "\n";);
-        auto &ax = m_clauses.axioms[clause_idx];
-        auto &clause = ax.clause;
+        auto* ax = m_clauses.axioms[clause_idx];
+        auto &clause = ax->clause;
         if (any_of(clause, [&](expr *e) { return ctx.find_assignment(e) == l_true; }))
             return;
         if (clause.size() <= 1) {
             m_clauses.squeue.push_back(clause_idx);
+            ctx.push_trail(push_back_vector(m_clauses.squeue));
             return;
         }
         expr *w1 = nullptr, *w2 = nullptr;
@@ -430,6 +459,7 @@ namespace smt {
         }
         if (!w2) {
             m_clauses.squeue.push_back(clause_idx);
+            ctx.push_trail(push_back_vector(m_clauses.squeue));
             return;
         }
         bool w1neg = m.is_not(w1, w1);
@@ -446,8 +476,8 @@ namespace smt {
             unsigned index;
             unwatch_clause(theory_finite_set &th, unsigned index) : th(th), index(index) {}
             void undo() override {
-                auto &ax = th.m_clauses.axioms[index];
-                auto &clause = ax.clause;
+                auto* ax = th.m_clauses.axioms[index];
+                auto &clause = ax->clause;
                 expr *w1 = clause.get(0);
                 expr *w2 = clause.get(1);
                 bool w1neg = th.m.is_not(w1, w1);
@@ -487,8 +517,9 @@ namespace smt {
             // Create a union expression that is canonical (sorted)
             auto& set = *m_set_members[r];
             ptr_vector<expr> elems;
-            for (auto e : set)
-                elems.push_back(e->get_expr());
+            for (auto [e,b] : set)
+                if (b)  
+                    elems.push_back(e->get_expr());
             std::sort(elems.begin(), elems.end(), [](expr *a, expr *b) { return a->get_id() < b->get_id(); });
             expr *s = mk_union(elems.size(), elems.data(), n->get_expr()->get_sort());
             trail.push_back(s);
@@ -569,9 +600,10 @@ namespace smt {
         }        
     }
 
-    void theory_finite_set::add_clause(theory_axiom const& ax) {
+    void theory_finite_set::add_clause(theory_axiom* ax) {
         TRACE(finite_set, tout << "add_clause: " << ax << "\n");
         ctx.push_trail(push_back_vector(m_clauses.axioms));
+        ctx.push_trail(new_obj_trail(ax));
         m_clauses.axioms.push_back(ax);
         m_stats.m_num_axioms_created++;
     }
@@ -601,19 +633,19 @@ namespace smt {
         mg.register_factory(m_factory);
         collect_members();
     }
-
+   
     void theory_finite_set::collect_members() {
         // This method can be used to collect all elements that are members of sets
         // and ensure that the model factory has values for them.
         // For now, we rely on the default model construction.
         reset_set_members();
+
         for (auto f : m_set_in_decls) {
             for (auto n : ctx.enodes_of(f)) {
-                SASSERT(u.is_in(n->get_expr()));
-                auto x = n->get_arg(0);
-                if (!ctx.is_relevant(x))
+                if (!ctx.is_relevant(n))
                     continue;
-                x = x->get_root();
+                SASSERT(u.is_in(n->get_expr()));
+                auto x = n->get_arg(0)->get_root();
                 if (x->is_marked())
                     continue;
                 x->set_mark();  // make sure we only do this once per element
@@ -622,61 +654,139 @@ namespace smt {
                         continue;
                     if (!u.is_in(p->get_expr()))
                         continue;
-                    if (ctx.get_assignment(p->get_expr()) != l_true)
-                        continue;
+                    bool b = ctx.find_assignment(p->get_expr()) == l_true;
                     auto set = p->get_arg(1)->get_root();
                     auto elem = p->get_arg(0)->get_root();
                     if (elem != x)
                         continue;
-                    if (!m_set_members.contains(set))
-                        m_set_members.insert(set, alloc(obj_hashtable<enode>));
-                    m_set_members.find(set)->insert(x);
+                    if (!m_set_members.contains(set)) {
+                        using om = obj_map<enode, bool>;
+                        auto m = alloc(om);
+                        m_set_members.insert(set, m);
+                    }
+                    m_set_members.find(set)->insert(x, b);
                 }
             }
         }
         for (auto f : m_set_in_decls) {
             for (auto n : ctx.enodes_of(f)) {
                 SASSERT(u.is_in(n->get_expr()));
-                auto x = n->get_arg(0);
-                x = x->get_root();
+                auto x = n->get_arg(0)->get_root();     
                 if (x->is_marked())
                     x->unset_mark();
             }
         }
     }
 
+    // to collect range interpretations for S:
+    // walk parents of S that are (set.in x S)
+    // evaluate truth value of (set.in x S), evaluate x
+    // add (eval(x), eval(set.in x S)) into a vector.
+    // sort the vector by eval(x)
+    // [(v1, b1), (v2, b2), ..., (vn, bn)]
+    // for the first i, with b_i true, add the range [vi, v_{i+1}-1].
+    // the last bn should be false by construction.
+
+    void theory_finite_set::add_range_interpretation(enode* s) {
+        vector<std::tuple<rational, enode *, bool>> elements;
+        arith_value av(m);
+        av.init(&ctx);
+        for (auto p : enode::parents(s)) {
+            if (!ctx.is_relevant(p))
+                continue;
+            if (u.is_in(p->get_expr())) {
+                rational val;
+                auto x = p->get_arg(0)->get_root();
+                VERIFY(av.get_value_equiv(x->get_expr(), val) && val.is_int());
+                elements.push_back({val, x, ctx.find_assignment(p->get_expr()) == l_true});
+            }
+        }
+        std::stable_sort(elements.begin(), elements.end(),
+                         [](auto const &a, auto const &b) { return std::get<0>(a) < std::get<0>(b); });
+
+
+    }
+
     struct finite_set_value_proc : model_value_proc {    
         theory_finite_set &th;        
-        sort *s = nullptr;
-        obj_hashtable<enode>* m_elements = nullptr;
+        enode *n = nullptr;
+        obj_map<enode, bool>* m_elements = nullptr;
 
-        finite_set_value_proc(theory_finite_set &th, sort *s, obj_hashtable<enode> *elements)
-            : th(th), s(s), m_elements(elements) {}
+        // use range interpretations if there is a range constraint and the base sort is integer
+        bool use_range() {
+            auto &m = th.m;
+            sort *base_s = nullptr;
+            VERIFY(th.u.is_finite_set(n->get_expr()->get_sort(), base_s));
+            arith_util a(m);
+            if (!a.is_int(base_s))
+                return false;
+            func_decl_ref range_fn(th.u.mk_range_decl(), m);
+            return th.ctx.get_num_enodes_of(range_fn.get()) > 0;
+        }
+
+        finite_set_value_proc(theory_finite_set &th, enode *n, obj_map<enode, bool> *elements)
+            : th(th), n(n), m_elements(elements) {}
 
         void get_dependencies(buffer<model_value_dependency> &result) override {
             if (!m_elements)
                 return;
-            for (auto v : *m_elements)
-                result.push_back(model_value_dependency(v));
+            bool ur = use_range();
+            for (auto [n, b] : *m_elements)
+                if (!ur || b)
+                    result.push_back(model_value_dependency(n));
         }
 
         app *mk_value(model_generator &mg, expr_ref_vector const &values) override {            
             SASSERT(values.empty() == !m_elements);
-            if (values.empty()) 
+            auto s = n->get_sort();
+            if (values.empty())
                 return th.u.mk_empty(s);
 
-            SASSERT(m_elements);
-            SASSERT(values.size() == m_elements->size());
-            return th.mk_union(values.size(), values.data(), s);
+            SASSERT(m_elements);            
+            if (use_range())
+                return mk_range_value(mg, values);
+            else 
+                return th.mk_union(values.size(), values.data(), s);
+        }
+
+        app *mk_range_value(model_generator &mg, expr_ref_vector const &values) {
+            unsigned i = 0;
+            arith_value av(th.m);
+            av.init(&th.ctx);
+            vector<std::tuple<rational, enode *, bool>> elems;
+            for (auto [n, b] : *m_elements) {
+                rational r;
+                av.get_value(n->get_expr(), r);               
+                elems.push_back({r, n, b});
+            }
+            std::stable_sort(elems.begin(), elems.end(),
+                             [](auto const &a, auto const &b) { return std::get<0>(a) < std::get<0>(b); });
+            app *range = nullptr;
+            arith_util a(th.m);
+
+            for (unsigned j = 0; j < elems.size(); ++j) {
+                auto [r, n, b] = elems[j];
+                if (!b)
+                    continue;
+                rational lo = r;
+                rational hi = j + 1 < elems.size() ? std::get<0>(elems[j + 1]) - rational(1) : r;
+                while (j + 1 < elems.size() && std::get<0>(elems[j + 1]) == hi + rational(1) && std::get<2>(elems[j + 1])) {
+                    hi = std::get<0>(elems[j + 1]);
+                    ++j;
+                }
+                auto new_range = th.u.mk_range(a.mk_int(lo), a.mk_int(hi));
+                range = range ? th.u.mk_union(range, new_range) : new_range;
+            }
+            return range ? range : th.u.mk_empty(n->get_sort());        
         }
     };
 
     model_value_proc * theory_finite_set::mk_value(enode * n, model_generator & mg) {
-        TRACE(finite_set, tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";);       
-        obj_hashtable<enode>*elements = nullptr;
-        sort *s = n->get_expr()->get_sort();
-        m_set_members.find(n->get_root(), elements); 
-        return alloc(finite_set_value_proc, *this, s, elements);
+        TRACE(finite_set, tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";);
+        obj_map<enode, bool>*elements = nullptr;
+        n = n->get_root();
+        m_set_members.find(n, elements); 
+        return alloc(finite_set_value_proc, *this, n, elements);
     }
 
 
@@ -692,10 +802,62 @@ namespace smt {
         return false;
     }
 
-    bool theory_finite_set::assert_clause(theory_axiom const &ax) {
-        auto const &clause = ax.clause;
+    /*
+     * Add x-1, x+1 in range axioms for every x in setop(range, S)
+     * then x-1, x+1 will also propagate against setop(range, S).
+     */
+    bool theory_finite_set::activate_range_local_axioms() {
+        bool new_axiom = false;
+        func_decl_ref range_fn(u.mk_range_decl(), m);
+        for (auto range : ctx.enodes_of(range_fn.get())) {
+            SASSERT(u.is_range(range->get_expr()));
+            auto v = range->get_th_var(get_id());
+            for (auto p : m_var_data[v]->m_parent_setops) {
+                auto w = p->get_th_var(get_id());
+                for (auto in : m_var_data[w]->m_parent_in) {
+                    if (activate_range_local_axioms(in->get_arg(0)->get_expr(), range))
+                        new_axiom = true;
+                }
+            }
+        }
+        return new_axiom;
+    }
+
+
+    bool theory_finite_set::activate_range_local_axioms(expr* elem, enode* range) {
+        auto v = range->get_th_var(get_id());
+        auto &range_local = m_var_data[v]->m_range_local;
+        auto &parent_in = m_var_data[v]->m_parent_in;
+        if (range_local.contains(elem))
+            return false;
+        arith_util a(m);
+        expr_ref lo(a.mk_add(elem, a.mk_int(-1)), m);
+        expr_ref hi(a.mk_add(elem, a.mk_int(1)), m);
+        bool new_axiom = false;
+        if (!range_local.contains(lo) && all_of(parent_in, [lo](enode* in) { return in->get_arg(0)->get_expr() != lo; })) {
+            // lo is not range local and lo is not already in an expression (lo in range)
+            // checking that lo is not in range_local is actually redundant because we will instantiate 
+            // membership expressions for every range local expression.
+            // but we keep this set and check for now in case we want to change the saturation strategy.
+            ctx.push_trail(push_back_vector(range_local));
+            range_local.push_back(lo);
+            m_axioms.in_range_axiom(lo, range->get_expr());
+            new_axiom = true;
+        }
+        if (!range_local.contains(hi) &&
+            all_of(parent_in, [&hi](enode *in) { return in->get_arg(0)->get_expr() != hi; })) {
+            ctx.push_trail(push_back_vector(range_local));
+            range_local.push_back(hi);
+            m_axioms.in_range_axiom(hi, range->get_expr());
+            new_axiom = true;
+        }
+        return new_axiom;
+    }
+
+    bool theory_finite_set::assert_clause(theory_axiom const *ax) {
         expr *unit = nullptr;
         unsigned undef_count = 0;
+        auto &clause = ax->clause;
         for (auto e : clause) {
             switch (ctx.find_assignment(e)) {
             case l_true:
@@ -719,8 +881,8 @@ namespace smt {
             }
             m_stats.m_num_axioms_propagated++;
             enode_pair_vector eqs;
-            auto just = ext_theory_propagation_justification(get_id(), ctx, antecedent.size(), antecedent.data(), eqs.size(), eqs.data(), lit, ax.params.size(),
-                                                       ax.params.data());
+            auto just = ext_theory_propagation_justification(get_id(), ctx, antecedent.size(), antecedent.data(), eqs.size(), eqs.data(), 
+                lit, ax->params.size(), ax->params.data());
             auto bjust = ctx.mk_justification(just);
             if (ctx.clause_proof_active()) {
                 // assume all justifications is a non-empty list of symbol parameters
@@ -729,8 +891,8 @@ namespace smt {
                 // this misses conflicts at base level.
                 proof_ref pr(m);
                 expr_ref_vector args(m);
-                for (auto const& p : ax.params)
-                    args.push_back(m.mk_const(p.get_symbol(), m.mk_proof_sort()));                  
+                for (auto const& p : ax->params)
+                    args.push_back(m.mk_const(p.get_symbol(), m.mk_proof_sort()));
                 pr = m.mk_app(m.get_family_name(get_family_id()), args.size(), args.data(), m.mk_proof_sort());
                 justification_proof_wrapper jp(ctx, pr.get(), false);
                 ctx.get_clause_proof().propagate(lit, &jp, antecedent);
@@ -748,7 +910,7 @@ namespace smt {
         literal_vector lclause;
         for (auto e : clause)
             lclause.push_back(mk_literal(e));
-        ctx.mk_th_axiom(get_id(), lclause, ax.params.size(), ax.params.data());
+        ctx.mk_th_axiom(get_id(), lclause, ax->params.size(), ax->params.data());
         return true;
     }
 
diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h
index 28ded4c51..359fc24f2 100644
--- a/src/smt/theory_finite_set.h
+++ b/src/smt/theory_finite_set.h
@@ -101,13 +101,15 @@ namespace smt {
         friend struct finite_set_value_proc;
 
         struct var_data {
-            ptr_vector<enode> m_setops;
-            ptr_vector<enode> m_parent_in;
-            ptr_vector<enode> m_parent_setops;
+            ptr_vector<enode> m_setops;                // set operations equivalent to this
+            ptr_vector<enode> m_parent_in;             // x in A expressions
+            ptr_vector<enode> m_parent_setops;         // set of set expressions where this appears as sub-expression
+            expr_ref_vector   m_range_local;           // set of range local variables associated with range
+            var_data(ast_manager &m) : m_range_local(m) {}
         };
 
         struct theory_clauses {
-            vector<theory_axiom>    axioms;            // vector of created theory axioms
+            ptr_vector<theory_axiom>    axioms;            // vector of created theory axioms
             unsigned                aqhead = 0;        // queue head of created axioms
             unsigned_vector         squeue;            // propagation queue of axioms to be added to the solver
             unsigned                sqhead = 0;        // head into propagation queue axioms to be added to solver
@@ -133,12 +135,16 @@ namespace smt {
             }
         };
 
+        struct range {
+            rational lo, hi;
+        };
+
         finite_set_util           u;
         finite_set_axioms         m_axioms;
         th_union_find             m_find;
         theory_clauses            m_clauses;
         finite_set_factory *m_factory = nullptr;
-        obj_map<enode, obj_hashtable<enode> *> m_set_members;
+        obj_map<enode, obj_map<enode, bool> *> m_set_members;
         ptr_vector<func_decl> m_set_in_decls;
         ptr_vector<var_data> m_var_data;
         stats m_stats;
@@ -172,11 +178,13 @@ namespace smt {
 
         // Helper methods for axiom instantiation
         void add_membership_axioms(expr* elem, expr* set);
-        void add_clause(theory_axiom const& ax);
-        bool assert_clause(theory_axiom const &ax);
+        void add_clause(theory_axiom * ax);
+        bool assert_clause(theory_axiom const *ax);
         void activate_clause(unsigned index);
         bool activate_unasserted_clause();
         void add_immediate_axioms(app *atom);
+        bool activate_range_local_axioms();
+        bool activate_range_local_axioms(expr *elem, enode *range);
         bool assume_eqs();
         bool is_new_axiom(expr *a, expr *b);
         app *mk_union(unsigned num_elems, expr *const *elems, sort* set_sort);
@@ -184,6 +192,7 @@ namespace smt {
         // model construction
         void collect_members();
         void reset_set_members();
+        void add_range_interpretation(enode *s);
 
         // manage union-find of theory variables
         theory_var find(theory_var v) const { return m_find.find(v); }        
diff --git a/src/test/finite_set.cpp b/src/test/finite_set.cpp
index e2e28e8a4..34c3f06e0 100644
--- a/src/test/finite_set.cpp
+++ b/src/test/finite_set.cpp
@@ -130,14 +130,12 @@ static void tst_finite_set_map_filter() {
 static void tst_finite_set_is_value() {
     ast_manager m;
     reg_decl_plugins(m);
-    
-
-    
+        
     finite_set_util fsets(m);
     arith_util arith(m);
     finite_set_decl_plugin* plugin = static_cast<finite_set_decl_plugin*>(m.get_plugin(fsets.get_family_id()));
   
-      // Create Int sort and finite set sort
+    // Create Int sort and finite set sort
     
     // Test with Int sort (should be fully interpreted)
     sort_ref int_sort(arith.mk_int(), m);
@@ -145,7 +143,7 @@ static void tst_finite_set_is_value() {
     sort_ref finite_set_int(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, &int_param), m);
     
     
-  // Test 1: Empty set is a value
+    // Test 1: Empty set is a value
     app_ref empty_set(fsets.mk_empty(finite_set_int), m);
     ENSURE(plugin->is_value(empty_set.get()));
     
@@ -179,19 +177,19 @@ static void tst_finite_set_is_value() {
     app_ref union_triple(fsets.mk_union(union_temp, singleton_nine), m);
     ENSURE(plugin->is_value(union_triple.get()));
     
-    // Test 8: Range is NOT a value (it's not a union of empty/singletons)
+    // Test 8: Range is a value
     expr_ref zero(arith.mk_int(0), m);
     expr_ref ten(arith.mk_int(10), m);
     app_ref range_set(fsets.mk_range(zero, ten), m);
-    ENSURE(!plugin->is_value(range_set.get()));
+    ENSURE(plugin->is_value(range_set.get()));
     
-    // Test 9: Union with range is NOT a value
+    // Test 9: Union with range is  a value
     app_ref union_with_range(fsets.mk_union(singleton_five, range_set), m);
-    ENSURE(!plugin->is_value(union_with_range.get()));
+    ENSURE(plugin->is_value(union_with_range.get()));
     
-    // Test 10: Intersect is NOT a value
+    // Test 10: Intersect is a value
     app_ref intersect_set(fsets.mk_intersect(singleton_five, singleton_seven), m);
-    ENSURE(!plugin->is_value(intersect_set.get()));
+    ENSURE(plugin->is_value(intersect_set.get()));
     ENSURE(m.is_fully_interp(int_sort));
     ENSURE(m.is_fully_interp(finite_set_int));
 }