diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f164d6a4f..a927df3b5 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1934,8 +1934,7 @@ sort * ast_manager::substitute(sort* s, unsigned n, sort * const * src, sort * c
     vector<parameter> ps;
     bool change = false;
     sort_ref_vector sorts(*this);
-    for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
-        parameter const& p = s->get_parameter(i);
+    for (parameter const& p : s->parameters()) {
         if (p.is_ast()) {
             SASSERT(is_sort(p.get_ast()));
             change = true;
@@ -2330,8 +2329,8 @@ bool ast_manager::is_label_lit(expr const * n, buffer<symbol> & names) const {
         return false;
     }
     func_decl const * decl = to_app(n)->get_decl();
-    for (unsigned i = 0; i < decl->get_num_parameters(); i++)
-        names.push_back(decl->get_parameter(i).get_symbol());
+    for (parameter const& p : decl->parameters()) 
+        names.push_back(p.get_symbol());
     return true;
 }
 
@@ -2928,8 +2927,8 @@ bool ast_manager::is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector<exp
         not_q_or_i = to_app(e)->get_arg(0);
         func_decl* d = to_app(e)->get_decl();
         SASSERT(binding.empty());
-        for (unsigned i = 0; i < d->get_num_parameters(); ++i) {
-            binding.push_back(to_expr(d->get_parameter(i).get_ast()));
+        for (parameter const& p : d->parameters()) {
+            binding.push_back(to_expr(p.get_ast()));
         }
         return true;
     }
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 7cd1dff93..364be8a77 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -273,6 +273,14 @@ public:
     parameter const * get_parameters() const { return m_parameters.begin(); }
     bool private_parameters() const { return m_private_parameters; }
 
+    struct iterator {
+        decl_info const& d;
+        iterator(decl_info const& d) : d(d) {}
+        parameter const* begin() const { return d.get_parameters(); }
+        parameter const* end() const { return begin() + d.get_num_parameters(); }
+    };
+    iterator parameters() const { return iterator(*this); }
+
     unsigned hash() const;
     bool operator==(decl_info const & info) const;
 };
@@ -571,6 +579,16 @@ public:
     parameter const & get_parameter(unsigned idx) const { return m_info->get_parameter(idx); }
     parameter const * get_parameters() const { return m_info == nullptr ? nullptr : m_info->get_parameters(); }
     bool private_parameters() const { return m_info != nullptr && m_info->private_parameters(); }
+
+    struct iterator {
+        decl const& d;
+        iterator(decl const& d) : d(d) {}
+        parameter const* begin() const { return d.get_parameters(); }
+        parameter const* end() const { return begin() + d.get_num_parameters(); }
+    };
+    iterator parameters() const { return iterator(*this); }
+
+
 };
 
 // -----------------------------------
@@ -2401,11 +2419,7 @@ public:
     }
 
     void reset() {
-        ptr_buffer<ast>::iterator it  = m_to_unmark.begin();
-        ptr_buffer<ast>::iterator end = m_to_unmark.end();
-        for (; it != end; ++it) {
-            reset_mark(*it);
-        }
+        for (ast* a : m_to_unmark) reset_mark(a); 
         m_to_unmark.reset();
     }
 
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 4869949b7..6bbe3ce13 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -401,7 +401,7 @@ bool bv_decl_plugin::get_int2bv_size(unsigned num_parameters, parameter const *
         m_manager->raise_exception("int2bv expects one parameter");
         return false;
     }
-    parameter p(parameters[0]);
+    const parameter &p = parameters[0];
     if (p.is_int()) {
         result = p.get_int();
         return true;
@@ -428,7 +428,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
     // After SMT-COMP, I should find all offending modules.
     // For now, I will just simplify the numeral here.
     parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
-    parameter ps[2] = { p0, parameters[1] };
+    parameter ps[2] = { std::move(p0), parameters[1] };
     sort * bv = get_bv_sort(bv_size);
     return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
 }
@@ -746,7 +746,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
 expr * bv_decl_plugin::get_some_value(sort * s) {
     SASSERT(s->is_sort_of(m_family_id, BV_SORT));
     unsigned bv_size = s->get_parameter(0).get_int();
-    parameter p[2] = { parameter(rational(0)), parameter(static_cast<int>(bv_size)) };
+    parameter p[2] = { parameter(rational::zero()), parameter(static_cast<int>(bv_size)) };
     return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, nullptr);
 }
 
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index d3704a84a..284c4df93 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -692,6 +692,7 @@ namespace datatype {
         }
         unsigned num_well_founded = 0, id = 0;
         bool changed;
+        ptr_vector<sort> subsorts;
         do {
             changed = false;
             for (unsigned tid = 0; tid < num_types; tid++) {
@@ -701,23 +702,25 @@ namespace datatype {
                 sort* s = sorts[tid];
                 def const& d = get_def(s);
                 for (constructor const* c : d) {
-                    bool found_nonwf = false;
                     for (accessor const* a : *c) {
-                        if (sort2id.find(a->range(), id) && !well_founded[id]) {
-                            found_nonwf = true;
-                            break;
+                        subsorts.reset();
+                        get_subsorts(a->range(), subsorts);
+                        for (sort* srt : subsorts) {
+                            if (sort2id.find(srt, id) && !well_founded[id]) {
+                                goto next_constructor;
+                            }
                         }
                     }
-                    if (!found_nonwf) {
-                        changed = true;
-                        well_founded[tid] = true;
-                        num_well_founded++;
-                        break;
-                    }
+                    changed = true;
+                    well_founded[tid] = true;
+                    num_well_founded++;
+                    break;
+                next_constructor:
+                    ;
                 }
             }
         } 
-        while(changed && num_well_founded < num_types);
+        while (changed && num_well_founded < num_types);
         return num_well_founded == num_types;
     }
 
@@ -727,8 +730,7 @@ namespace datatype {
 
     void util::get_subsorts(sort* s, ptr_vector<sort>& sorts) const {
         sorts.push_back(s);
-        for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
-            parameter const& p = s->get_parameter(i);
+        for (parameter const& p : s->parameters()) {
             if (p.is_ast() && is_sort(p.get_ast())) {
                 get_subsorts(to_sort(p.get_ast()), sorts);
             }
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index cd8571a95..00ba93ccb 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -376,8 +376,7 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
     if (s->get_family_id() == sP->get_family_id() &&
         s->get_decl_kind() == sP->get_decl_kind() &&
         s->get_num_parameters() == sP->get_num_parameters()) {
-        for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
-            parameter const& p = s->get_parameter(i);
+        for (parameter const& p : s->parameters()) {
             if (p.is_ast() && is_sort(p.get_ast())) {
                 parameter const& p2 = sP->get_parameter(i);
                 if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;
diff --git a/src/util/lp/general_matrix.h b/src/util/lp/general_matrix.h
index ce510eb6e..1c643161a 100644
--- a/src/util/lp/general_matrix.h
+++ b/src/util/lp/general_matrix.h
@@ -105,12 +105,12 @@ public:
     }
     
     template <typename T>
-    void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> column_fix) {
+    void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> column_fix, const mpq& sign) {
         auto & row = m_data[adjust_row(i)];
         lp_assert(row_is_initialized_correctly(row));
         for (const auto & p : c) {
             unsigned j = adjust_column(column_fix(p.var()));
-            row[j] = p.coeff();
+            row[j] = sign * p.coeff();
         }
     }
     
diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h
index 9a06e1bc9..3f9038651 100644
--- a/src/util/lp/hnf_cutter.h
+++ b/src/util/lp/hnf_cutter.h
@@ -29,6 +29,7 @@ class hnf_cutter {
     var_register               m_var_register;
     general_matrix             m_A;
     vector<const lar_term*>    m_terms;
+    vector<bool>               m_terms_upper;
     svector<constraint_index>  m_constraints_for_explanation;
     vector<mpq>                m_right_sides;
     lp_settings &              m_settings;
@@ -54,15 +55,22 @@ public:
         // m_A will be filled from scratch in init_matrix_A
         m_var_register.clear();
         m_terms.clear();
+        m_terms_upper.clear();
         m_constraints_for_explanation.clear();
         m_right_sides.clear();
         m_abs_max = zero_of_type<mpq>();
         m_overflow = false;
     }
-    void add_term(const lar_term* t, const mpq &rs, constraint_index ci) {
+    void add_term(const lar_term* t, const mpq &rs, constraint_index ci, bool upper_bound) {
         m_terms.push_back(t);
-        m_right_sides.push_back(rs);
+        m_terms_upper.push_back(upper_bound);
+        if (upper_bound)
+            m_right_sides.push_back(rs);
+        else
+            m_right_sides.push_back(-rs);
+        
         m_constraints_for_explanation.push_back(ci);
+       
         for (const auto &p : *t) {
             m_var_register.add_var(p.var());
             mpq t = abs(ceil(p.coeff()));
@@ -76,7 +84,8 @@ public:
     }
 
     void initialize_row(unsigned i) {
-        m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);});
+        mpq sign = m_terms_upper[i]? one_of_type<mpq>(): - one_of_type<mpq>();
+        m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);}, sign);
     }
 
     void init_matrix_A() {
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 8bc2056b4..29dd9eed8 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -537,8 +537,9 @@ void int_solver::try_add_term_to_A_for_hnf(unsigned i) {
     mpq rs;
     const lar_term* t = m_lar_solver->terms()[i];
     constraint_index ci;
-    if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci)) {
-        m_hnf_cutter.add_term(t, rs, ci);
+    bool upper_bound;
+    if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) {
+        m_hnf_cutter.add_term(t, rs, ci, upper_bound);
     }
 }
 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 99a0c5883..f8d16ab8c 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -2227,8 +2227,19 @@ void lar_solver::round_to_integer_solution() {
         update_delta_for_terms(del, j, vars_to_terms[j]);
     }
 }
+// return true if all y coords are zeroes
+bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const {
+    val = zero_of_type<mpq>();
+    for (const auto & c : t) {
+        const auto & x = m_mpq_lar_core_solver.m_r_x[c.var()];
+        if (!is_zero(x.y))
+            return false;
+        val += x.x * c.coeff();
+    }
+    return true;
+}
 
-bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci) const {
+bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci, bool &upper_bound) const {
     unsigned tj = term_index + m_terms_start_index;
     unsigned j;
     bool is_int;
@@ -2236,26 +2247,29 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term
         return false; // the term does not have a bound because it does not correspond to a column
     if (!is_int) // todo - allow for the next version of hnf
         return false;
-    impq term_val;
-    bool term_val_ready = false;
+    bool rs_is_calculated = false;
     mpq b;
     bool is_strict;
+    const lar_term& t = *terms()[term_index];
     if (has_upper_bound(j, ci, b, is_strict) && !is_strict) {
         lp_assert(b.is_int());
-        term_val = terms()[term_index]->apply(m_mpq_lar_core_solver.m_r_x);
-        term_val_ready = true;
-        if (term_val.x == b) {
-            rs = b;
+        if (!sum_first_coords(t, rs))
+            return false;
+        rs_is_calculated = true;
+        if (rs == b) {
+            upper_bound = true;
             return true;
         }
     }
     if (has_lower_bound(j, ci, b, is_strict) && !is_strict) {
-        if (!term_val_ready)
-            term_val = terms()[term_index]->apply(m_mpq_lar_core_solver.m_r_x);
+        if (!rs_is_calculated){
+            if (!sum_first_coords(t, rs))
+                return false;
+        }
         lp_assert(b.is_int());
         
-        if (term_val.x == b) {
-            rs = b;
+        if (rs == b) {
+            upper_bound = false;
             return true;
         }
     }
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index f17aa4a0d..72705dfb3 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -573,9 +573,10 @@ public:
     unsigned column_count() const { return A_r().column_count(); }
     const vector<unsigned> & r_basis() const { return m_mpq_lar_core_solver.r_basis(); }
     const vector<unsigned> & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); }
-    bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci) const;
+    bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci, bool &upper_bound) const;
     bool remove_from_basis(unsigned);
     lar_term get_term_to_maximize(unsigned ext_j) const;
     void set_cut_strategy(unsigned cut_frequency);
+    bool sum_first_coords(const lar_term& t, mpq & val) const;
 };
 }
diff --git a/src/util/trace.h b/src/util/trace.h
index c0dc90f23..1a245036f 100644
--- a/src/util/trace.h
+++ b/src/util/trace.h
@@ -51,7 +51,6 @@ void finalize_trace();
 static inline void enable_trace(const char * tag) {}
 static inline void enable_all_trace(bool flag) {}
 static inline void disable_trace(const char * tag) {}
-// On a default Visual C++ build on Windows, a non-void function either needs to return a value, or we have to add: #pragma warning(default:4716)  
 static inline bool is_trace_enabled(const char * tag) { return false; }
 static inline void close_trace() {}
 static inline void open_trace() {}