diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp
index dad7dd162..025040be0 100644
--- a/src/ast/rewriter/finite_set_axioms.cpp
+++ b/src/ast/rewriter/finite_set_axioms.cpp
@@ -33,23 +33,55 @@ std::ostream& operator<<(std::ostream& out, theory_axiom const& ax) {
 }
 
 void finite_set_axioms::add_unit(char const *name, expr *p1, expr *unit) {
+    expr_ref _f1(unit, m);
+    if (is_true(unit))
+        return;
     theory_axiom *ax = alloc(theory_axiom, m, name, p1);
     ax->clause.push_back(unit);
     m_add_clause(ax);
 }
 
+
+bool finite_set_axioms::is_true(expr *f) {
+    if (m.is_true(f))
+        return true;
+    if (m.is_not(f, f) && m.is_false(f))
+        return true;
+    return false;
+}
+
+
+bool finite_set_axioms::is_false(expr* f) {
+    if (m.is_false(f))
+        return true;
+    if (m.is_not(f, f) && m.is_true(f))
+        return true;
+    return false;
+}
+
 void finite_set_axioms::add_binary(char const *name, expr *p1, expr *p2, expr *f1, expr *f2) {
+    expr_ref _f1(f1, m), _f2(f2, m);
+    if (is_true(f1) || is_true(f2))
+        return;    
     theory_axiom *ax = alloc(theory_axiom, m, name, p1, p2);
-    ax->clause.push_back(f1);
-    ax->clause.push_back(f2);
+    if (!is_false(f1))
+        ax->clause.push_back(f1);
+    if (!is_false(f2))
+        ax->clause.push_back(f2);
     m_add_clause(ax);
 }
 
 void finite_set_axioms::add_ternary(char const *name, expr *p1, expr *p2, expr *f1, expr *f2, expr *f3) {
+    expr_ref _f1(f1, m), _f2(f2, m), _f3(f3, m);
+    if (is_true(f1) || is_true(f2) || is_true(f3))
+        return;
     theory_axiom *ax = alloc(theory_axiom, m, name, p1, p2);
-    ax->clause.push_back(f1);
-    ax->clause.push_back(f2);
-    ax->clause.push_back(f3);
+    if (!is_false(f1))
+        ax->clause.push_back(f1);
+    if (!is_false(f2))
+        ax->clause.push_back(f2);
+    if (!is_false(f3))
+        ax->clause.push_back(f3);
     m_add_clause(ax);
 }
 
diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h
index 457232fe3..029833fd0 100644
--- a/src/ast/rewriter/finite_set_axioms.h
+++ b/src/ast/rewriter/finite_set_axioms.h
@@ -52,6 +52,10 @@ class finite_set_axioms {
 
     void add_ternary(char const *name, expr *p1, expr *p2, expr *f1, expr *f2, expr *f3);
 
+    bool is_true(expr *f);
+
+    bool is_false(expr *f);
+
 public:
 
     finite_set_axioms(ast_manager &m) : m(m), u(m), m_rewriter(m) {}
diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index ac58b52e2..14208074e 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/src/smt/theory_finite_set.cpp
@@ -331,7 +331,7 @@ namespace smt {
     * - there is not both set.size and set.filter
     */
     bool theory_finite_set::is_fully_solved() {
-        bool has_map = false, has_filter = false, has_size = false;
+        bool has_map = false, has_filter = false, has_size = false, has_range = false;
         for (unsigned v = 0; v < get_num_vars(); ++v) {
             auto n = get_enode(v);
             auto e = n->get_expr();
@@ -341,12 +341,16 @@ namespace smt {
                 has_map = true;
             if (u.is_size(e))
                 has_size = true;
+            if (u.is_range(e))
+                has_range = true;
         }
         TRACE(finite_set, tout << "has-map " << has_map << " has-filter-size " << has_filter << has_size << "\n");
         if (has_map)
             return false; // todo use more expensive model check here
         if (has_filter && has_size)
-            return false; // tood use more expensive model check here
+            return false; // todo use more expensive model check here
+        if (has_range && has_size)
+            return false; // todo use more expensive model check here or even ensure range expressions are handled natively by size.
         return true;
     }
 
@@ -799,8 +803,7 @@ namespace smt {
                     result.push_back(model_value_dependency(n));
         }
 
-        app *mk_value(model_generator &mg, expr_ref_vector const &values) override {            
-            SASSERT(values.empty() == !m_elements);
+        app *mk_value(model_generator &mg, expr_ref_vector const &values) override {   
             auto s = n->get_sort();
             if (values.empty())
                 return th.u.mk_empty(s);