diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 27c52140f..13957064e 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -59,6 +59,8 @@ Version 4.3.2
 
 - Fixed http://stackoverflow.com/questions/14524316/z3-4-3-get-complete-model.
 
+- Fixed bugs in the C++ API (Thanks to Andrey Kupriyanov).
+
 Version 4.3.1
 =============
 
diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py
index 3b9511367..8256236cb 100644
--- a/scripts/mk_unix_dist.py
+++ b/scripts/mk_unix_dist.py
@@ -190,7 +190,7 @@ def mk_zip():
     try:
         os.chdir(DIST_DIR)
         zfname = '%s.zip' % dist_path
-        ZIPOUT = zipfile.ZipFile(zfname, 'w')
+        ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
         os.path.walk(dist_path, mk_zip_visitor, '*')
         if is_verbose():
             print "Generated '%s'" % zfname
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 4e1a38af2..873c22b80 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -76,10 +76,7 @@ GPROF=False
 GIT_HASH=False
 
 def check_output(cmd):
-    try:
-        return subprocess.check_output(cmd, shell=True).rstrip('\r\n')
-    except:
-        return subprocess.check_output(cmd).rstrip('\r\n')
+    return subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0].rstrip('\r\n')
 
 def git_hash():
     try:
diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
index 137ea431c..a52c8af43 100644
--- a/scripts/mk_win_dist.py
+++ b/scripts/mk_win_dist.py
@@ -205,7 +205,7 @@ def mk_zip_core(x64):
     try:
         os.chdir(DIST_DIR)
         zfname = '%s.zip' % dist_path
-        ZIPOUT = zipfile.ZipFile(zfname, 'w')
+        ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
         os.path.walk(dist_path, mk_zip_visitor, '*')
         if is_verbose():
             print "Generated '%s'" % zfname
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 5c1e6ca0c..5af4bf60b 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -619,6 +619,8 @@ namespace z3 {
             a.check_error();
             return expr(a.ctx(), r);
         }
+        friend expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
+        friend expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
 
         /**
            \brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
@@ -758,7 +760,7 @@ namespace z3 {
             return expr(a.ctx(), r);
         }
         friend expr operator-(expr const & a, int b) { return a - a.ctx().num_val(b, a.get_sort()); }
-        friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - a; }
+        friend expr operator-(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) - b; }
 
         friend expr operator<=(expr const & a, expr const & b) {
             check_context(a, b);
@@ -777,7 +779,7 @@ namespace z3 {
             return expr(a.ctx(), r);
         }
         friend expr operator<=(expr const & a, int b) { return a <= a.ctx().num_val(b, a.get_sort()); }
-        friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= a; }
+        friend expr operator<=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) <= b; }
 
         friend expr operator>=(expr const & a, expr const & b) {
             check_context(a, b);
@@ -796,7 +798,7 @@ namespace z3 {
             return expr(a.ctx(), r);
         }
         friend expr operator>=(expr const & a, int b) { return a >= a.ctx().num_val(b, a.get_sort()); }
-        friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= a; }
+        friend expr operator>=(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) >= b; }
 
         friend expr operator<(expr const & a, expr const & b) {
             check_context(a, b);
@@ -815,7 +817,7 @@ namespace z3 {
             return expr(a.ctx(), r);
         }
         friend expr operator<(expr const & a, int b) { return a < a.ctx().num_val(b, a.get_sort()); }
-        friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < a; }
+        friend expr operator<(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) < b; }
         
         friend expr operator>(expr const & a, expr const & b) {
             check_context(a, b);
@@ -834,7 +836,7 @@ namespace z3 {
             return expr(a.ctx(), r);
         }
         friend expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
-        friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > a; }
+        friend expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
 
         friend expr operator&(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
         friend expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
@@ -888,31 +890,31 @@ namespace z3 {
     */
     inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
     inline expr ule(expr const & a, int b) { return ule(a, a.ctx().num_val(b, a.get_sort())); }
-    inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), a); }
+    inline expr ule(int a, expr const & b) { return ule(b.ctx().num_val(a, b.get_sort()), b); }
     /**
        \brief unsigned less than operator for bitvectors.
     */
     inline expr ult(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
     inline expr ult(expr const & a, int b) { return ult(a, a.ctx().num_val(b, a.get_sort())); }
-    inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), a); }
+    inline expr ult(int a, expr const & b) { return ult(b.ctx().num_val(a, b.get_sort()), b); }
     /**
        \brief unsigned greater than or equal to operator for bitvectors.
     */
     inline expr uge(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
     inline expr uge(expr const & a, int b) { return uge(a, a.ctx().num_val(b, a.get_sort())); }
-    inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), a); }
+    inline expr uge(int a, expr const & b) { return uge(b.ctx().num_val(a, b.get_sort()), b); }
     /**
        \brief unsigned greater than operator for bitvectors.
     */
     inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
     inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
-    inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), a); }
+    inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
     /**
        \brief unsigned division operator for bitvectors.
     */
     inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
     inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
-    inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), a); }
+    inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
 
     // Basic functions for creating quantified formulas.
     // The C API should be used for creating quantifiers with patterns, weights, many variables, etc.
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 704ae9fc8..8d643a348 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1849,9 +1849,9 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
             sort * given = get_sort(args[i]);
             if (!compatible_sorts(expected, given)) {
                 std::ostringstream buff;
-                buff << "Invalid function application for " << decl->get_name() << ". ";
-                buff << "Sort mismatch on argument at position " << (i+1) << ". ";
-                buff << "Expected: " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
+                buff << "invalid function application for " << decl->get_name() << ", ";
+                buff << "sort mismatch on argument at position " << (i+1) << ", ";
+                buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
                 throw ast_exception(buff.str().c_str());
             }
         }
@@ -1865,9 +1865,9 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
             sort * given    = get_sort(args[i]);
             if (!compatible_sorts(expected, given)) {
                 std::ostringstream buff;
-                buff << "Invalid function application for " << decl->get_name() << ". ";
-                buff << "Sort mismatch on argument at position " << (i+1) << ". ";
-                buff << "Expected: " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
+                buff << "invalid function application for " << decl->get_name() << ", ";
+                buff << "sort mismatch on argument at position " << (i+1) << ", ";
+                buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
                 throw ast_exception(buff.str().c_str());
             }
         }
diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp
index 70bd4b0dd..e89d7807b 100644
--- a/src/muz_qe/hilbert_basis.cpp
+++ b/src/muz_qe/hilbert_basis.cpp
@@ -21,413 +21,222 @@ Revision History:
 #include "heap.h"
 #include "map.h"
 
-typedef u_map<unsigned> offset_refs_t;
-
 template<typename Value>
 class rational_map : public map<rational, Value, rational::hash_proc, rational::eq_proc> {};
 
-class rational_abs_lt {
-    vector<rational> & m_values;
-public:
-    rational_abs_lt(vector<rational> & values):
-        m_values(values) {
-    }
-    bool operator()(int v1, int v2) const {
-        return m_values[v1] < m_values[v2];
-    }
-};
 
-
-class hilbert_basis::rational_heap {
-    vector<numeral>          m_u2r;     // [index |-> weight]
-    rational_map<unsigned>   m_r2u;     // [weight |-> index]
-    rational_abs_lt          m_lt;      // less_than on indices
-    heap<rational_abs_lt>    m_heap;    // binary heap over weights
-public:
-
-    rational_heap(): m_lt(m_u2r), m_heap(10, m_lt) {}
-
-    vector<numeral>& u2r() { return m_u2r; }
-
-    void insert(unsigned v) {
-        m_heap.insert(v);
-    }
-
-    void reset() {
-        m_u2r.reset();
-        m_r2u.reset();
-        m_heap.reset();
-    }
-
-    bool is_declared(numeral const& r, unsigned& val) const {
-        return m_r2u.find(r, val);
-    }
-
-    unsigned declare(numeral const& r) {
-        SASSERT(!m_r2u.contains(r));
-        unsigned val = m_u2r.size();
-        m_u2r.push_back(r);
-        m_r2u.insert(r, val);
-        m_heap.set_bounds(val+1);
-        return val;
-    }
-
-    void find_le(unsigned val, int_vector & result) {
-        m_heap.find_le(val, result);
-    }
-
-};
-
-class hilbert_basis::weight_map {
+class hilbert_basis::value_index {
     struct stats {
         unsigned m_num_comparisons;
+        unsigned m_num_hit;
+        unsigned m_num_miss;
+
         stats() { reset(); }
         void reset() { memset(this, 0, sizeof(*this)); }
     };    
 
-    rational_heap            m_heap;         
-    vector<unsigned_vector>  m_offsets;      // [index |-> offset-list]
-    int_vector               m_le;           // recycled set of indices with lesser weights
-    stats                    m_stats;
-    svector<offset_t>&       m_found;
-    offset_refs_t&           m_refs;
-    unsigned                 m_cost;
+    typedef int_hashtable<int_hash, default_eq<int> > int_table;
+    hilbert_basis&     hb;
+    int_table          m_table;
+    stats              m_stats;
 
-    unsigned get_value(numeral const& w) {
-        numeral r = abs(w);
-        unsigned val;
-        if (!m_heap.is_declared(r, val)) {
-            val = m_heap.declare(r);
-            SASSERT(val == m_offsets.size());
-            if (r.is_nonneg()) {
-                m_heap.insert(val);
-            }
-            m_offsets.push_back(unsigned_vector());
-        }
-        return val;
-    }
 public:
-    weight_map(svector<offset_t>& found, offset_refs_t& refs): m_found(found), m_refs(refs) {}
-    
-    void insert(offset_t idx, numeral const& w) {
-        unsigned val = get_value(w);
-        m_offsets[val].push_back(idx.m_offset);
+    value_index(hilbert_basis& hb):
+        hb(hb)
+    {}
+
+    void insert(offset_t idx, values const& vs) {
+        m_table.insert(idx.m_offset);
     }
 
-    void remove(offset_t idx, numeral const& w) {
-        unsigned val = get_value(w);
-        m_offsets[val].erase(idx.m_offset);
-    }
-
-    unsigned get_size() const {
-        unsigned sz = 0;
-        for (unsigned i = 0; i < m_offsets.size(); ++i) {
-            sz += m_offsets[i].size();
-        }
-        return sz;
+    void remove(offset_t idx, values const& vs) {
+        m_table.remove(idx.m_offset);
     }
 
     void reset() {
-        m_offsets.reset();
-        m_heap.reset();
-        m_le.reset();
-    }
-    
-    unsigned get_cost() const { return m_cost; }
-
-    /**
-       retrieve 
-     */
-    bool init_find(numeral const& w, offset_t idx) {
-        m_le.reset();
-        m_found.reset();
-        m_cost = 0;
-        unsigned val = get_value(w);
-        // for positive values, the weights should be less or equal.
-        // for non-positive values, the weights have to be the same.
-        if (w.is_pos()) {
-            m_heap.find_le(val, m_le);
-        }
-        else {
-            m_le.push_back(val);
-        }
-        for (unsigned i = 0; i < m_le.size(); ++i) {
-            if (m_heap.u2r()[m_le[i]].is_zero() && !w.is_zero()) {
-                continue;
-            } 
-            unsigned_vector const& offsets = m_offsets[m_le[i]];
-            for (unsigned j = 0; j < offsets.size(); ++j) {
-                unsigned offs = offsets[j];
-                ++m_stats.m_num_comparisons;
-                ++m_cost;
-                if (offs != idx.m_offset) {
-                    m_refs.insert(offs, 0);
-                    m_found.push_back(offset_t(offs));
-                }
-            }
-        }
-        return !m_found.empty();
+        m_table.reset();
     }
 
-    unsigned get_find_cost(numeral const& w) {
-        m_le.reset();
-        unsigned cost = 0;
-        unsigned val = get_value(w);
-        m_heap.find_le(val, m_le);
-        for (unsigned i = 0; i < m_le.size(); ++i) {
-            cost += m_offsets[m_le[i]].size();
-        }
-        return cost;        
-    }
-    
-    bool update_find(unsigned round, numeral const& w, offset_t idx) {
-        m_found.reset();
-        m_le.reset();
-        m_cost = 0;
-        unsigned vl = get_value(w);
-        m_heap.find_le(vl, m_le);
-        for (unsigned i = 0; i < m_le.size(); ++i) {
-            unsigned_vector const& offsets = m_offsets[m_le[i]];
-            for (unsigned j = 0; j < offsets.size(); ++j) {
-                unsigned offs = offsets[j];
-                ++m_stats.m_num_comparisons;
-                ++m_cost;
-                if (offs != idx.m_offset && m_refs.find(offs, vl) && vl == round) {
-                    m_refs.insert(offs, round + 1);
-                    m_found.push_back(offset_t(offs));
-                }
+    bool find(offset_t idx, values const& vs, offset_t& found_idx) {
+        // display_profile(idx, std::cout);
+        int_table::iterator it = m_table.begin(), end = m_table.end();
+        for (; it != end; ++it) {
+            offset_t offs(*it);
+            ++m_stats.m_num_comparisons;
+            if (*it != idx.m_offset && hb.is_subsumed(idx, offs)) {
+                found_idx = offs;
+                ++m_stats.m_num_hit;
+                return true;
             }
         }
-        return !m_found.empty();
-    }    
+        ++m_stats.m_num_miss;
+        return false;
+    }
 
     void collect_statistics(statistics& st) const {
         st.update("hb.index.num_comparisons", m_stats.m_num_comparisons);
+        st.update("hb.index.num_hit", m_stats.m_num_hit);
+        st.update("hb.index.num_miss", m_stats.m_num_miss);
     }
 
     void reset_statistics() {
         m_stats.reset();
     }
-};
 
-
-class hilbert_basis::value_index {
-    hilbert_basis&         hb;
-    ptr_vector<weight_map> m_values;
-    offset_refs_t          m_refs;
-    svector<offset_t>      m_found;
-    weight_map             m_weight;
-
-public:
-    value_index(hilbert_basis& hb): hb(hb) {}
-
-    ~value_index() {
-        for (unsigned i = 0; i < m_values.size(); ++i) {
-            dealloc(m_values[i]);
-        }
+    unsigned size() const {
+        return m_table.size();
     }
-
-    void init(unsigned num_vars) {
-        if (m_values.empty()) {
-            for (unsigned i = 0; i < num_vars; ++i) {
-                m_values.push_back(alloc(weight_map, m_found, m_refs));
+private:
+    void display_profile(offset_t idx, std::ostream& out) {
+        unsigned_vector leq;
+        unsigned nv = hb.get_num_vars();
+        values const& vs = hb.vec(idx);
+        leq.resize(nv+1);
+        numeral maxw(0);
+        for (unsigned i = 0; i < nv; ++i) {
+            if (!hb.is_abs_geq(maxw, vs[i])) {
+                maxw = vs[i];
             }
         }
-        SASSERT(m_values.size() == num_vars);
-    }
-
-    void insert(offset_t idx, values const& vs) {
-        for (unsigned i = 0; i < m_values.size(); ++i) {
-            m_values[i]->insert(idx, vs[i]);
+        unsigned num_below_max = 0;
+        int_table::iterator it = m_table.begin(), end = m_table.end();
+        for (; it != end; ++it) {
+            offset_t offs(*it);
+            values const& ws = hb.vec(offs);
+            if (ws.weight() <= vs.weight()) {
+                leq[0]++;
+            }
+            bool filtered = false;
+            for (unsigned i = 0; i < nv; ++i) {
+                if (hb.is_abs_geq(vs[i], ws[i])) {
+                    leq[i+1]++;
+                }
+                if (!hb.is_abs_geq(maxw, ws[i])) {
+                    filtered = true;
+                }
+            }
+            if (!filtered) {
+                ++num_below_max;
+            }
         }
-    }
-
-    void remove(offset_t idx, values const& vs) {
-        for (unsigned i = 0; i < m_values.size(); ++i) {
-            m_values[i]->remove(idx, vs[i]);
+        out << vs.weight() << ":" << leq[0] << " ";
+        for (unsigned i = 0; i < nv; ++i) {
+            out << vs[i] << ":" << leq[i+1] << " ";
         }
+        out << " max<= " << num_below_max;
+        out << "\n";
     }
 };
 
+
+
 class hilbert_basis::index {
-    // for each index, a heap of weights.
-    // for each weight a list of offsets
+    // for each non-positive weight a separate index.
+    // for positive weights a shared value index.
 
     struct stats {
-        unsigned m_num_comparisons;
         unsigned m_num_find;
         unsigned m_num_insert;
         stats() { reset(); }
         void reset() { memset(this, 0, sizeof(*this)); }
-    };    
-    
-    hilbert_basis&     hb;
-    value_index        m_values;
-    rational_map<value_index*> m_negative;
-    stats              m_stats;
+    };        
+
+    typedef rational_map<value_index*> value_map;
+    hilbert_basis&   hb;
+    value_map        m_neg;
+    value_index      m_pos;
+    value_index      m_zero;
+    stats            m_stats;
 
 public:
-
-    index(hilbert_basis& hb): 
-        hb(hb), 
-        m_weight(m_found, m_refs),
-        m_values(hb) {}
-
-    ~index() {
-        rational_map<weight_map*>::iterator it = m_negative.begin(), end = m_negative.end();
-        for (; it != end; ++it) {
-            dealloc(it->m_value);
-        }
-    }
-
-    void init(unsigned num_vars) {
-        m_values.init(num_vars);
-        m_num_vars = num_vars;
-        SASSERT(m_negative.empty());
-    }
+    index(hilbert_basis& hb): hb(hb), m_pos(hb), m_zero(hb) {}
     
     void insert(offset_t idx, values const& vs) {
         ++m_stats.m_num_insert;
-        if (vs.value().is_neg()) {
-            weight_map* w = 0;
-            if (!m_negative.find(vs.value(), w)) {
-                w = alloc(weight_map, m_found, m_refs);
-            }
-            w->insert(idx, vs);
+        if (vs.weight().is_pos()) {
+            m_pos.insert(idx, vs);
+        }
+        else if (vs.weight().is_zero()) {
+            m_zero.insert(idx, vs);
         }
         else {
-            m_weight.insert(idx, vs.value());
-            m_values.insert(idx, vs);
+            value_index* map = 0;
+            if (!m_neg.find(vs.weight(), map)) {
+                map = alloc(value_index, hb);
+                m_neg.insert(vs.weight(), map);
+            }
+            map->insert(idx, vs);
         }
     }
 
     void remove(offset_t idx, values const& vs) {
-        if (vs.value().is_neg()) {
-            weight_map* w = m_negative.find(vs.value());
-            w->remove(idx, vs);
+        if (vs.weight().is_pos()) {
+            m_pos.remove(idx, vs);
+        }
+        else if (vs.weight().is_zero()) {
+            m_zero.remove(idx, vs);
         }
         else {
-            m_weight.remove(idx, vs.value());
-            m_values.remove(idx, vs);
-        }
+            m_neg.find(vs.weight())->remove(idx, vs);
+        }        
     }
 
-    bool find(values const& vs, offset_t idx, offset_t& found_idx) {
+    bool find(offset_t idx, values const& vs, offset_t& found_idx) {
         ++m_stats.m_num_find;
-        m_refs.reset();
-        bool found = m_weight.init_find(vs.value(), idx);
-        TRACE("hilbert_basis", tout << "init: " << m_found.size() << " cost: " << m_weight.get_cost() << "\n";);
-#if 0
-        std::cout << vs.value() << " " << m_found.size() << " ";
-        for (unsigned i = 0; i < m_values.size(); ++i) {
-            std::cout << vs[i] << ": " << m_values[i]->get_find_cost(vs[i]) << " ";
+        if (vs.weight().is_pos()) {
+            return m_pos.find(idx,  vs, found_idx); 
         }
-        std::cout << "\n";
-#endif
-#if 0
-        for (unsigned i = 0; found && i < m_values.size(); ++i) {
-            found = m_values[i]->update_find(i, vs[i], idx);
-            std::cout << vs[i] << ": " << m_found.size() << " ";
-            TRACE("hilbert_basis", tout << "update " << i << ": " << m_found.size() << " cost: " << m_values[i]->get_cost() << "\n";);
+        else if (vs.weight().is_zero()) {
+            return m_zero.find(idx, vs, found_idx);
         }
-#else
-        for (unsigned i = 0; i < m_found.size(); ++i) {
-            if (is_subsumed(idx, m_found[i])) {
-                found_idx = m_found[i];
-                return true;
-            }
-        }
-        return false;
-#endif
-
-        if (found) {
-            found_idx = m_found[0];
-        }
-        return found;
-    }
+        else {
+            value_index* map;
+            return
+                m_neg.find(vs.weight(), map) && 
+                map->find(idx, vs, found_idx);
+        }        
+    }    
 
     void reset() {
-        for (unsigned i = 0; i < m_values.size(); ++i) {
-            m_values[i]->reset();
+        m_pos.reset();
+        m_neg.reset();
+        value_map::iterator it = m_neg.begin(), end = m_neg.end();
+        for (; it != end; ++it) {
+            it->m_value->reset();
         }
-        m_weight.reset();
-        m_refs.reset();
     }
 
     void collect_statistics(statistics& st) const {
-        m_weight.collect_statistics(st);
-        for (unsigned i = 0; i < m_values.size(); ++i) {
-            m_values[i]->collect_statistics(st);
-        }        
-        st.update("hb.index.num_find", m_stats.m_num_find);
+        m_pos.collect_statistics(st);
+        m_zero.collect_statistics(st);
+        value_map::iterator it = m_neg.begin(), end = m_neg.end();
+        for (; it != end; ++it) {
+            it->m_value->collect_statistics(st);
+        }
+        st.update("hb.index.num_find",   m_stats.m_num_find);
         st.update("hb.index.num_insert", m_stats.m_num_insert);
-        st.update("hb.index.size", m_weight.get_size());
+        st.update("hb.index.size",       size());
     }
 
     void reset_statistics() {
-        m_stats.reset();
-        m_weight.reset_statistics();
-        for (unsigned i = 0; i < m_values.size(); ++i) {
-            m_values[i]->reset_statistics();
-        }        
-    }
-
-
-    /**
-       Vector v is subsumed by vector w if
-       
-       v[i] >= w[i] for each index i.
-       
-       a*v >= a*w  for the evaluation of vectors with respect to a.
-       
-       a*v < 0 => a*v = a*w
-       
-
-       Justification:
-       
-       let u := v - w, then
-       
-       u[i] >= 0  for each index i
-       
-       a*u = a*(v-w) >= 0
-       
-       So v = u + w, where a*u >= 0, a*w >= 0.
-       
-       If a*v >= a*w >= 0 then v and w are linear 
-       solutions of e_i, and also v-w is a solution.
-
-       If a*v = a*w < 0, then a*(v-w) = 0, so v can be obtained from w + (v - w).
-       
-    */
-
-    bool is_subsumed(offset_t i, offset_t j) const {
-        values v = hb.vec(i);
-        values w = hb.vec(j);
-        numeral const& n = v.value();
-        numeral const& m = w.value();
-        bool r = 
-            i.m_offset != j.m_offset &&         
-            n >= m && (!m.is_neg() || n == m) &&
-            is_geq(v, w);
-        CTRACE("hilbert_basis", r, 
-               hb.display(tout, i);
-               tout << " <= \n";
-               hb.display(tout, j);
-               tout << "\n";);
-        return r;
-    }
-
-    bool is_geq(values v, values w) const {
-        unsigned nv = hb.get_num_vars();
-        for (unsigned i = 0; i < nv; ++i) {
-            if (v[i] < w[i]) {
-                return false;
-            }
+        m_pos.reset_statistics();
+        m_zero.reset_statistics();
+        value_map::iterator it = m_neg.begin(), end = m_neg.end();
+        for (; it != end; ++it) {
+            it->m_value->reset_statistics();
         }
-        return true;
     }
-
-
+    
+private:
+    unsigned size() const {
+        unsigned sz = m_pos.size();
+        sz += m_zero.size();
+        value_map::iterator it = m_neg.begin(), end = m_neg.end();
+        for (; it != end; ++it) {
+            sz += it->m_value->size();
+        }        
+        return sz;
+    }
 };
 
 /**
@@ -435,18 +244,24 @@ public:
 */
 
 class hilbert_basis::passive {
-    hilbert_basis&         hb;
-    svector<offset_t>      m_passive;
-    vector<numeral>        m_weights;
-    unsigned_vector        m_free_list;
-    rational_abs_lt        m_lt;      // less_than on indices
-    heap<rational_abs_lt>  m_heap;    // binary heap over weights
+    struct lt {
+        passive& p;
+        lt(passive& p): p(p) {}
+        bool operator()(int v1, int v2) const {
+            return p(v1, v2);
+        }
+    };
+    hilbert_basis&      hb;
+    svector<offset_t>   m_passive;
+    unsigned_vector     m_free_list;
+    lt                  m_lt;
+    heap<lt>            m_heap;    // binary heap over weights
 
-    numeral get_weight(offset_t idx) {
+    numeral get_value(offset_t idx) const {
         numeral w(0);
         unsigned nv = hb.get_num_vars();
         for (unsigned i = 0; i < nv; ++i) {
-            w += hb.vec(idx)[i];
+            w += abs(hb.vec(idx)[i]);
         }
         return w;
     }
@@ -455,14 +270,14 @@ public:
     
     passive(hilbert_basis& hb): 
         hb(hb) ,
-        m_lt(m_weights),
+        m_lt(*this),
         m_heap(10, m_lt)
-    {}
+    {
+    }
 
     void reset() {
         m_heap.reset();
         m_free_list.reset();
-        m_weights.reset();
         m_passive.reset();
     }
     
@@ -484,14 +299,12 @@ public:
         if (m_free_list.empty()) {
             v = m_passive.size();
             m_passive.push_back(idx);
-            m_weights.push_back(get_weight(idx));
             m_heap.set_bounds(v+1);
         }
         else {
             v = m_free_list.back();
             m_free_list.pop_back();
             m_passive[v] = idx;
-            m_weights[v] = get_weight(idx);
         }
         m_heap.insert(v);
     }
@@ -522,6 +335,43 @@ public:
     iterator end() {
         return iterator(*this, m_passive.size());
     }
+
+public:
+    /**
+       Prefer positive weights to negative.
+       If both weights are positive, prefer the smallest weight.
+       If weights are the same, prefer the one that has smallest sum of values.
+     */
+    bool operator()(int v1, int v2) const {
+        offset_t idx1 = m_passive[v1];
+        offset_t idx2 = m_passive[v2];
+        return get_value(idx1) < get_value(idx2);
+#if 0
+        values const& vec1 = hb.vec(idx1);
+        values const& vec2 = hb.vec(idx2);
+        numeral const& w1 = vec1.weight();
+        numeral const& w2 = vec2.weight();
+        SASSERT(!w1.is_zero());
+        SASSERT(!w2.is_zero());
+
+        if (w1.is_pos()) {
+            if (w2.is_neg()) {
+                return true;
+            }
+            if (w1 != w2) {
+                return w1 < w2;
+            }
+        }
+        else {
+            if (w2.is_pos()) {
+                return false;
+            }
+        }
+        SASSERT(w1 == w2);
+        return get_value(idx1) < get_value(idx2);
+#endif
+    }
+
 };
 
 hilbert_basis::hilbert_basis(): 
@@ -573,10 +423,8 @@ void hilbert_basis::add_ge(num_vector const& v, numeral const& b) {
     num_vector w;
     w.push_back(-b);
     w.append(v);
-    if (m_ineqs.empty()) {
-        m_index->init(w.size());
-    }
     m_ineqs.push_back(w);
+    m_iseq.push_back(false);
 }
 
 void hilbert_basis::add_le(num_vector const& v, numeral const& b) {
@@ -588,8 +436,12 @@ void hilbert_basis::add_le(num_vector const& v, numeral const& b) {
 }
 
 void hilbert_basis::add_eq(num_vector const& v, numeral const& b) {
-    add_le(v, b);
-    add_ge(v, b);
+    SASSERT(m_ineqs.empty() || v.size() + 1 == get_num_vars());
+    num_vector w;
+    w.push_back(-b);
+    w.append(v);
+    m_ineqs.push_back(w);
+    m_iseq.push_back(true);
 }
 
 void hilbert_basis::add_ge(num_vector const& v) {
@@ -601,8 +453,15 @@ void hilbert_basis::add_le(num_vector const& v) {
 }
 
 void hilbert_basis::add_eq(num_vector const& v) {
-    add_le(v);
-    add_ge(v);
+    add_eq(v, numeral(0));
+}
+
+void hilbert_basis::set_is_int(unsigned var_index) {
+    //
+    // The 0't index is reserved for the constant
+    // coefficient. Shift indices by 1.
+    //
+    m_ints.push_back(var_index+1);
 }
 
 unsigned hilbert_basis::get_num_vars() const {
@@ -624,26 +483,36 @@ void hilbert_basis::init_basis() {
     m_free_list.reset();
     unsigned num_vars = get_num_vars();
     for (unsigned i = 0; i < num_vars; ++i) {
-        num_vector w(num_vars, numeral(0));
-        w[i] = numeral(1);
-        offset_t idx = alloc_vector();
-        values v = vec(idx);
-        for (unsigned i = 0; i < num_vars; ++i) {
-            v[i] = w[i];
-        }
-        m_basis.push_back(idx);
+        add_unit_vector(i, numeral(1));
     }
+    for (unsigned i = 0; i < m_ints.size(); ++i) {
+        add_unit_vector(m_ints[i], numeral(-1));
+    }
+}
+ 
+void hilbert_basis::add_unit_vector(unsigned i, numeral const& e) {
+    unsigned num_vars = get_num_vars();
+    num_vector w(num_vars, numeral(0));
+    w[i] = e;
+    offset_t idx = alloc_vector();
+    values v = vec(idx);
+    for (unsigned j = 0; j < num_vars; ++j) {
+        v[j] = w[j];
+    }
+    m_basis.push_back(idx);            
 }
 
 lbool hilbert_basis::saturate() {
-    init_basis();    
-    for (unsigned i = 0; !m_cancel && i < m_ineqs.size(); ++i) {
-        lbool r = saturate(m_ineqs[i]);
+    init_basis();
+    m_current_ineq = 0;
+    while (!m_cancel && m_current_ineq < m_ineqs.size()) {
+        select_inequality();
+        lbool r = saturate(m_ineqs[m_current_ineq], m_iseq[m_current_ineq]);
         ++m_stats.m_num_saturations;
         if (r != l_true) {
             return r;
-        }
-        
+        }        
+        ++m_current_ineq;
     }
     if (m_cancel) {
         return l_undef;
@@ -651,19 +520,19 @@ lbool hilbert_basis::saturate() {
     return l_true;
 }
 
-lbool hilbert_basis::saturate(num_vector const& ineq) {
+lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) {
     m_active.reset();
     m_passive->reset();
     m_zero.reset();
     m_index->reset();
-    TRACE("hilbert_basis", display_ineq(tout, ineq););
+    TRACE("hilbert_basis", display_ineq(tout, ineq, is_eq););
     bool has_non_negative = false;
     iterator it = begin();
     for (; it != end(); ++it) {
         values v = vec(*it);
-        set_eval(v, ineq);
+        v.weight() = get_weight(v, ineq);
         add_goal(*it);
-        if (v.value().is_nonneg()) {
+        if (v.weight().is_nonneg()) {
             has_non_negative = true;
         }
     }
@@ -694,9 +563,9 @@ lbool hilbert_basis::saturate(num_vector const& ineq) {
     // Move positive from active and zeros to new basis.
     m_basis.reset();
     m_basis.append(m_zero);
-    for (unsigned i = 0; i < m_active.size(); ++i) {
+    for (unsigned i = 0; !is_eq && i < m_active.size(); ++i) {
         offset_t idx = m_active[i];
-        if (vec(idx).value().is_pos()) {
+        if (vec(idx).weight().is_pos()) {
             m_basis.push_back(idx);
         }
         else {
@@ -710,6 +579,52 @@ lbool hilbert_basis::saturate(num_vector const& ineq) {
     return l_true;
 }
 
+void hilbert_basis::select_inequality() {
+    SASSERT(m_current_ineq < m_ineqs.size());
+    unsigned best = m_current_ineq;
+    unsigned non_zeros = get_num_nonzeros(m_ineqs[best]);
+    unsigned prod      = get_ineq_product(m_ineqs[best]);
+    for (unsigned j = best+1; prod != 0 && j < m_ineqs.size(); ++j) {
+        unsigned non_zeros2 = get_num_nonzeros(m_ineqs[j]);
+        unsigned prod2 = get_ineq_product(m_ineqs[j]);
+        if (prod2 < prod || (prod2 == prod && non_zeros2 < non_zeros)) {
+            prod = prod2;
+            non_zeros = non_zeros2;
+            best = j;
+        }
+    }
+    if (best != m_current_ineq) {
+        std::swap(m_ineqs[m_current_ineq], m_ineqs[best]);
+        std::swap(m_iseq[m_current_ineq], m_iseq[best]);
+    }
+}
+
+unsigned hilbert_basis::get_num_nonzeros(num_vector const& ineq) {
+    unsigned count = 0;
+    for (unsigned i = 0; i < ineq.size(); ++i) {
+        if (!ineq[i].is_zero()) {
+            ++count;
+        }
+    }
+    return count;
+}
+
+unsigned hilbert_basis::get_ineq_product(num_vector const& ineq) {
+    unsigned num_pos = 0, num_neg = 0;
+    iterator it = begin();
+    for (; it != end(); ++it) {
+        values v = vec(*it);
+        numeral w = get_weight(v, ineq);
+        if (w.is_pos()) {
+            ++num_pos;
+        }
+        else if (w.is_neg()) {
+            ++num_neg;
+        }
+    }
+    return num_pos * num_neg;
+}
+
 void hilbert_basis::recycle(offset_t idx) {
     m_index->remove(idx, vec(idx));
     m_free_list.push_back(idx);
@@ -724,8 +639,8 @@ void hilbert_basis::resolve(offset_t i, offset_t j, offset_t r) {
     for (unsigned k = 0; k < nv; ++k) {
         u[k] = v[k] + w[k];
     }
-    u.value() = v.value() + w.value();
-    // std::cout << "resolve: " << v.value() << " + " << w.value() << " = " << u.value() << "\n";
+    u.weight() = v.weight() + w.weight();
+    // std::cout << "resolve: " << v.weight() << " + " << w.weight() << " = " << u.weight() << "\n";
     TRACE("hilbert_basis_verbose",
           display(tout, i); 
           display(tout, j); 
@@ -738,7 +653,7 @@ hilbert_basis::offset_t hilbert_basis::alloc_vector() {
     if (m_free_list.empty()) {
         unsigned num_vars = get_num_vars();
         unsigned idx =  m_store.size();
-        m_store.resize(idx + 1 + get_num_vars());
+        m_store.resize(idx + 1 + num_vars);
         return offset_t(idx);
     }
     else {
@@ -754,7 +669,7 @@ void hilbert_basis::add_goal(offset_t idx) {
         return;
     }
     m_index->insert(idx, v);
-    if (v.value().is_zero()) {
+    if (v.weight().is_zero()) {
         m_zero.push_back(idx);
     }
     else {
@@ -765,12 +680,7 @@ void hilbert_basis::add_goal(offset_t idx) {
 bool hilbert_basis::is_subsumed(offset_t idx)  {
 
     offset_t found_idx;
-    if (m_index->find(vec(idx), idx, found_idx)) {        
-        TRACE("hilbert_basis",  
-           display(tout, idx);
-           tout << " <= \n";
-           display(tout, found_idx);
-           tout << "\n";);
+    if (m_index->find(idx, vec(idx), found_idx)) {        
         ++m_stats.m_num_subsumptions;
         return true;
     }
@@ -778,13 +688,30 @@ bool hilbert_basis::is_subsumed(offset_t idx)  {
 }
 
 bool hilbert_basis::can_resolve(offset_t i, offset_t j) const {
-    sign_t s1 = get_sign(i);
-    sign_t s2 = get_sign(j);
-    return s1 != s2 && abs(vec(i)[0] + vec(j)[0]) <= numeral(1);
+    if (get_sign(i) == get_sign(j)) {
+        return false;
+    }
+    values const& v1 = vec(i);
+    values const& v2 = vec(j);
+    // index 0 is reserved for the constant coefficient. 
+    // The value of it should either be 0 or 1.
+    if (abs(v1[0] + v2[0]) > numeral(1)) {
+        return false;
+    }
+    for (unsigned i = 0; i < m_ints.size(); ++i) {
+        unsigned j = m_ints[i];
+        if (v1[j].is_pos() && v2[j].is_neg()) {
+            return false;
+        }
+        if (v1[j].is_neg() && v2[j].is_pos()) {
+            return false;
+        }
+    }
+    return true;
 }
 
 hilbert_basis::sign_t hilbert_basis::get_sign(offset_t idx) const {
-    numeral val = vec(idx).value();
+    numeral val = vec(idx).weight();
     if (val.is_pos()) {
         return pos;
     }
@@ -794,20 +721,20 @@ hilbert_basis::sign_t hilbert_basis::get_sign(offset_t idx) const {
     return zero;
 }
 
-void hilbert_basis::set_eval(values& val, num_vector const& ineq) const {
+hilbert_basis::numeral hilbert_basis::get_weight(values& val, num_vector const& ineq) const {
     numeral result(0);
     unsigned num_vars = get_num_vars();
     for (unsigned i = 0; i < num_vars; ++i) {
         result += val[i]*ineq[i];
     }
-    val.value() = result;
+    return result;
 }
 
 void hilbert_basis::display(std::ostream& out) const {
     unsigned nv = get_num_vars();
     out << "inequalities:\n";
     for (unsigned i = 0; i < m_ineqs.size(); ++i) {
-        display_ineq(out, m_ineqs[i]);
+        display_ineq(out, m_ineqs[i], m_iseq[i]);
     }
     if (!m_basis.empty()) {
         out << "basis:\n";
@@ -835,12 +762,11 @@ void hilbert_basis::display(std::ostream& out) const {
             display(out, m_zero[i]);
         }
     }
-
 }
 
 void hilbert_basis::display(std::ostream& out, offset_t o) const {
     display(out, vec(o));
-    out << " -> " << vec(o).value() << "\n";    
+    out << " -> " << vec(o).weight() << "\n";    
 }
 
 void hilbert_basis::display(std::ostream& out, values const& v) const {
@@ -850,7 +776,7 @@ void hilbert_basis::display(std::ostream& out, values const& v) const {
     }
 }
 
-void hilbert_basis::display_ineq(std::ostream& out, num_vector const& v) const {
+void hilbert_basis::display_ineq(std::ostream& out, num_vector const& v, bool is_eq) const {
     unsigned nv = get_num_vars();
     for (unsigned j = 0; j < nv; ++j) {
         if (!v[j].is_zero()) {
@@ -871,7 +797,12 @@ void hilbert_basis::display_ineq(std::ostream& out, num_vector const& v) const {
             out << "x" << j;
         }
     }
-    out << " >= 0\n";
+    if (is_eq) {
+        out << " = 0\n";
+    }
+    else {
+        out << " >= 0\n";
+    }
 }
 
 
@@ -886,3 +817,71 @@ void hilbert_isl_basis::add_le(num_vector const& v, numeral bound) {
     }
     m_basis.add_le(w);
 }
+
+
+/**
+   Vector v is subsumed by vector w if
+       
+       v[i] >= w[i] for each index i.
+       
+       a*v >= a*w  for the evaluation of vectors with respect to a.
+       
+       . a*v < 0 => a*v = a*w
+       . a*v > 0 => a*w > 0
+       . a*v = 0 => a*w = 0
+
+   Justification:
+       
+       let u := v - w, then
+       
+       u[i] >= 0  for each index i
+       
+       a*u = a*(v-w) >= 0
+       
+       So v = u + w, where a*u >= 0, a*w >= 0.
+       
+       If a*v >= a*w >= 0 then v and w are linear 
+       solutions of e_i, and also v-w is a solution.
+
+       If a*v = a*w < 0, then a*(v-w) = 0, so v can be obtained from w + (v - w).
+       
+*/
+
+bool hilbert_basis::is_subsumed(offset_t i, offset_t j) const {
+    values v = vec(i);
+    values w = vec(j);
+    numeral const& n = v.weight();
+    numeral const& m = w.weight();
+    bool r = 
+        i.m_offset != j.m_offset &&         
+        n >= m && (!m.is_nonpos() || n == m) &&
+        is_geq(v, w);
+    for (unsigned k = 0; r && k < m_current_ineq; ++k) {
+        r = get_weight(vec(i), m_ineqs[k]) >= get_weight(vec(j), m_ineqs[k]);
+    }
+    CTRACE("hilbert_basis", r, 
+           display(tout, i);
+           tout << " <= \n";
+           display(tout, j);
+           tout << "\n";);
+    return r;
+}
+
+bool hilbert_basis::is_geq(values const& v, values const& w) const {
+    unsigned nv = get_num_vars();
+    for (unsigned i = 0; i < nv; ++i) {
+        if (!is_abs_geq(v[i], w[i])) {
+            return false;
+        }
+    }
+    return true;
+}
+
+bool hilbert_basis::is_abs_geq(numeral const& v, numeral const& w) const {
+    if (w.is_neg()) {
+        return v <= w;
+    }
+    else {
+        return v >= w;
+    }
+}
diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h
index 4e3b76542..be136fbf9 100644
--- a/src/muz_qe/hilbert_basis.h
+++ b/src/muz_qe/hilbert_basis.h
@@ -34,11 +34,9 @@ public:
     typedef rational numeral;
     typedef vector<numeral> num_vector;
 private:
-    class rational_heap;
     class value_index;
     class index;
     class passive;
-    class weight_map;
     struct offset_t { 
         unsigned m_offset; 
         offset_t(unsigned o) : m_offset(o) {} 
@@ -59,25 +57,28 @@ private:
         numeral* m_values;
     public:
         values(numeral* v):m_values(v) {}
-        numeral& value() { return m_values[0]; } // value of a*x 
+        numeral& weight() { return m_values[0]; } // value of a*x 
         numeral& operator[](unsigned i) { return m_values[i+1]; } // value of x_i
-        numeral const& value() const { return m_values[0]; } // value of a*x 
+        numeral const& weight() const { return m_values[0]; } // value of a*x 
         numeral const& operator[](unsigned i) const { return m_values[i+1]; } // value of x_i
     };
 
-    vector<num_vector> m_ineqs;
-    num_vector         m_store;
-    svector<offset_t>  m_basis;
-    svector<offset_t>  m_free_list;
-    svector<offset_t>  m_active;
-    svector<offset_t>  m_zero;
-    volatile bool      m_cancel;
+    vector<num_vector> m_ineqs;      // set of asserted inequalities
+    svector<bool>      m_iseq;       // inequalities that are equalities
+    num_vector         m_store;      // store of vectors
+    svector<offset_t>  m_basis;      // vector of current basis
+    svector<offset_t>  m_free_list;  // free list of unused storage
+    svector<offset_t>  m_active;     // active set
+    svector<offset_t>  m_zero;       // zeros
+    passive*           m_passive;    // passive set
+    volatile bool      m_cancel;     
     stats              m_stats;
-    index*             m_index;
-    passive*           m_passive;
+    index*             m_index;      // index of generated vectors
+    unsigned_vector    m_ints;       // indices that can be both positive and negative
+    unsigned           m_current_ineq;
     class iterator {
         hilbert_basis const& hb;
-        unsigned   m_idx;
+        unsigned             m_idx;
     public:
         iterator(hilbert_basis const& hb, unsigned idx): hb(hb), m_idx(idx) {}
         offset_t operator*() const { return hb.m_basis[m_idx]; }
@@ -89,10 +90,17 @@ private:
 
     static offset_t mk_invalid_offset();
     static bool     is_invalid_offset(offset_t offs);
-    lbool saturate(num_vector const& ineq);
+    lbool saturate(num_vector const& ineq, bool is_eq);
     void init_basis();
+    void select_inequality();
+    unsigned get_num_nonzeros(num_vector const& ineq);
+    unsigned get_ineq_product(num_vector const& ineq);
+
+    void add_unit_vector(unsigned i, numeral const& e);
     unsigned get_num_vars() const;
-    void set_eval(values& val, num_vector const& ineq) const;
+    numeral get_weight(values& val, num_vector const& ineq) const;
+    bool is_geq(values const& v, values const& w) const;
+    bool is_abs_geq(numeral const& v, numeral const& w) const;
     bool is_subsumed(offset_t idx);
     bool is_subsumed(offset_t i, offset_t j) const;
     void recycle(offset_t idx);
@@ -108,7 +116,7 @@ private:
     
     void display(std::ostream& out, offset_t o) const;
     void display(std::ostream& out, values const & v) const;
-    void display_ineq(std::ostream& out, num_vector const& v) const;
+    void display_ineq(std::ostream& out, num_vector const& v, bool is_eq) const;
 
 public:
         
@@ -131,6 +139,8 @@ public:
     void add_le(num_vector const& v, numeral const& b);
     void add_eq(num_vector const& v, numeral const& b);
 
+    void set_is_int(unsigned var_index);
+
     lbool saturate();
 
     void set_cancel(bool f) { m_cancel = f; }
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index 86b0f1bad..4d401c4c2 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -74,6 +74,14 @@ static void gorrila_test(unsigned seed, unsigned n, unsigned k, unsigned bound,
     saturate_basis(hb);
 }
 
+static vector<rational> vec(int i, int j) {
+    vector<rational> nv;
+    nv.resize(2);
+    nv[0] = rational(i);
+    nv[1] = rational(j);
+    return nv;
+}
+
 static vector<rational> vec(int i, int j, int k) {
     vector<rational> nv;
     nv.resize(3);
@@ -243,25 +251,37 @@ static void tst11() {
     saturate_basis(hb);
 }
 
+static void tst12() {
+    hilbert_basis hb;
+    hb.add_le(vec(1, 0), R(1));
+    hb.add_le(vec(0, 1), R(1));
+    saturate_basis(hb);
+}
+
 void tst_hilbert_basis() {
     std::cout << "hilbert basis test\n";
-#if 0
-    tst1();
-    tst2();
-    tst3();
-    tst4();
-    tst5();
-    tst6();
-    tst7();
-    tst8();
-    tst9();
-    tst10();
-    tst11();
-    gorrila_test(0, 4, 3, 20, 5);
-    gorrila_test(1, 4, 3, 20, 5);
-    gorrila_test(2, 4, 3, 20, 5);
-    gorrila_test(0, 4, 2, 20, 5);
-    gorrila_test(0, 4, 2, 20, 5);
-#endif
-    gorrila_test(0, 10, 7, 20, 11);
+    tst12();
+    return;
+
+    if (true) {
+        tst1();
+        tst2();
+        tst3();
+        tst4();
+        tst5();
+        tst6();
+        tst7();
+        tst8();
+        tst9();
+        tst10();
+        tst11();
+        gorrila_test(0, 4, 3, 20, 5);
+        gorrila_test(1, 4, 3, 20, 5);
+        gorrila_test(2, 4, 3, 20, 5);
+        gorrila_test(0, 4, 2, 20, 5);
+        gorrila_test(0, 4, 2, 20, 5);
+    }
+    else {
+        gorrila_test(0, 10, 7, 20, 11);
+    }
 }