diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt
index 4ca8cb1d2..dd72f36ee 100644
--- a/src/math/lp/CMakeLists.txt
+++ b/src/math/lp/CMakeLists.txt
@@ -1,7 +1,5 @@
 z3_add_component(lp
   SOURCES
-    binary_heap_priority_queue.cpp
-    binary_heap_upair_queue.cpp
     core_solver_pretty_printer.cpp
     dense_matrix.cpp
     emonics.cpp
diff --git a/src/math/lp/binary_heap_priority_queue.cpp b/src/math/lp/binary_heap_priority_queue.cpp
deleted file mode 100644
index ec6630b1d..000000000
--- a/src/math/lp/binary_heap_priority_queue.cpp
+++ /dev/null
@@ -1,38 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-#include "math/lp/numeric_pair.h"
-#include "math/lp/binary_heap_priority_queue_def.h"
-namespace lp {
-template binary_heap_priority_queue<int>::binary_heap_priority_queue(unsigned int);
-template unsigned binary_heap_priority_queue<int>::dequeue();
-template void binary_heap_priority_queue<int>::enqueue(unsigned int, int const&);
-template void binary_heap_priority_queue<mpq>::enqueue(unsigned int, mpq const&);
-template void binary_heap_priority_queue<int>::remove(unsigned int);
-template unsigned binary_heap_priority_queue<numeric_pair<mpq> >::dequeue();
-template unsigned binary_heap_priority_queue<mpq>::dequeue();
-template void binary_heap_priority_queue<numeric_pair<mpq> >::enqueue(unsigned int, numeric_pair<mpq> const&);
-template void binary_heap_priority_queue<numeric_pair<mpq> >::resize(unsigned int);
-template binary_heap_priority_queue<unsigned int>::binary_heap_priority_queue(unsigned int);
-template void binary_heap_priority_queue<unsigned>::resize(unsigned int);
-template unsigned binary_heap_priority_queue<unsigned int>::dequeue();
-template void binary_heap_priority_queue<unsigned int>::enqueue(unsigned int, unsigned int const&);
-template void binary_heap_priority_queue<unsigned int>::remove(unsigned int);
-template void lp::binary_heap_priority_queue<mpq>::resize(unsigned int);
-}
diff --git a/src/math/lp/binary_heap_priority_queue.h b/src/math/lp/binary_heap_priority_queue.h
deleted file mode 100644
index 1ea8363ef..000000000
--- a/src/math/lp/binary_heap_priority_queue.h
+++ /dev/null
@@ -1,83 +0,0 @@
-
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-#pragma once
-#include "util/vector.h"
-#include "util/debug.h"
-#include "math/lp/lp_utils.h"
-namespace lp {
-// the elements with the smallest priority are dequeued first
-template <typename T>
-class binary_heap_priority_queue {
-    vector<T> m_priorities;
-
-    // indexing for A starts from 1
-    vector<unsigned> m_heap; // keeps the elements of the queue
-    vector<int> m_heap_inverse; // o = m_heap[m_heap_inverse[o]]
-    unsigned m_heap_size;
-    // is is the child place in heap
-    void swap_with_parent(unsigned i);
-    void put_at(unsigned i, unsigned h);
-    void decrease_priority(unsigned o, T newPriority);
-public:
-#ifdef Z3DEBUG
-    bool is_consistent() const;
-#endif
-public:
-    void remove(unsigned o);
-    unsigned size() const { return m_heap_size; }
-    binary_heap_priority_queue(): m_heap(1), m_heap_size(0) {} // the empty constructror
-    // n is the initial queue capacity.
-    // The capacity will be enlarged each time twice if needed
-    binary_heap_priority_queue(unsigned n);
-
-    void clear() {
-        for (unsigned i = 0; i < m_heap_size; i++) {
-            unsigned o = m_heap[i+1];
-            m_heap_inverse[o] = -1;
-        }
-        m_heap_size = 0;
-    }
-
-    void resize(unsigned n);
-    void put_to_heap(unsigned i, unsigned o);
-
-    void enqueue_new(unsigned o, const T& priority);
-
-    // This method can work with an element that is already in the queue.
-    // In this case the priority will be changed and the queue adjusted.
-    void enqueue(unsigned o, const T & priority);
-    void change_priority_for_existing(unsigned o, const T & priority);
-    T get_priority(unsigned o) const { return m_priorities[o]; }
-    bool is_empty() const { return m_heap_size == 0; }
-
-    /// return the first element of the queue and removes it from the queue
-    unsigned dequeue_and_get_priority(T & priority);
-    void fix_heap_under(unsigned i);
-    void put_the_last_at_the_top_and_fix_the_heap();
-    /// return the first element of the queue and removes it from the queue
-    unsigned dequeue();
-    unsigned peek() const {
-        lp_assert(m_heap_size > 0);
-        return m_heap[1];
-    }
-    void print(std::ostream & out);
-};
-}
diff --git a/src/math/lp/binary_heap_priority_queue_def.h b/src/math/lp/binary_heap_priority_queue_def.h
deleted file mode 100644
index 0e640d949..000000000
--- a/src/math/lp/binary_heap_priority_queue_def.h
+++ /dev/null
@@ -1,214 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-#pragma once
-
-#include "util/vector.h"
-#include "math/lp/binary_heap_priority_queue.h"
-namespace lp {
-// "i" is the child's place in the heap
-template <typename T> void binary_heap_priority_queue<T>::swap_with_parent(unsigned i) {
-    unsigned parent = m_heap[i >> 1];
-    put_at(i >> 1, m_heap[i]);
-    put_at(i, parent);
-}
-
-template <typename T> void binary_heap_priority_queue<T>::put_at(unsigned i, unsigned h) {
-    m_heap[i] = h;
-    m_heap_inverse[h] = i;
-}
-
-template <typename T> void binary_heap_priority_queue<T>::decrease_priority(unsigned o, T newPriority) {
-    m_priorities[o] = newPriority;
-    int i = m_heap_inverse[o];
-    while (i > 1) {
-        if (m_priorities[m_heap[i]] < m_priorities[m_heap[i >> 1]])
-            swap_with_parent(i);
-        else
-            break;
-        i >>= 1;
-    }
-}
-
-#ifdef Z3DEBUG
-template <typename T> bool binary_heap_priority_queue<T>::is_consistent() const {
-    for (int i = 0; i < m_heap_inverse.size(); i++) {
-        int i_index = m_heap_inverse[i];
-        lp_assert(i_index <= static_cast<int>(m_heap_size));
-        lp_assert(i_index == -1 || m_heap[i_index] == i);
-    }
-    for (unsigned i = 1; i < m_heap_size; i++) {
-        unsigned ch = i << 1;
-        for (int k = 0; k < 2; k++) {
-            if (ch > m_heap_size) break;
-            if (!(m_priorities[m_heap[i]] <= m_priorities[m_heap[ch]])){
-                return false;
-            }
-            ch++;
-        }
-    }
-    return true;
-}
-#endif
-
-template <typename T> void binary_heap_priority_queue<T>::remove(unsigned o) {
-    T priority_of_o = m_priorities[o];
-    int o_in_heap = m_heap_inverse[o];
-    if (o_in_heap == -1)  {
-        return;  // nothing to do
-    }
-    lp_assert(static_cast<unsigned>(o_in_heap) <= m_heap_size);
-    if (static_cast<unsigned>(o_in_heap) < m_heap_size) {
-        put_at(o_in_heap, m_heap[m_heap_size--]);
-        if (m_priorities[m_heap[o_in_heap]] > priority_of_o) {
-            fix_heap_under(o_in_heap);
-        } else { // we need to propagate the m_heap[o_in_heap] up
-            unsigned i = o_in_heap;
-            while (i > 1) {
-                unsigned ip = i >> 1;
-                if (m_priorities[m_heap[i]] < m_priorities[m_heap[ip]])
-                    swap_with_parent(i);
-                else
-                    break;
-                i = ip;
-            }
-        }
-    } else {
-        lp_assert(static_cast<unsigned>(o_in_heap) == m_heap_size);
-        m_heap_size--;
-    }
-    m_heap_inverse[o] = -1;
-    // lp_assert(is_consistent());
-}
-// n is the initial queue capacity.
-// The capacity will be enlarged two times automatically if needed
-template <typename T> binary_heap_priority_queue<T>::binary_heap_priority_queue(unsigned n) :
-    m_priorities(n),
-    m_heap(n + 1), // because the indexing for A starts from 1
-    m_heap_inverse(n, -1),
-    m_heap_size(0)
-{ }
-
-
-template <typename T> void binary_heap_priority_queue<T>::resize(unsigned n) {
-    m_priorities.resize(n);
-    m_heap.resize(n + 1);
-    m_heap_inverse.resize(n, -1);
-}
-
-template <typename T> void binary_heap_priority_queue<T>::put_to_heap(unsigned i, unsigned o) {
-    m_heap[i] = o;
-    m_heap_inverse[o] = i;
-}
-
-template <typename T> void binary_heap_priority_queue<T>::enqueue_new(unsigned o, const T& priority) {
-    m_heap_size++;
-    int i = m_heap_size;
-    lp_assert(o < m_priorities.size());
-    m_priorities[o] = priority;
-    put_at(i, o);
-    while (i > 1 && m_priorities[m_heap[i >> 1]] > priority) {
-        swap_with_parent(i);
-        i >>= 1;
-    }
-}
-// This method can work with an element that is already in the queue.
-// In this case the priority will be changed and the queue adjusted.
-template <typename T> void binary_heap_priority_queue<T>::enqueue(unsigned o, const T & priority) {
-    if (o >= m_priorities.size()) {
-        if (o == 0)
-            resize(2);
-        else 
-            resize(o << 1); // make the size twice larger
-    }
-    
-    if (m_heap_inverse[o] == -1)
-        enqueue_new(o, priority);
-    else
-        change_priority_for_existing(o, priority);
-}
-
-template <typename T> void binary_heap_priority_queue<T>::change_priority_for_existing(unsigned o, const T & priority) {
-    if (m_priorities[o] > priority) {
-        decrease_priority(o, priority);
-    } else {
-        m_priorities[o] = priority;
-        fix_heap_under(m_heap_inverse[o]);
-    }
-}
-
-
-/// return the first element of the queue and removes it from the queue
-template <typename T> unsigned binary_heap_priority_queue<T>::dequeue_and_get_priority(T & priority) {
-    lp_assert(m_heap_size != 0);
-    int ret = m_heap[1];
-    priority = m_priorities[ret];
-    put_the_last_at_the_top_and_fix_the_heap();
-    return ret;
-}
-
-template <typename T> void binary_heap_priority_queue<T>::fix_heap_under(unsigned i) {
-    while (true) {
-        unsigned smallest = i;
-        unsigned l = i << 1;
-        if (l <= m_heap_size && m_priorities[m_heap[l]] < m_priorities[m_heap[i]])
-            smallest = l;
-        unsigned r = l + 1;
-        if (r <= m_heap_size && m_priorities[m_heap[r]] < m_priorities[m_heap[smallest]])
-            smallest = r;
-        if (smallest != i)
-            swap_with_parent(smallest);
-        else
-            break;
-        i = smallest;
-    }
-}
-
-template <typename T> void binary_heap_priority_queue<T>::put_the_last_at_the_top_and_fix_the_heap() {
-    if (m_heap_size > 1) {
-        put_at(1, m_heap[m_heap_size--]);
-        fix_heap_under(1);
-    } else {
-        m_heap_size--;
-    }
-}
-/// return the first element of the queue and removes it from the queue
-template <typename T> unsigned binary_heap_priority_queue<T>::dequeue() {
-    lp_assert(m_heap_size > 0);
-    int ret = m_heap[1];
-    put_the_last_at_the_top_and_fix_the_heap();
-    m_heap_inverse[ret] = -1;
-    return ret;
-}
-template <typename T> void binary_heap_priority_queue<T>::print(std::ostream & out) {
-    vector<int> index;
-    vector<T> prs;
-    while (size()) {
-        T prior;
-        int j = dequeue_and_get_priority(prior);
-        index.push_back(j);
-        prs.push_back(prior);
-        out << "(" << j << ", " << prior << ")";
-    }
-    out << std::endl;
-    // restore the queue
-    for (int i = 0; i < index.size(); i++)
-        enqueue(index[i], prs[i]);
-}
-}
diff --git a/src/math/lp/binary_heap_upair_queue.cpp b/src/math/lp/binary_heap_upair_queue.cpp
deleted file mode 100644
index f1ff1d639..000000000
--- a/src/math/lp/binary_heap_upair_queue.cpp
+++ /dev/null
@@ -1,32 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-#include "math/lp/binary_heap_upair_queue_def.h"
-namespace lp {
-template binary_heap_upair_queue<int>::binary_heap_upair_queue(unsigned int);
-template binary_heap_upair_queue<unsigned int>::binary_heap_upair_queue(unsigned int);
-template unsigned binary_heap_upair_queue<int>::dequeue_available_spot();
-template unsigned binary_heap_upair_queue<unsigned int>::dequeue_available_spot();
-template void binary_heap_upair_queue<int>::enqueue(unsigned int, unsigned int, int const&);
-template void binary_heap_upair_queue<int>::remove(unsigned int, unsigned int);
-template void binary_heap_upair_queue<unsigned int>::remove(unsigned int, unsigned int);
-template void binary_heap_upair_queue<int>::dequeue(unsigned int&, unsigned int&);
-template void binary_heap_upair_queue<unsigned int>::enqueue(unsigned int, unsigned int, unsigned int const&);
-template void binary_heap_upair_queue<unsigned int>::dequeue(unsigned int&, unsigned int&);
-}
diff --git a/src/math/lp/binary_heap_upair_queue.h b/src/math/lp/binary_heap_upair_queue.h
deleted file mode 100644
index ce4542803..000000000
--- a/src/math/lp/binary_heap_upair_queue.h
+++ /dev/null
@@ -1,65 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-
-#pragma once
-#include <unordered_set>
-#include <unordered_map>
-#include <queue>
-#include "util/vector.h"
-#include <set>
-#include <utility>
-#include "math/lp/binary_heap_priority_queue.h"
-
-
-typedef std::pair<unsigned, unsigned> upair;
-
-namespace lp {
-template <typename  T>
-class binary_heap_upair_queue {
-    binary_heap_priority_queue<T> m_q;
-    std::unordered_map<upair, unsigned> m_pairs_to_index;
-    svector<upair> m_pairs; // inverse to index
-    svector<unsigned> m_available_spots;
-public:
-    binary_heap_upair_queue(unsigned size);
-
-    unsigned dequeue_available_spot();
-    bool is_empty() const { return m_q.is_empty(); }
-
-    unsigned size() const {return m_q.size(); }
-
-    bool contains(unsigned i, unsigned j) const { return m_pairs_to_index.find(std::make_pair(i, j)) != m_pairs_to_index.end();
-    }
-
-    void remove(unsigned i, unsigned j);
-    bool ij_index_is_new(unsigned ij_index) const;
-    void enqueue(unsigned i, unsigned j, const T & priority);
-    void dequeue(unsigned & i, unsigned &j);
-    T get_priority(unsigned i, unsigned j) const;
-#ifdef Z3DEBUG
-    bool pair_to_index_is_a_bijection() const;
-    bool available_spots_are_correct() const;
-    bool is_correct() const {
-        return m_q.is_consistent() && pair_to_index_is_a_bijection() && available_spots_are_correct();
-    }
-#endif
-    void resize(unsigned size) { m_q.resize(size); }
-};
-}
diff --git a/src/math/lp/binary_heap_upair_queue_def.h b/src/math/lp/binary_heap_upair_queue_def.h
deleted file mode 100644
index 65485a6eb..000000000
--- a/src/math/lp/binary_heap_upair_queue_def.h
+++ /dev/null
@@ -1,126 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-#pragma once
-
-#include <set>
-#include "math/lp/lp_utils.h"
-#include "math/lp/binary_heap_upair_queue.h"
-namespace lp {
-template <typename T> binary_heap_upair_queue<T>::binary_heap_upair_queue(unsigned size) : m_q(size), m_pairs(size) {
-    for (unsigned i = 0; i < size; i++)
-        m_available_spots.push_back(i);
-}
-
-template <typename T> unsigned
-binary_heap_upair_queue<T>::dequeue_available_spot() {
-    lp_assert(m_available_spots.empty() == false);
-    unsigned ret = m_available_spots.back();
-    m_available_spots.pop_back();
-    return ret;
-}
-
-template <typename T> void binary_heap_upair_queue<T>::remove(unsigned i, unsigned j) {
-    upair p(i, j);
-    auto it = m_pairs_to_index.find(p);
-    if (it == m_pairs_to_index.end())
-        return; // nothing to do
-    m_q.remove(it->second);
-    m_available_spots.push_back(it->second);
-    m_pairs_to_index.erase(it);
-}
-
-
-template <typename T> bool binary_heap_upair_queue<T>::ij_index_is_new(unsigned ij_index) const {
-    for (auto it : m_pairs_to_index) {
-        if (it.second == ij_index)
-            return false;
-    }
-    return true;
-}
-
-template <typename T> void binary_heap_upair_queue<T>::enqueue(unsigned i, unsigned j, const T & priority) {
-    upair p(i, j);
-    auto it = m_pairs_to_index.find(p);
-    unsigned ij_index;
-    if (it == m_pairs_to_index.end()) {
-        // it is a new pair, let us find a spot for it
-        if (m_available_spots.empty()) {
-            // we ran out of empty spots
-            unsigned size_was = static_cast<unsigned>(m_pairs.size());
-            unsigned new_size = size_was << 1;
-            for (unsigned i = size_was; i < new_size; i++)
-                m_available_spots.push_back(i);
-            m_pairs.resize(new_size);
-        }
-        ij_index = dequeue_available_spot();
-        // lp_assert(ij_index<m_pairs.size() && ij_index_is_new(ij_index));
-        m_pairs[ij_index] = p;
-        m_pairs_to_index[p] = ij_index;
-    } else {
-        ij_index = it->second;
-    }
-    m_q.enqueue(ij_index, priority);
-}
-
-template <typename T> void binary_heap_upair_queue<T>::dequeue(unsigned & i, unsigned &j) {
-    lp_assert(!m_q.is_empty());
-    unsigned ij_index = m_q.dequeue();
-    upair & p = m_pairs[ij_index];
-    i = p.first;
-    j = p.second;
-    m_available_spots.push_back(ij_index);
-    m_pairs_to_index.erase(p);
-}
-
-
-template <typename T> T binary_heap_upair_queue<T>::get_priority(unsigned i, unsigned j) const {
-    auto it =  m_pairs_to_index.find(std::make_pair(i, j));
-    if (it == m_pairs_to_index.end())
-        return T(0xFFFFFF); // big number
-    return m_q.get_priority(it->second);
-}
-
-#ifdef Z3DEBUG
-template <typename T> bool binary_heap_upair_queue<T>::pair_to_index_is_a_bijection() const {
-    std::set<int> tmp;
-    for (auto p : m_pairs_to_index) {
-        unsigned j = p.second;
-        unsigned size = tmp.size();
-        tmp.insert(j);
-        if (tmp.size() == size)
-            return false;
-    }
-    return true;
-}
-
-template <typename T> bool binary_heap_upair_queue<T>::available_spots_are_correct() const {
-    std::set<int> tmp;
-    for (auto p : m_available_spots){
-        tmp.insert(p);
-    }
-    if (tmp.size() != m_available_spots.size())
-        return false;
-    for (auto it : m_pairs_to_index)
-        if (tmp.find(it.second) != tmp.end())
-            return false;
-    return true;
-}
-#endif
-}
diff --git a/src/math/lp/conversion_helper.h b/src/math/lp/conversion_helper.h
deleted file mode 100644
index ba8b6a983..000000000
--- a/src/math/lp/conversion_helper.h
+++ /dev/null
@@ -1,35 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-
-#pragma once
-namespace lp {
-template <typename V>
-struct conversion_helper {
-    static V get_lower_bound(const column_info<mpq> & ci) {
-        return V(ci.get_lower_bound(), ci.lower_bound_is_strict()? 1 : 0);
-    }
-
-    static V get_upper_bound(const column_info<mpq> & ci) {
-        return V(ci.get_upper_bound(), ci.upper_bound_is_strict()? -1 : 0);
-    }
-};
-
-
-}
diff --git a/src/math/lp/indexer_of_constraints.h b/src/math/lp/indexer_of_constraints.h
deleted file mode 100644
index 9bda22bc1..000000000
--- a/src/math/lp/indexer_of_constraints.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-    Nikolaj Bjorner (nbjorner)
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-
-#pragma once
-#include "math/lp/binary_heap_priority_queue.h"
-namespace lp {
-
-class indexer_of_constraints {
-    binary_heap_priority_queue<unsigned> m_queue_of_released_indices;
-    unsigned m_max;
-public:
-    indexer_of_constraints() :m_max(0) {}
-    unsigned get_new_index() {
-        unsigned ret;
-        if (m_queue_of_released_indices.is_empty()) {
-            ret = m_max++;
-        }
-        else {
-            ret = m_queue_of_released_indices.dequeue();
-        }
-        return ret;
-    };
-    void release_index(unsigned i) {
-        m_queue_of_released_indices.enqueue(i, i);
-    };
-    unsigned max() const { return m_max; }
-};
-}
diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
index 966e2f0d7..59929e34f 100644
--- a/src/math/lp/lar_core_solver.h
+++ b/src/math/lp/lar_core_solver.h
@@ -12,7 +12,6 @@ Author:
 #include "math/lp/lp_core_solver_base.h"
 #include <algorithm>
 #include "math/lp/indexed_vector.h"
-#include "math/lp/binary_heap_priority_queue.h"
 #include "math/lp/lp_primal_core_solver.h"
 #include "math/lp/stacked_vector.h"
 #include "math/lp/lar_solution_signature.h"
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index a321632fb..5c77c679a 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -37,7 +37,6 @@
 #include "math/lp/stacked_vector.h"
 #include "math/lp/implied_bound.h"
 #include "math/lp/bound_analyzer_on_row.h"
-#include "math/lp/conversion_helper.h"
 #include "math/lp/int_solver.h"
 #include "math/lp/nra_solver.h"
 #include "math/lp/lp_types.h"
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index 1719f9c55..628777f33 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -32,7 +32,6 @@ Revision History:
 #include "math/lp/static_matrix.h"
 #include "math/lp/core_solver_pretty_printer.h"
 #include "math/lp/lp_core_solver_base.h"
-#include "math/lp/binary_heap_priority_queue.h"
 #include "math/lp/u_set.h"
 namespace lp {
 
diff --git a/src/math/lp/permutation_matrix.cpp b/src/math/lp/permutation_matrix.cpp
index 762b85d63..be4b7335c 100644
--- a/src/math/lp/permutation_matrix.cpp
+++ b/src/math/lp/permutation_matrix.cpp
@@ -24,31 +24,8 @@ Revision History:
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::init(unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq>>::init(unsigned int);
 
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_from_right(vector<lp::mpq>&);
-template bool lp::permutation_matrix<lp::mpq, lp::mpq>::is_identity() const;
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::multiply_by_permutation_from_left(lp::permutation_matrix<lp::mpq, lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::multiply_by_permutation_from_right(lp::permutation_matrix<lp::mpq, lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::multiply_by_permutation_reverse_from_left(lp::permutation_matrix<lp::mpq, lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::multiply_by_reverse_from_right(lp::permutation_matrix<lp::mpq, lp::mpq>&);
 template lp::permutation_matrix<lp::mpq, lp::mpq>::permutation_matrix(unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::transpose_from_left(unsigned int, unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::mpq>::transpose_from_right(unsigned int, unsigned int);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_from_right(vector<lp::mpq>&);
-template bool lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::is_identity() const;
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multiply_by_permutation_from_left(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multiply_by_permutation_from_right(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multiply_by_permutation_reverse_from_left(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::multiply_by_reverse_from_right(lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
 template lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::permutation_matrix(unsigned int);
 template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_from_left(unsigned int, unsigned int);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_from_right(unsigned int, unsigned int);
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_left<lp::mpq>(lp::indexed_vector<lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_left_to_T(vector<lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_right_to_T(vector<lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_left<lp::mpq>(lp::indexed_vector<lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_left_to_T(vector<lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_right_to_T(vector<lp::mpq >&);
-template void  lp::permutation_matrix< lp::mpq, lp::mpq>::apply_reverse_from_left_to_X(vector<lp::mpq> &);
-template void lp::permutation_matrix< lp::mpq, lp::numeric_pair< lp::mpq> >::apply_reverse_from_left_to_X(vector<lp::numeric_pair< lp::mpq>> &);
-template void lp::permutation_matrix<lp::mpq, lp::mpq>::apply_reverse_from_right_to_T(lp::indexed_vector<lp::mpq>&);
-template void lp::permutation_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_reverse_from_right_to_T(lp::indexed_vector<lp::mpq>&);
diff --git a/src/math/lp/permutation_matrix.h b/src/math/lp/permutation_matrix.h
index 35a58906a..a3fff4f7f 100644
--- a/src/math/lp/permutation_matrix.h
+++ b/src/math/lp/permutation_matrix.h
@@ -25,20 +25,16 @@ Revision History:
 #include "math/lp/indexed_vector.h"
 #include "math/lp/lp_settings.h"
 #include "math/lp/matrix.h"
-#include "math/lp/tail_matrix.h"
 namespace lp {
-#ifdef Z3DEBUG
-    inline bool is_even(int k) {  return (k/2)*2 == k; }
-#endif
 
-    template <typename T, typename X>
-class permutation_matrix : public tail_matrix<T, X> {
+template <typename T, typename X>
+class permutation_matrix 
+#ifdef Z3DEBUG
+    : public matrix<T, X>
+#endif 
+{
         vector<unsigned> m_permutation;
         vector<unsigned> m_rev;
-        vector<unsigned> m_work_array;
-        vector<T> m_T_buffer;
-        vector<X> m_X_buffer;
-
 
         class ref {
             permutation_matrix & m_p;
@@ -63,42 +59,15 @@ class permutation_matrix : public tail_matrix<T, X> {
         // create a unit permutation of the given length
         void init(unsigned length);
         unsigned get_rev(unsigned i) { return m_rev[i]; }
-        bool is_dense() const override { return false; }
-#ifdef Z3DEBUG
-        permutation_matrix get_inverse() const {
-            return permutation_matrix(size(), m_rev);
-        }
+
+#ifdef Z3DEBUG        
         void print(std::ostream & out) const;
 #endif
 
         ref operator[](unsigned i) { return ref(*this, i); }
 
         unsigned operator[](unsigned i) const { return m_permutation[i]; }
-
-        void apply_from_left(vector<X> & w, lp_settings &) override;
-
-        void apply_from_left_to_T(indexed_vector<T> & w, lp_settings & settings) override;
-
-        void apply_from_right(vector<T> & w) override;
-
-        void apply_from_right(indexed_vector<T> & w) override;
         
-        template <typename L>
-        void copy_aside(vector<L> & t, vector<unsigned> & tmp_index, indexed_vector<L> & w);
-
-        template <typename L>
-        void clear_data(indexed_vector<L> & w);
-
-        template <typename L>
-        void apply_reverse_from_left(indexed_vector<L> & w);
-
-        void apply_reverse_from_left_to_T(vector<T> & w);
-        void apply_reverse_from_left_to_X(vector<X> & w);
-
-        void apply_reverse_from_right_to_T(vector<T> & w);
-        void apply_reverse_from_right_to_T(indexed_vector<T> & w);
-        void apply_reverse_from_right_to_X(vector<X> & w);
-
         void set_val(unsigned i, unsigned pi) {
             lp_assert(i < size() && pi < size());  m_permutation[i] = pi;  m_rev[pi] = i;  }
 
@@ -116,18 +85,6 @@ class permutation_matrix : public tail_matrix<T, X> {
         void set_number_of_rows(unsigned /*m*/) override { }
         void set_number_of_columns(unsigned /*n*/) override { }
 #endif
-        void multiply_by_permutation_from_left(permutation_matrix<T, X> & p);
-
-        // this is multiplication in the matrix sense
-        void multiply_by_permutation_from_right(permutation_matrix<T, X> & p);
-
-        void multiply_by_reverse_from_right(permutation_matrix<T, X> & q);
-
-        void multiply_by_permutation_reverse_from_left(permutation_matrix<T, X> & r);
-
-        void shrink_by_one_identity();
-
-        bool is_identity() const;
 
         unsigned size() const { return static_cast<unsigned>(m_rev.size()); }
 
@@ -135,8 +92,6 @@ class permutation_matrix : public tail_matrix<T, X> {
             unsigned old_size = m_permutation.size();
             m_permutation.resize(size);
             m_rev.resize(size);
-            m_T_buffer.resize(size);
-            m_X_buffer.resize(size);
             for (unsigned i = old_size; i < size; i++) {
                 m_permutation[i] = m_rev[i] = i;
     }
diff --git a/src/math/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h
index b6f9924ff..c86fef4f4 100644
--- a/src/math/lp/permutation_matrix_def.h
+++ b/src/math/lp/permutation_matrix_def.h
@@ -22,13 +22,13 @@ Revision History:
 #include "util/vector.h"
 #include "math/lp/permutation_matrix.h"
 namespace lp {
-template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length): m_permutation(length), m_rev(length), m_T_buffer(length), m_X_buffer(length)  {
+template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length): m_permutation(length), m_rev(length)  {
     for (unsigned i = 0; i < length; i++) { // do not change the direction of the loop because of the vectorization bug in clang3.3
         m_permutation[i] = m_rev[i] = i;
     }
 }
 
-template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length, vector<unsigned> const & values): m_permutation(length), m_rev(length) , m_T_buffer(length), m_X_buffer(length) {
+template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(unsigned length, vector<unsigned> const & values): m_permutation(length), m_rev(length) {
     for (unsigned i = 0; i < length; i++) {
         set_val(i, values[i]);
     }
@@ -37,8 +37,6 @@ template <typename T, typename X> permutation_matrix<T, X>::permutation_matrix(u
 template <typename T, typename X> void permutation_matrix<T, X>::init(unsigned length) {
     m_permutation.resize(length);
     m_rev.resize(length);
-    m_T_buffer.resize(length);
-    m_X_buffer.resize(length);
     for (unsigned i = 0; i < length; i++) {
         m_permutation[i] = m_rev[i] = i;
     }
@@ -59,211 +57,6 @@ template <typename T, typename X> void permutation_matrix<T, X>::print(std::ostr
 }
 #endif
 
-template <typename T, typename X>
-void permutation_matrix<T, X>::apply_from_left(vector<X> & w, lp_settings & ) {
-#ifdef Z3DEBUG
-    // dense_matrix<L, X> deb(*this);
-    // L * deb_w = clone_vector<L>(w, row_count());
-    // deb.apply_from_left(deb_w);
-#endif
-    lp_assert(m_X_buffer.size() == w.size());
-    unsigned i = size();
-    while (i-- > 0) {
-        m_X_buffer[i] = w[m_permutation[i]];
-    }
-    i = size();
-    while (i-- > 0) {
-        w[i] = m_X_buffer[i];
-    }
-#ifdef Z3DEBUG
-    // lp_assert(vectors_are_equal<L>(deb_w, w, row_count()));
-    // delete [] deb_w;
-#endif
-}
-
-template <typename T, typename X>
-void permutation_matrix<T, X>::apply_from_left_to_T(indexed_vector<T> & w, lp_settings & ) {
-    vector<T> t(w.m_index.size());
-    vector<unsigned> tmp_index(w.m_index.size());
-    copy_aside(t, tmp_index, w); // todo: is it too much copying
-    clear_data(w);
-    // set the new values
-    for (unsigned i = static_cast<unsigned>(t.size()); i > 0;) {
-        i--;
-        unsigned j = m_rev[tmp_index[i]];
-        w[j] = t[i];
-        w.m_index[i] = j;
-    }
-}
-
-template <typename T, typename X> void permutation_matrix<T, X>::apply_from_right(vector<T> & w) {
-#ifdef Z3DEBUG
-    // dense_matrix<T, X> deb(*this);
-    // T * deb_w = clone_vector<T>(w, row_count());
-    // deb.apply_from_right(deb_w);
-#endif
-    lp_assert(m_T_buffer.size() == w.size());
-    for (unsigned i = 0; i < size(); i++) {
-        m_T_buffer[i] = w[m_rev[i]];
-    }
-
-    for (unsigned i = 0; i < size(); i++) {
-        w[i] = m_T_buffer[i];
-    }
-#ifdef Z3DEBUG
-    // lp_assert(vectors_are_equal<T>(deb_w, w, row_count()));
-    // delete [] deb_w;
-#endif
-}
-
-template <typename T, typename X> void permutation_matrix<T, X>::apply_from_right(indexed_vector<T> & w) {
-#ifdef Z3DEBUG
-    vector<T> wcopy(w.m_data);
-    apply_from_right(wcopy);
-#endif
-    vector<T> buffer(w.m_index.size());
-    vector<unsigned> index_copy(w.m_index);
-    for (unsigned i = 0; i < w.m_index.size(); i++) {
-        buffer[i] = w.m_data[w.m_index[i]];
-    }
-    w.clear();
-
-    for (unsigned i = 0; i < index_copy.size(); i++) {
-        unsigned j = index_copy[i];
-        unsigned pj = m_permutation[j];
-        w.set_value(buffer[i], pj);
-    }
-    
-#ifdef Z3DEBUG
-    lp_assert(vectors_are_equal(wcopy, w.m_data));
-#endif
-}
-
-
-template <typename T, typename X> template <typename L>
-void permutation_matrix<T, X>::copy_aside(vector<L> & t, vector<unsigned> & tmp_index, indexed_vector<L> & w) {
-    for (unsigned i = static_cast<unsigned>(t.size()); i > 0;) {
-        i--;
-        unsigned j = w.m_index[i];
-        t[i] = w[j]; // copy aside all non-zeroes
-        tmp_index[i] = j; // and the indices too
-    }
-}
-
-template <typename T, typename X> template <typename L>
-void permutation_matrix<T, X>::clear_data(indexed_vector<L> & w) {
-    // clear old non-zeroes
-    for (unsigned i = static_cast<unsigned>(w.m_index.size()); i > 0;) {
-        i--;
-        unsigned j = w.m_index[i];
-        w[j] = zero_of_type<L>();
-    }
-}
-
-template <typename T, typename X>template <typename L>
-void permutation_matrix<T, X>::apply_reverse_from_left(indexed_vector<L> & w) {
-    // the result will be w = p(-1) * w
-#ifdef Z3DEBUG
-    // dense_matrix<L, X> deb(get_reverse());
-    // L * deb_w = clone_vector<L>(w.m_data, row_count());
-    // deb.apply_from_left(deb_w);
-#endif
-    vector<L> t(w.m_index.size());
-    vector<unsigned> tmp_index(w.m_index.size());
-
-    copy_aside(t, tmp_index, w);
-    clear_data(w);
-
-    // set the new values
-    for (unsigned i = static_cast<unsigned>(t.size()); i > 0;) {
-        i--;
-        unsigned j = m_permutation[tmp_index[i]];
-        w[j] = t[i];
-        w.m_index[i] = j;
-    }
-#ifdef Z3DEBUG
-    // lp_assert(vectors_are_equal<L>(deb_w, w.m_data, row_count()));
-    // delete [] deb_w;
-#endif
-}
-
-template <typename T, typename X>
-void permutation_matrix<T, X>::apply_reverse_from_left_to_T(vector<T> & w) {
-    // the result will be w = p(-1) * w
-    lp_assert(m_T_buffer.size() == w.size());
-    unsigned i = size();
-    while (i-- > 0) {
-        m_T_buffer[m_permutation[i]] = w[i];
-    }
-    i = size();
-    while (i-- > 0) {
-        w[i] = m_T_buffer[i];
-    }
-}
-template <typename T, typename X>
-void permutation_matrix<T, X>::apply_reverse_from_left_to_X(vector<X> & w) {
-    // the result will be w = p(-1) * w
-    lp_assert(m_X_buffer.size() == w.size());
-    unsigned i = size();
-    while (i-- > 0) {
-        m_X_buffer[m_permutation[i]] = w[i];
-    }
-    i = size();
-    while (i-- > 0) {
-        w[i] = m_X_buffer[i];
-    }
-}
-
-template <typename T, typename X>
-void permutation_matrix<T, X>::apply_reverse_from_right_to_T(vector<T> & w) {
-    // the result will be w = w * p(-1)
-    lp_assert(m_T_buffer.size() == w.size());
-    unsigned i = size();
-    while (i-- > 0) {
-        m_T_buffer[i] = w[m_permutation[i]];
-    }
-    i = size();
-    while (i-- > 0) {
-        w[i] = m_T_buffer[i];
-    }
-}
-
-template <typename T, typename X>
-void permutation_matrix<T, X>::apply_reverse_from_right_to_T(indexed_vector<T> & w) {
-    // the result will be w = w * p(-1)
-#ifdef Z3DEBUG
-    // vector<T> wcopy(w.m_data);
-    // apply_reverse_from_right_to_T(wcopy);
-#endif
-    vector<T> tmp;
-    vector<unsigned> tmp_index(w.m_index);
-    for (auto i : w.m_index) {
-        tmp.push_back(w[i]);
-    }
-    w.clear();
-    
-    for (unsigned k = 0; k < tmp_index.size(); k++) {
-        unsigned j = tmp_index[k];
-        w.set_value(tmp[k], m_rev[j]);
-    }
-
-    
-}
-
-
-template <typename T, typename X>
-void permutation_matrix<T, X>::apply_reverse_from_right_to_X(vector<X> & w) {
-    // the result will be w = w * p(-1)
-    lp_assert(m_X_buffer.size() == w.size());
-    unsigned i = size();
-    while (i-- > 0) {
-        m_X_buffer[i] = w[m_permutation[i]];
-    }
-    i = size();
-    while (i-- > 0) {
-        w[i] = m_X_buffer[i];
-    }
-}
 
 template <typename T, typename X> void permutation_matrix<T, X>::transpose_from_left(unsigned i, unsigned j) {
     // the result will be this = (i,j)*this
@@ -283,55 +76,5 @@ template <typename T, typename X> void permutation_matrix<T, X>::transpose_from_
     set_val(j, pi);
 }
 
-template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_permutation_from_left(permutation_matrix<T, X> & p) {
-    m_work_array = m_permutation;
-    lp_assert(p.size() == size());
-    unsigned i = size();
-    while (i-- > 0) {
-        set_val(i, m_work_array[p[i]]); // we have m(P)*m(Q) = m(QP), where m is the matrix of the permutation
-    }
-}
-
-// this is multiplication in the matrix sense
-template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_permutation_from_right(permutation_matrix<T, X> & p) {
-    m_work_array = m_permutation;
-    lp_assert(p.size() == size());
-    unsigned i = size();
-    while (i-- > 0)
-        set_val(i, p[m_work_array[i]]); // we have m(P)*m(Q) = m(QP), where m is the matrix of the permutation
-    
-}
-
-template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_reverse_from_right(permutation_matrix<T, X> & q){ // todo : condensed permutations ?
-    lp_assert(q.size() == size());
-    m_work_array = m_permutation;
-    // the result is this = this*q(-1)
-    unsigned i = size();
-    while (i-- > 0) {
-        set_val(i, q.m_rev[m_work_array[i]]); // we have m(P)*m(Q) = m(QP), where m is the matrix of the permutation
-    }
-}
-
-template <typename T, typename X> void permutation_matrix<T, X>::multiply_by_permutation_reverse_from_left(permutation_matrix<T, X> & r){ // todo : condensed permutations?
-    // the result is this = r(-1)*this
-    m_work_array = m_permutation;
-    // the result is this = this*q(-1)
-    unsigned i = size();
-    while (i-- > 0) {
-        set_val(i, m_work_array[r.m_rev[i]]);
-    }
-}
-
-
-template <typename T, typename X> bool permutation_matrix<T, X>::is_identity() const {
-    unsigned i = size();
-    while (i-- > 0) {
-        if (m_permutation[i] != i) {
-            return false;
-        }
-    }
-    return true;
-}
-
 
 }
diff --git a/src/math/lp/tail_matrix.h b/src/math/lp/tail_matrix.h
deleted file mode 100644
index 9fa1a4a47..000000000
--- a/src/math/lp/tail_matrix.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-
-#pragma once
-#include "util/vector.h"
-#include "math/lp/indexed_vector.h"
-#include "math/lp/matrix.h"
-#include "math/lp/lp_settings.h"
-// These matrices appear at the end of the list
-
-namespace lp {
-template <typename T, typename X>
-class tail_matrix
-#ifdef Z3DEBUG
-    : public matrix<T, X>
-#endif
-{
-public:
-    virtual void apply_from_left_to_T(indexed_vector<T> & w, lp_settings & settings) = 0;
-    virtual void apply_from_left(vector<X> & w, lp_settings & settings) = 0;
-    virtual void apply_from_right(vector<T> & w) = 0;
-    virtual void apply_from_right(indexed_vector<T> & w) = 0;
-    virtual ~tail_matrix() = default;
-    virtual bool is_dense() const = 0;
-    struct ref_row {
-        const tail_matrix & m_A;
-        unsigned m_row;
-        ref_row(const tail_matrix& m, unsigned row): m_A(m), m_row(row) {}
-        T operator[](unsigned j) const { return m_A.get_elem(m_row, j);}
-    };
-    ref_row operator[](unsigned i) const { return ref_row(*this, i);}
-};
-}
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 24aa8767a..446ead415 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -34,13 +34,11 @@
 #include <utility>
 #include "math/lp/lp_utils.h"
 #include "test/lp/smt_reader.h"
-#include "math/lp/binary_heap_priority_queue.h"
 #include "test/lp/argument_parser.h"
 #include "test/lp/test_file_reader.h"
 #include "math/lp/indexed_value.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/numeric_pair.h"
-#include "math/lp/binary_heap_upair_queue.h"
 #include "util/stacked_value.h"
 #include "math/lp/u_set.h"
 #include "util/stopwatch.h"
@@ -458,72 +456,7 @@ void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, uns
 
 
 
-void test_upair_queue() {
-    int n = 10;
-    binary_heap_upair_queue<int> q(2);
-    std::unordered_map<upair, int> m;
-    for (int k = 0; k < 100; k++) {
-        int i = my_random()%n;
-        int j = my_random()%n;
-        q.enqueue(i, j, my_random()%n);
-    }
 
-    q.remove(5, 5);
-
-    while (!q.is_empty()) {
-        unsigned i, j;
-        q.dequeue(i, j);
-    }
-}
-
-void test_binary_priority_queue() {
-    std::cout << "testing binary_heap_priority_queue...";
-    auto q = binary_heap_priority_queue<int>(10);
-    q.enqueue(2, 2);
-    q.enqueue(1, 1);
-    q.enqueue(9, 9);
-    q.enqueue(8, 8);
-    q.enqueue(5, 25);
-    q.enqueue(3, 3);
-    q.enqueue(4, 4);
-    q.enqueue(7, 30);
-    q.enqueue(6, 6);
-    q.enqueue(0, 0);
-    q.enqueue(5, 5);
-    q.enqueue(7, 7);
-
-    for (unsigned i = 0; i < 10; i++) {
-        unsigned de = q.dequeue();
-        lp_assert(i == de);
-        std::cout << de << std::endl;
-    }
-    q.enqueue(2, 2);
-    q.enqueue(1, 1);
-    q.enqueue(9, 9);
-    q.enqueue(8, 8);
-    q.enqueue(5, 5);
-    q.enqueue(3, 3);
-    q.enqueue(4, 4);
-    q.enqueue(7, 2);
-    q.enqueue(0, 1);
-    q.enqueue(6, 6);
-    q.enqueue(7, 7);
-    q.enqueue(33, 1000);
-    q.enqueue(20, 0);
-    q.dequeue();
-    q.remove(33);
-    q.enqueue(0, 0);
-#ifdef Z3DEBUG
-    unsigned t = 0;
-    while (q.size() > 0) {
-        unsigned d =q.dequeue();
-        lp_assert(t++ == d);
-        std::cout << d << std::endl;
-    }
-#endif
-    test_upair_queue();
-    std::cout << " done" << std::endl;
-}
 
 
 int get_random_rows() {