13 files changed, 558 insertions, 575 deletions

diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index e636f2b87..bb1ee5ad2 100644
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -1,5 +1,6 @@
 /*******************************************************************************************[Alg.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
@@ -17,22 +18,20 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "cvc4_private.h"
+#ifndef Minisat_Alg_h
+#define Minisat_Alg_h
 
-#ifndef CVC4_MiniSat_Alg_h
-#define CVC4_MiniSat_Alg_h
+#include "mtl/Vec.h"
 
-#include <cassert>
-
-namespace CVC4 {
-namespace prop {
-namespace minisat {
+namespace Minisat {
 
 //=================================================================================================
-// Useful functions on vectors
+// Useful functions on vector-like types:
 
+//=================================================================================================
+// Removing and searching for elements:
+//
 
-#if 1
 template<class V, class T>
 static inline void remove(V& ts, const T& t)
 {
@@ -42,17 +41,7 @@ static inline void remove(V& ts, const T& t)
     for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
     ts.pop();
 }
-#else
-template<class V, class T>
-static inline void remove(V& ts, const T& t)
-{
-    int j = 0;
-    for (; j < ts.size() && ts[j] != t; j++);
-    assert(j < ts.size());
-    ts[j] = ts.last();
-    ts.pop();
-}
-#endif
+
 
 template<class V, class T>
 static inline bool find(V& ts, const T& t)
@@ -62,8 +51,34 @@ static inline bool find(V& ts, const T& t)
     return j < ts.size();
 }
 
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
 
-#endif /* CVC4_MiniSat_Alg_h */
+//=================================================================================================
+// Copying vectors with support for nested vector types:
+//
+
+// Base case:
+template<class T>
+static inline void copy(const T& from, T& to)
+{
+    to = from;
+}
+
+// Recursive case:
+template<class T>
+static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
+{
+    if (!append)
+        to.clear();
+    for (int i = 0; i < from.size(); i++){
+        to.push();
+        copy(from[i], to.last());
+    }
+}
+
+template<class T>
+static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
new file mode 100644
index 000000000..76322b8b6
--- /dev/null
+++ b/src/prop/minisat/mtl/Alloc.h
@@ -0,0 +1,131 @@
+/*****************************************************************************************[Alloc.h]
+Copyright (c) 2008-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+
+#ifndef Minisat_Alloc_h
+#define Minisat_Alloc_h
+
+#include "mtl/XAlloc.h"
+#include "mtl/Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple Region-based memory allocator:
+
+template<class T>
+class RegionAllocator
+{
+    T*        memory;
+    uint32_t  sz;
+    uint32_t  cap;
+    uint32_t  wasted_;
+
+    void capacity(uint32_t min_cap);
+
+ public:
+    // TODO: make this a class for better type-checking?
+    typedef uint32_t Ref;
+    enum { Ref_Undef = UINT32_MAX };
+    enum { Unit_Size = sizeof(uint32_t) };
+
+    explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }
+    ~RegionAllocator()
+    {
+        if (memory != NULL)
+            ::free(memory);
+    }
+
+
+    uint32_t size      () const      { return sz; }
+    uint32_t wasted    () const      { return wasted_; }
+
+    Ref      alloc     (int size); 
+    void     free      (int size)    { wasted_ += size; }
+
+    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+    T&       operator[](Ref r)       { assert(r >= 0 && r < sz); return memory[r]; }
+    const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; }
+
+    T*       lea       (Ref r)       { assert(r >= 0 && r < sz); return &memory[r]; }
+    const T* lea       (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; }
+    Ref      ael       (const T* t)  { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
+        return  (Ref)(t - &memory[0]); }
+
+    void     moveTo(RegionAllocator& to) {
+        if (to.memory != NULL) ::free(to.memory);
+        to.memory = memory;
+        to.sz = sz;
+        to.cap = cap;
+        to.wasted_ = wasted_;
+
+        memory = NULL;
+        sz = cap = wasted_ = 0;
+    }
+
+
+};
+
+template<class T>
+void RegionAllocator<T>::capacity(uint32_t min_cap)
+{
+    if (cap >= min_cap) return;
+
+    uint32_t prev_cap = cap;
+    while (cap < min_cap){
+        // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the
+        // result even by clearing the least significant bit. The resulting sequence of capacities
+        // is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when
+        // using 'uint32_t' as indices so that as much as possible of this space can be used.
+        uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
+        cap += delta;
+
+        if (cap <= prev_cap)
+            throw OutOfMemoryException();
+    }
+    // printf(" .. (%p) cap = %u\n", this, cap);
+
+    assert(cap > 0);
+    memory = (T*)xrealloc(memory, sizeof(T)*cap);
+}
+
+
+template<class T>
+typename RegionAllocator<T>::Ref
+RegionAllocator<T>::alloc(int size)
+{ 
+    // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
+    assert(size > 0);
+    capacity(sz + size);
+
+    uint32_t prev_sz = sz;
+    sz += size;
+    
+    // Handle overflow:
+    if (sz < prev_sz)
+        throw OutOfMemoryException();
+
+    return prev_sz;
+}
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h
deleted file mode 100644
index cb6a7cbd8..000000000
--- a/src/prop/minisat/mtl/BasicHeap.h
+++ /dev/null
@@ -1,109 +0,0 @@
-/******************************************************************************************[Heap.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4_MiniSat_BasicHeap_h
-#define CVC4_MiniSat_BasicHeap_h
-
-#include "Vec.h"
-
-namespace CVC4 {
-namespace prop {
-namespace minisat {
-
-//=================================================================================================
-// A heap implementation with support for decrease/increase key.
-
-
-template<class Comp>
-class BasicHeap {
-    Comp     lt;
-    vec<int> heap;     // heap of ints
-
-    // Index "traversal" functions
-    static inline int left  (int i) { return i*2+1; }
-    static inline int right (int i) { return (i+1)*2; }
-    static inline int parent(int i) { return (i-1) >> 1; }
-
-    inline void percolateUp(int i)
-    {
-        int x = heap[i];
-        while (i != 0 && lt(x, heap[parent(i)])){
-            heap[i]          = heap[parent(i)];
-            i                = parent(i);
-        }
-        heap   [i] = x;
-    }
-
-
-    inline void percolateDown(int i)
-    {
-        int x = heap[i];
-        while (left(i) < heap.size()){
-            int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
-            if (!lt(heap[child], x)) break;
-            heap[i]          = heap[child];
-            i                = child;
-        }
-        heap[i] = x;
-    }
-
-
-    bool heapProperty(int i) {
-        return i >= heap.size()
-            || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
-
-
-  public:
-    BasicHeap(const C& c) : comp(c) { }
-
-    int  size      ()                     const { return heap.size(); }
-    bool empty     ()                     const { return heap.size() == 0; }
-    int  operator[](int index)            const { return heap[index+1]; }
-    void clear     (bool dealloc = false)       { heap.clear(dealloc); }
-    void insert    (int n)                      { heap.push(n); percolateUp(heap.size()-1); }
-
-
-    int  removeMin() {
-        int r   = heap[0];
-        heap[0] = heap.last();
-        heap.pop();
-        if (heap.size() > 1) percolateDown(0);
-        return r; 
-    }
-
-
-    // DEBUG: consistency checking
-    bool heapProperty() {
-        return heapProperty(1); }
-
-
-    // COMPAT: should be removed
-    int  getmin    ()      { return removeMin(); }
-};
-
-
-//=================================================================================================
-
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4_MiniSat_BasicHeap_h */
diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h
deleted file mode 100644
index 7cf5ba14f..000000000
--- a/src/prop/minisat/mtl/BoxedVec.h
+++ /dev/null
@@ -1,156 +0,0 @@
-/*******************************************************************************************[Vec.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
-
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4_MiniSat_BoxedVec_h
-#define CVC4_MiniSat_BoxedVec_h
-
-#include <cstdlib>
-#include <cassert>
-#include <new>
-
-namespace CVC4 {
-namespace prop {
-namespace minisat {
-
-//=================================================================================================
-// Automatically resizable arrays
-//
-// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
-
-template<class T>
-class bvec {
-
-    static inline int imin(int x, int y) {
-        int mask = (x-y) >> (sizeof(int)*8-1);
-        return (x&mask) + (y&(~mask)); }
-
-    static inline int imax(int x, int y) {
-        int mask = (y-x) >> (sizeof(int)*8-1);
-        return (x&mask) + (y&(~mask)); }
-
-    struct Vec_t {
-        int sz;
-        int cap;
-        T   data[0];
-
-        static Vec_t* alloc(Vec_t* x, int size){
-            x = (Vec_t*)realloc((void*)x, sizeof(Vec_t) + sizeof(T)*size);
-            x->cap = size;
-            return x;
-        }
-
-    };
-
-    Vec_t* ref;
-
-    static const int init_size = 2;
-    static int   nextSize (int current) { return (current * 3 + 1) >> 1; }
-    static int   fitSize  (int needed)  { int x; for (x = init_size; needed > x; x = nextSize(x)); return x; }
-
-    void fill (int size) {
-        assert(ref != NULL);
-        for (T* i = ref->data; i < ref->data + size; i++)
-            new (i) T();
-    }
-
-    void fill (int size, const T& pad) {
-        assert(ref != NULL);
-        for (T* i = ref->data; i < ref->data + size; i++)
-            new (i) T(pad);
-    }
-
-    // Don't allow copying (error prone):
-    altvec<T>&  operator = (altvec<T>& other) { assert(0); }
-    altvec (altvec<T>& other)                  { assert(0); }
-
-public:
-    void     clear  (bool dealloc = false) {
-        if (ref != NULL){
-            for (int i = 0; i < ref->sz; i++)
-                (*ref).data[i].~T();
-
-            if (dealloc) {
-                free(ref); ref = NULL;
-            }else
-                ref->sz = 0;
-        }
-    }
-
-    // Constructors:
-    altvec(void)                   : ref (NULL) { }
-    altvec(int size)               : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size);      ref->sz = size; }
-    altvec(int size, const T& pad) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size, pad); ref->sz = size; }
-   ~altvec(void) { clear(true); }
-
-    // Ownership of underlying array:
-    operator T*       (void)           { return ref->data; }     // (unsafe but convenient)
-    operator const T* (void) const     { return ref->data; }
-
-    // Size operations:
-    int      size   (void) const       { return ref != NULL ? ref->sz : 0; }
-
-    void     pop    (void)             { assert(ref != NULL && ref->sz > 0); int last = --ref->sz; ref->data[last].~T(); }
-    void     push   (const T& elem) {
-        int size = ref != NULL ? ref->sz  : 0;
-        int cap  = ref != NULL ? ref->cap : 0;
-        if (size == cap){
-            cap = cap != 0 ? nextSize(cap) : init_size;
-            ref = Vec_t::alloc(ref, cap);
-        }
-        //new (&ref->data[size]) T(elem);
-        ref->data[size] = elem;
-        ref->sz = size+1;
-    }
-
-    void     push   () {
-        int size = ref != NULL ? ref->sz  : 0;
-        int cap  = ref != NULL ? ref->cap : 0;
-        if (size == cap){
-            cap = cap != 0 ? nextSize(cap) : init_size;
-            ref = Vec_t::alloc(ref, cap);
-        }
-        new (&ref->data[size]) T();
-        ref->sz = size+1;
-    }
-
-    void     shrink (int nelems)             { for (int i = 0; i < nelems; i++) pop(); }
-    void     shrink_(int nelems)             { for (int i = 0; i < nelems; i++) pop(); }
-    void     growTo (int size)               { while (this->size() < size) push(); }
-    void     growTo (int size, const T& pad) { while (this->size() < size) push(pad); }
-    void     capacity (int size)             { growTo(size); }
-
-    const T& last  (void) const              { return ref->data[ref->sz-1]; }
-    T&       last  (void)                    { return ref->data[ref->sz-1]; }
-
-    // Vector interface:
-    const T& operator [] (int index) const  { return ref->data[index]; }
-    T&       operator [] (int index)        { return ref->data[index]; }
-
-    void copyTo(altvec<T>& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); }
-    void moveTo(altvec<T>& dest) { dest.clear(true); dest.ref = ref; ref = NULL; }
-
-};
-
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4_MiniSat_BoxedVec_h */
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index 20d379b1d..226407e77 100644
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -1,5 +1,6 @@
 /******************************************************************************************[Heap.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
@@ -17,17 +18,12 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "cvc4_private.h"
+#ifndef Minisat_Heap_h
+#define Minisat_Heap_h
 
-#ifndef CVC4_MiniSat_Heap_h
-#define CVC4_MiniSat_Heap_h
+#include "mtl/Vec.h"
 
-#include "Vec.h"
-#include <cassert>
-
-namespace CVC4 {
-namespace prop {
-namespace minisat {
+namespace Minisat {
 
 //=================================================================================================
 // A heap implementation with support for decrease/increase key.
@@ -35,9 +31,9 @@ namespace minisat {
 
 template<class Comp>
 class Heap {
-    Comp     lt;
-    vec<int> heap;     // heap of ints
-    vec<int> indices;  // int -> index in heap
+    Comp     lt;       // The heap is a minimum-heap with respect to this comparator
+    vec<int> heap;     // Heap of integers
+    vec<int> indices;  // Each integers position (index) in the Heap
 
     // Index "traversal" functions
     static inline int left  (int i) { return i*2+1; }
@@ -45,20 +41,23 @@ class Heap {
     static inline int parent(int i) { return (i-1) >> 1; }
 
 
-    inline void percolateUp(int i)
+    void percolateUp(int i)
     {
-        int x = heap[i];
-        while (i != 0 && lt(x, heap[parent(i)])){
-            heap[i]          = heap[parent(i)];
-            indices[heap[i]] = i;
-            i                = parent(i);
+        int x  = heap[i];
+        int p  = parent(i);
+        
+        while (i != 0 && lt(x, heap[p])){
+            heap[i]          = heap[p];
+            indices[heap[p]] = i;
+            i                = p;
+            p                = parent(p);
         }
         heap   [i] = x;
         indices[x] = i;
     }
 
 
-    inline void percolateDown(int i)
+    void percolateDown(int i)
     {
         int x = heap[i];
         while (left(i) < heap.size()){
@@ -73,11 +72,6 @@ class Heap {
     }
 
 
-    bool heapProperty (int i) const {
-        return i >= heap.size()
-            || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
-
-
   public:
     Heap(const Comp& c) : lt(c) { }
 
@@ -86,10 +80,20 @@ class Heap {
     bool inHeap    (int n)     const { return n < indices.size() && indices[n] >= 0; }
     int  operator[](int index) const { assert(index < heap.size()); return heap[index]; }
 
-    void decrease  (int n) { assert(inHeap(n)); percolateUp(indices[n]); }
 
-    // RENAME WHEN THE DEPRECATED INCREASE IS REMOVED.
-    void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+    void decrease  (int n) { assert(inHeap(n)); percolateUp  (indices[n]); }
+    void increase  (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+
+
+    // Safe variant of insert/decrease/increase:
+    void update(int n)
+    {
+        if (!inHeap(n))
+            insert(n);
+        else {
+            percolateUp(indices[n]);
+            percolateDown(indices[n]); }
+    }
 
 
     void insert(int n)
@@ -99,7 +103,7 @@ class Heap {
 
         indices[n] = heap.size();
         heap.push(n);
-        percolateUp(indices[n]);
+        percolateUp(indices[n]); 
     }
 
 
@@ -111,69 +115,34 @@ class Heap {
         indices[x]       = -1;
         heap.pop();
         if (heap.size() > 1) percolateDown(0);
-        return x;
+        return x; 
     }
 
 
-    void clear(bool dealloc = false)
-    {
+    // Rebuild the heap from scratch, using the elements in 'ns':
+    void build(vec<int>& ns) {
         for (int i = 0; i < heap.size(); i++)
             indices[heap[i]] = -1;
-#ifdef NDEBUG
-        for (int i = 0; i < indices.size(); i++)
-            assert(indices[i] == -1);
-#endif
-        heap.clear(dealloc);
-    }
-
-
-    // Fool proof variant of insert/decrease/increase
-    void update (int n)
-    {
-        if (!inHeap(n))
-            insert(n);
-        else {
-            percolateUp(indices[n]);
-            percolateDown(indices[n]);
-        }
-    }
+        heap.clear();
 
+        for (int i = 0; i < ns.size(); i++){
+            indices[ns[i]] = i;
+            heap.push(ns[i]); }
 
-    // Delete elements from the heap using a given filter function (-object).
-    // *** this could probaly be replaced with a more general "buildHeap(vec<int>&)" method ***
-    template <class F>
-    void filter(const F& filt) {
-        int i,j;
-        for (i = j = 0; i < heap.size(); i++)
-            if (filt(heap[i])){
-                heap[j]          = heap[i];
-                indices[heap[i]] = j++;
-            }else
-                indices[heap[i]] = -1;
-
-        heap.shrink(i - j);
         for (int i = heap.size() / 2 - 1; i >= 0; i--)
             percolateDown(i);
-
-        assert(heapProperty());
     }
 
-
-    // DEBUG: consistency checking
-    bool heapProperty() const {
-        return heapProperty(1); }
-
-
-    // COMPAT: should be removed
-    void setBounds (int n) { }
-    void increase  (int n) { decrease(n); }
-    int  getmin    ()      { return removeMin(); }
-
+    void clear(bool dealloc = false) 
+    { 
+        for (int i = 0; i < heap.size(); i++)
+            indices[heap[i]] = -1;
+        heap.clear(dealloc); 
+    }
 };
 
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
 
 //=================================================================================================
-#endif /* CVC4_MiniSat_Heap_h */
+}
+
+#endif
diff --git a/src/prop/minisat/mtl/IntTypes.h b/src/prop/minisat/mtl/IntTypes.h
new file mode 100644
index 000000000..c48816284
--- /dev/null
+++ b/src/prop/minisat/mtl/IntTypes.h
@@ -0,0 +1,42 @@
+/**************************************************************************************[IntTypes.h]
+Copyright (c) 2009-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_IntTypes_h
+#define Minisat_IntTypes_h
+
+#ifdef __sun
+    // Not sure if there are newer versions that support C99 headers. The
+    // needed features are implemented in the headers below though:
+
+#   include <sys/int_types.h>
+#   include <sys/int_fmtio.h>
+#   include <sys/int_limits.h>
+
+#else
+
+#   include <stdint.h>
+#   include <inttypes.h>
+
+#endif
+
+#include <limits.h>
+
+//=================================================================================================
+
+#endif
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index 715b84da4..8a82d0e28 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -1,5 +1,5 @@
 /*******************************************************************************************[Map.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2006-2010, Niklas Sorensson
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
@@ -17,18 +17,13 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "cvc4_private.h"
+#ifndef Minisat_Map_h
+#define Minisat_Map_h
 
-#ifndef CVC4_MiniSat_Map_h
-#define CVC4_MiniSat_Map_h
+#include "mtl/IntTypes.h"
+#include "mtl/Vec.h"
 
-#include <stdint.h>
-
-#include "Vec.h"
-
-namespace CVC4 {
-namespace prop {
-namespace minisat {
+namespace Minisat {
 
 //=================================================================================================
 // Default hash/equals functions
@@ -40,6 +35,12 @@ template<class K> struct Equal { bool     operator()(const K& k1, const K& k2) c
 template<class K> struct DeepHash  { uint32_t operator()(const K* k)               const { return hash(*k);  } };
 template<class K> struct DeepEqual { bool     operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
 
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
+
 //=================================================================================================
 // Some primes
 //
@@ -53,8 +54,10 @@ static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 1
 
 template<class K, class D, class H = Hash<K>, class E = Equal<K> >
 class Map {
+ public:
     struct Pair { K key; D data; };
 
+ private:
     H          hash;
     E          equals;
 
@@ -66,45 +69,89 @@ class Map {
     Map<K,D,H,E>&  operator = (Map<K,D,H,E>& other) { assert(0); }
                    Map        (Map<K,D,H,E>& other) { assert(0); }
 
+    bool    checkCap(int new_size) const { return new_size > cap; }
+
     int32_t index  (const K& k) const { return hash(k) % cap; }
-    void   _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; }
+    void   _insert (const K& k, const D& d) { 
+        vec<Pair>& ps = table[index(k)];
+        ps.push(); ps.last().key = k; ps.last().data = d; }
+
     void    rehash () {
         const vec<Pair>* old = table;
 
+        int old_cap = cap;
         int newsize = primes[0];
         for (int i = 1; newsize <= cap && i < nprimes; i++)
            newsize = primes[i];
 
         table = new vec<Pair>[newsize];
+        cap   = newsize;
 
-        for (int i = 0; i < cap; i++){
+        for (int i = 0; i < old_cap; i++){
             for (int j = 0; j < old[i].size(); j++){
                 _insert(old[i][j].key, old[i][j].data); }}
 
         delete [] old;
 
-        cap = newsize;
+        // printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);
     }
 
+    
+ public:
 
-    public:
-
-     Map () : table(NULL), cap(0), size(0) {}
-     Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
+    Map () : table(NULL), cap(0), size(0) {}
+    Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}
     ~Map () { delete [] table; }
 
-    void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; }
-    bool peek   (const K& k, D& d) {
+    // PRECONDITION: the key must already exist in the map.
+    const D& operator [] (const K& k) const
+    {
+        assert(size != 0);
+        const D*         res = NULL;
+        const vec<Pair>& ps  = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k))
+                res = &ps[i].data;
+        assert(res != NULL);
+        return *res;
+    }
+
+    // PRECONDITION: the key must already exist in the map.
+    D& operator [] (const K& k)
+    {
+        assert(size != 0);
+        D*         res = NULL;
+        vec<Pair>& ps  = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k))
+                res = &ps[i].data;
+        assert(res != NULL);
+        return *res;
+    }
+
+    // PRECONDITION: the key must *NOT* exist in the map.
+    void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }
+    bool peek   (const K& k, D& d) const {
         if (size == 0) return false;
         const vec<Pair>& ps = table[index(k)];
         for (int i = 0; i < ps.size(); i++)
             if (equals(ps[i].key, k)){
                 d = ps[i].data;
-                return true; }
+                return true; } 
         return false;
     }
 
-    void remove (const K& k) {
+    bool has   (const K& k) const {
+        if (size == 0) return false;
+        const vec<Pair>& ps = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k))
+                return true;
+        return false;
+    }
+
+    // PRECONDITION: the key must exist in the map.
+    void remove(const K& k) {
         assert(table != NULL);
         vec<Pair>& ps = table[index(k)];
         int j = 0;
@@ -112,6 +159,7 @@ class Map {
         assert(j < ps.size());
         ps[j] = ps.last();
         ps.pop();
+        size--;
     }
 
     void clear  () {
@@ -119,10 +167,27 @@ class Map {
         delete [] table;
         table = NULL;
     }
+
+    int  elems() const { return size; }
+    int  bucket_count() const { return cap; }
+
+    // NOTE: the hash and equality objects are not moved by this method:
+    void moveTo(Map& other){
+        delete [] other.table;
+
+        other.table = table;
+        other.cap   = cap;
+        other.size  = size;
+
+        table = NULL;
+        size = cap = 0;
+    }
+
+    // NOTE: given a bit more time, I could make a more C++-style iterator out of this:
+    const vec<Pair>& bucket(int i) const { return table[i]; }
 };
 
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+//=================================================================================================
+}
 
-#endif /* CVC4_MiniSat_Map_h */
+#endif
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index 291a1f2e3..17567d694 100644
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -1,5 +1,6 @@
 /*****************************************************************************************[Queue.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
@@ -17,77 +18,52 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "cvc4_private.h"
+#ifndef Minisat_Queue_h
+#define Minisat_Queue_h
 
-#ifndef CVC4_MiniSat_Queue_h
-#define CVC4_MiniSat_Queue_h
+#include "mtl/Vec.h"
 
-#include "Vec.h"
-
-namespace CVC4 {
-namespace prop {
-namespace minisat {
+namespace Minisat {
 
 //=================================================================================================
 
-
-template <class T>
+template<class T>
 class Queue {
-    vec<T>  elems;
+    vec<T>  buf;
     int     first;
+    int     end;
 
 public:
-    Queue(void) : first(0) { }
-
-    void insert(T x)   { elems.push(x); }
-    T    peek  () const { return elems[first]; }
-    void pop   () { first++; }
-
-    void clear(bool dealloc = false)   { elems.clear(dealloc); first = 0; }
-    int  size(void)    { return elems.size() - first; }
-
-    //bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; }
-
-    const T& operator [] (int index) const  { return elems[first + index]; }
-
+    typedef T Key;
+
+    Queue() : buf(1), first(0), end(0) {}
+
+    void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
+    int  size  () const { return (end >= first) ? end - first : end - first + buf.size(); }
+
+    const T& operator [] (int index) const  { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+    T&       operator [] (int index)        { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+
+    T    peek  () const { assert(first != end); return buf[first]; }
+    void pop   () { assert(first != end); first++; if (first == buf.size()) first = 0; }
+    void insert(T elem) {   // INVARIANT: buf[end] is always unused
+        buf[end++] = elem;
+        if (end == buf.size()) end = 0;
+        if (first == end){  // Resize:
+            vec<T>  tmp((buf.size()*3 + 1) >> 1);
+            //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);
+            int     i = 0;
+            for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j];
+            for (int j = 0    ; j < end       ; j++) tmp[i++] = buf[j];
+            first = 0;
+            end   = buf.size();
+            tmp.moveTo(buf);
+        }
+    }
 };
 
-//template<class T>
-//class Queue {
-//    vec<T>  buf;
-//    int     first;
-//    int     end;
-//
-//public:
-//    typedef T Key;
-//
-//    Queue() : buf(1), first(0), end(0) {}
-//
-//    void clear () { buf.shrinkTo(1); first = end = 0; }
-//    int  size  () { return (end >= first) ? end - first : end - first + buf.size(); }
-//
-//    T    peek  () { assert(first != end); return buf[first]; }
-//    void pop   () { assert(first != end); first++; if (first == buf.size()) first = 0; }
-//    void insert(T elem) {   // INVARIANT: buf[end] is always unused
-//        buf[end++] = elem;
-//        if (end == buf.size()) end = 0;
-//        if (first == end){  // Resize:
-//            vec<T>  tmp((buf.size()*3 + 1) >> 1);
-//            //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);
-//            int     i = 0;
-//            for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j];
-//            for (int j = 0    ; j < end       ; j++) tmp[i++] = buf[j];
-//            first = 0;
-//            end   = buf.size();
-//            tmp.moveTo(buf);
-//        }
-//    }
-//};
 
 //=================================================================================================
+}
 
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4_MiniSat_Queue_h */
+#endif
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index 19e89803b..e9313ef86 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -1,5 +1,6 @@
 /******************************************************************************************[Sort.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
@@ -17,21 +18,17 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "cvc4_private.h"
+#ifndef Minisat_Sort_h
+#define Minisat_Sort_h
 
-#ifndef CVC4_MiniSat_Sort_h
-#define CVC4_MiniSat_Sort_h
-
-#include "Vec.h"
-
-namespace CVC4 {
-namespace prop {
-namespace minisat {
+#include "mtl/Vec.h"
 
 //=================================================================================================
 // Some sorting algorithms for vec's
 
 
+namespace Minisat {
+
 template<class T>
 struct LessThan_default {
     bool operator () (T x, T y) { return x < y; }
@@ -96,9 +93,6 @@ template <class T> void sort(vec<T>& v) {
 
 
 //=================================================================================================
+}
 
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4_MiniSat_Sort_h */
+#endif
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index 364991aa9..9e220852e 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -1,5 +1,6 @@
 /*******************************************************************************************[Vec.h]
-MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
@@ -17,18 +18,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 **************************************************************************************************/
 
-#include "cvc4_private.h"
+#ifndef Minisat_Vec_h
+#define Minisat_Vec_h
 
-#ifndef CVC4_MiniSat_Vec_h
-#define CVC4_MiniSat_Vec_h
-
-#include <cstdlib>
-#include <cassert>
+#include <assert.h>
 #include <new>
 
-namespace CVC4 {
-namespace prop {
-namespace minisat {
+#include "mtl/IntTypes.h"
+#include "mtl/XAlloc.h"
+
+namespace Minisat {
 
 //=================================================================================================
 // Automatically resizable arrays
@@ -41,93 +40,83 @@ class vec {
     int sz;
     int cap;
 
-    void     init(int size, const T& pad);
-    void     grow(int min_cap);
-
     // Don't allow copying (error prone):
     vec<T>&  operator = (vec<T>& other) { assert(0); return *this; }
              vec        (vec<T>& other) { assert(0); }
-
-    static inline int imin(int x, int y) {
-        int mask = (x-y) >> (sizeof(int)*8-1);
-        return (x&mask) + (y&(~mask)); }
-
-    static inline int imax(int x, int y) {
-        int mask = (y-x) >> (sizeof(int)*8-1);
-        return (x&mask) + (y&(~mask)); }
+             
+    // Helpers for calculating next capacity:
+    static inline int  imax   (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
+    //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
+    static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
 
 public:
-    // Types:
-    typedef int Key;
-    typedef T   Datum;
-
     // Constructors:
-    vec(void)                   : data(NULL) , sz(0)   , cap(0)    { }
-    vec(int size)               : data(NULL) , sz(0)   , cap(0)    { growTo(size); }
+    vec()                       : data(NULL) , sz(0)   , cap(0)    { }
+    explicit vec(int size)      : data(NULL) , sz(0)   , cap(0)    { growTo(size); }
     vec(int size, const T& pad) : data(NULL) , sz(0)   , cap(0)    { growTo(size, pad); }
-    vec(T* array, int size)     : data(array), sz(size), cap(size) { }      // (takes ownership of array -- will be deallocated with 'free()')
-   ~vec(void)                                                      { clear(true); }
+   ~vec()                                                          { clear(true); }
 
-    // Ownership of underlying array:
-    T*       release  (void)           { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; }
-    operator T*       (void)           { return data; }     // (unsafe but convenient)
-    operator const T* (void) const     { return data; }
+    // Pointer to first element:
+    operator T*       (void)           { return data; }
 
     // Size operations:
-    int      size   (void) const       { return sz; }
-    void     shrink (int nelems)       { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
-    void     shrink_(int nelems)       { assert(nelems <= sz); sz -= nelems; }
-    void     pop    (void)             { sz--, data[sz].~T(); }
-    void     growTo (int size);
-    void     growTo (int size, const T& pad);
-    void     clear  (bool dealloc = false);
-    void     capacity (int size) { grow(size); }
+    int      size     (void) const     { return sz; }
+    void     shrink   (int nelems)     { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
+    void     shrink_  (int nelems)     { assert(nelems <= sz); sz -= nelems; }
+    int      capacity (void) const     { return cap; }
+    void     capacity (int min_cap);
+    void     growTo   (int size);
+    void     growTo   (int size, const T& pad);
+    void     clear    (bool dealloc = false);
 
     // Stack interface:
-#if 1
-    void     push  (void)              { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; }
-    //void     push  (const T& elem)     { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; }
-    void     push  (const T& elem)     { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; }
+    void     push  (void)              { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
+    void     push  (const T& elem)     { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
     void     push_ (const T& elem)     { assert(sz < cap); data[sz++] = elem; }
-#else
-    void     push  (void)              { if (sz == cap) grow(sz+1); new (&data[sz]) T()    ; sz++; }
-    void     push  (const T& elem)     { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; }
-#endif
+    void     pop   (void)              { assert(sz > 0); sz--, data[sz].~T(); }
+    // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
+    // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
+    // happen given the way capacities are calculated (below). Essentially, all capacities are
+    // even, but INT_MAX is odd.
 
     const T& last  (void) const        { return data[sz-1]; }
     T&       last  (void)              { return data[sz-1]; }
 
     // Vector interface:
-    const T& operator [] (int index) const  { return data[index]; }
-    T&       operator [] (int index)        { return data[index]; }
-
+    const T& operator [] (int index) const { return data[index]; }
+    T&       operator [] (int index)       { return data[index]; }
 
     // Duplicatation (preferred instead):
-    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (&copy[i]) T(data[i]); }
+    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
     void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
 };
 
+
 template<class T>
-void vec<T>::grow(int min_cap) {
-    if (min_cap <= cap) return;
-    if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
-    else          do cap = (cap*3+1) >> 1; while (cap < min_cap);
-    data = (T*)realloc(data, cap * sizeof(T)); }
+void vec<T>::capacity(int min_cap) {
+    if (cap >= min_cap) return;
+    int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
+    if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
+        throw OutOfMemoryException();
+ }
+
 
 template<class T>
 void vec<T>::growTo(int size, const T& pad) {
     if (sz >= size) return;
-    grow(size);
-    for (int i = sz; i < size; i++) new (&data[i]) T(pad);
+    capacity(size);
+    for (int i = sz; i < size; i++) data[i] = pad;
     sz = size; }
 
+
 template<class T>
 void vec<T>::growTo(int size) {
     if (sz >= size) return;
-    grow(size);
+    capacity(size);
     for (int i = sz; i < size; i++) new (&data[i]) T();
     sz = size; }
 
+
 template<class T>
 void vec<T>::clear(bool dealloc) {
     if (data != NULL){
@@ -135,8 +124,7 @@ void vec<T>::clear(bool dealloc) {
         sz = 0;
         if (dealloc) free(data), data = NULL, cap = 0; } }
 
-}/* CVC4::prop::minisat namespace */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+//=================================================================================================
+}
 
-#endif /* CVC4_MiniSat_Vec_h */
+#endif
diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h
new file mode 100644
index 000000000..1da176028
--- /dev/null
+++ b/src/prop/minisat/mtl/XAlloc.h
@@ -0,0 +1,45 @@
+/****************************************************************************************[XAlloc.h]
+Copyright (c) 2009-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+
+#ifndef Minisat_XAlloc_h
+#define Minisat_XAlloc_h
+
+#include <errno.h>
+#include <stdlib.h>
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:
+
+class OutOfMemoryException{};
+static inline void* xrealloc(void *ptr, size_t size)
+{
+    void* mem = realloc(ptr, size);
+    if (mem == NULL && errno == ENOMEM){
+        throw OutOfMemoryException();
+    }else
+        return mem;
+}
+
+//=================================================================================================
+}
+
+#endif
diff --git a/src/prop/minisat/mtl/config.mk b/src/prop/minisat/mtl/config.mk
new file mode 100644
index 000000000..b5c36fc6b
--- /dev/null
+++ b/src/prop/minisat/mtl/config.mk
@@ -0,0 +1,6 @@
+##
+##  This file is for system specific configurations. For instance, on
+##  some systems the path to zlib needs to be added. Example:
+##
+##  CFLAGS += -I/usr/local/include
+##  LFLAGS += -L/usr/local/lib
diff --git a/src/prop/minisat/mtl/template.mk b/src/prop/minisat/mtl/template.mk
index 15f023fb3..3f443fc38 100644
--- a/src/prop/minisat/mtl/template.mk
+++ b/src/prop/minisat/mtl/template.mk
@@ -5,45 +5,53 @@
 ##        "make d"  for a debug version (no optimizations).
 ##        "make"    for the standard version (optimized, but with debug information and assertions active)
 
-CSRCS     ?= $(wildcard *.C)
-CHDRS     ?= $(wildcard *.h)
-COBJS     ?= $(addsuffix .o, $(basename $(CSRCS)))
+PWD        = $(shell pwd)
+EXEC      ?= $(notdir $(PWD))
+
+CSRCS      = $(wildcard $(PWD)/*.cc) 
+DSRCS      = $(foreach dir, $(DEPDIR), $(filter-out $(MROOT)/$(dir)/Main.cc, $(wildcard $(MROOT)/$(dir)/*.cc)))
+CHDRS      = $(wildcard $(PWD)/*.h)
+COBJS      = $(CSRCS:.cc=.o) $(DSRCS:.cc=.o)
 
 PCOBJS     = $(addsuffix p,  $(COBJS))
 DCOBJS     = $(addsuffix d,  $(COBJS))
 RCOBJS     = $(addsuffix r,  $(COBJS))
 
-EXEC      ?= $(notdir $(shell pwd))
-LIB       ?= $(EXEC)
 
 CXX       ?= g++
-CFLAGS    ?= -Wall
+CFLAGS    ?= -Wall -Wno-parentheses
 LFLAGS    ?= -Wall
 
 COPTIMIZE ?= -O3
 
-.PHONY : s p d r rs lib libd clean 
+CFLAGS    += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
+LFLAGS    += -lz
+
+.PHONY : s p d r rs clean 
 
 s:	$(EXEC)
 p:	$(EXEC)_profile
 d:	$(EXEC)_debug
 r:	$(EXEC)_release
 rs:	$(EXEC)_static
-lib:	lib$(LIB).a
-libd:	lib$(LIB)d.a
+
+libs:	lib$(LIB)_standard.a
+libp:	lib$(LIB)_profile.a
+libd:	lib$(LIB)_debug.a
+libr:	lib$(LIB)_release.a
 
 ## Compile options
-%.o:			CFLAGS +=$(COPTIMIZE) -ggdb -D DEBUG
-%.op:			CFLAGS +=$(COPTIMIZE) -pg -ggdb -D NDEBUG
-%.od:			CFLAGS +=-O0 -ggdb -D DEBUG # -D INVARIANTS
-%.or:			CFLAGS +=$(COPTIMIZE) -D NDEBUG
+%.o:			CFLAGS +=$(COPTIMIZE) -g -D DEBUG
+%.op:			CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
+%.od:			CFLAGS +=-O0 -g -D DEBUG
+%.or:			CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
 
 ## Link options
-$(EXEC):		LFLAGS := -ggdb $(LFLAGS)
-$(EXEC)_profile:	LFLAGS := -ggdb -pg $(LFLAGS)
-$(EXEC)_debug:		LFLAGS := -ggdb $(LFLAGS)
-$(EXEC)_release:	LFLAGS := $(LFLAGS)
-$(EXEC)_static:		LFLAGS := --static $(LFLAGS)
+$(EXEC):		LFLAGS += -g
+$(EXEC)_profile:	LFLAGS += -g -pg
+$(EXEC)_debug:		LFLAGS += -g
+#$(EXEC)_release:	LFLAGS += ...
+$(EXEC)_static:		LFLAGS += --static
 
 ## Dependencies
 $(EXEC):		$(COBJS)
@@ -52,39 +60,48 @@ $(EXEC)_debug:		$(DCOBJS)
 $(EXEC)_release:	$(RCOBJS)
 $(EXEC)_static:		$(RCOBJS)
 
-lib$(LIB).a:	$(filter-out Main.or, $(RCOBJS))
-lib$(LIB)d.a:	$(filter-out Main.od, $(DCOBJS))
+lib$(LIB)_standard.a:	$(filter-out */Main.o,  $(COBJS))
+lib$(LIB)_profile.a:	$(filter-out */Main.op, $(PCOBJS))
+lib$(LIB)_debug.a:	$(filter-out */Main.od, $(DCOBJS))
+lib$(LIB)_release.a:	$(filter-out */Main.or, $(RCOBJS))
 
 
 ## Build rule
-%.o %.op %.od %.or:	%.C
-	@echo Compiling: "$@ ( $< )"
+%.o %.op %.od %.or:	%.cc
+	@echo Compiling: $(subst $(MROOT)/,,$@)
 	@$(CXX) $(CFLAGS) -c -o $@ $<
 
 ## Linking rules (standard/profile/debug/release)
 $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
-	@echo Linking: "$@ ( $^ )"
+	@echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
 	@$(CXX) $^ $(LFLAGS) -o $@
 
-## Library rule
-lib$(LIB).a lib$(LIB)d.a:
-	@echo Library: "$@ ( $^ )"
-	@rm -f $@
-	@ar cq $@ $^
+## Library rules (standard/profile/debug/release)
+lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
+	@echo Making library: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+	@$(AR) -rcsv $@ $^
+
+## Library Soft Link rule:
+libs libp libd libr:
+	@echo "Making Soft Link: $^ -> lib$(LIB).a"
+	@ln -sf $^ lib$(LIB).a
 
 ## Clean rule
 clean:
 	@rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
-	  $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mak lib$(LIB).a lib$(LIB)d.a
+	  $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk 
 
 ## Make dependencies
 depend.mk: $(CSRCS) $(CHDRS)
-	@echo Making dependencies ...
-	@$(CXX) $(CFLAGS) -MM $(CSRCS) > depend.mk
-	@cp depend.mk /tmp/depend.mk.tmp
-	@sed "s/o:/op:/" /tmp/depend.mk.tmp >> depend.mk
-	@sed "s/o:/od:/" /tmp/depend.mk.tmp >> depend.mk
-	@sed "s/o:/or:/" /tmp/depend.mk.tmp >> depend.mk
-	@rm /tmp/depend.mk.tmp
-
+	@echo Making dependencies
+	@$(CXX) $(CFLAGS) -I$(MROOT) \
+	   $(CSRCS) -MM | sed 's|\(.*\):|$(PWD)/\1 $(PWD)/\1r $(PWD)/\1d $(PWD)/\1p:|' > depend.mk
+	@for dir in $(DEPDIR); do \
+	      if [ -r $(MROOT)/$${dir}/depend.mk ]; then \
+		  echo Depends on: $${dir}; \
+		  cat $(MROOT)/$${dir}/depend.mk >> depend.mk; \
+	      fi; \
+	  done
+
+-include $(MROOT)/mtl/config.mk
 -include depend.mk