diff --git a/src/basis_factorization/SparseUnsortedList.cpp b/src/basis_factorization/SparseUnsortedList.cpp
index ffb185dc5c..969d5e986c 100644
--- a/src/basis_factorization/SparseUnsortedList.cpp
+++ b/src/basis_factorization/SparseUnsortedList.cpp
@@ -52,6 +52,12 @@ void SparseUnsortedList::initialize( const double *V, unsigned size )
     }
 }
 
+void SparseUnsortedList::initialize( unsigned size )
+{
+    _size = size;
+    _list.clear();
+}
+
 void SparseUnsortedList::clear()
 {
     _list.clear();
diff --git a/src/basis_factorization/SparseUnsortedList.h b/src/basis_factorization/SparseUnsortedList.h
index a215c78c51..e5dd4c2deb 100644
--- a/src/basis_factorization/SparseUnsortedList.h
+++ b/src/basis_factorization/SparseUnsortedList.h
@@ -46,6 +46,7 @@ class SparseUnsortedList
     SparseUnsortedList( unsigned size );
     SparseUnsortedList( const double *V, unsigned size );
     void initialize( const double *V, unsigned size );
+    void initialize( unsigned size );
     void initializeToEmpty();
 
     /*
diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
index 2dce46495d..b071d7e99e 100644
--- a/src/engine/Engine.cpp
+++ b/src/engine/Engine.cpp
@@ -32,7 +32,8 @@
 #include "TimeUtils.h"
 
 Engine::Engine()
-    : _rowBoundTightener( *_tableau )
+    : _work_alloc( 0 )
+    , _rowBoundTightener( *_tableau )
     , _smtCore( this )
     , _numPlConstraintsDisabledByValidSplits( 0 )
     , _preprocessingEnabled( false )
@@ -72,6 +73,7 @@ Engine::~Engine()
     {
         delete[] _work;
         _work = NULL;
+        _work_alloc = 0;
     }
 }
 
@@ -82,15 +84,21 @@ void Engine::setVerbosity( unsigned verbosity )
 
 void Engine::adjustWorkMemorySize()
 {
+    int new_alloc = _tableau->getM();
+
+    if ( _work_alloc >= new_alloc ) return;
+
     if ( _work )
     {
         delete[] _work;
         _work = NULL;
+        _work_alloc = 0;
     }
 
-    _work = new double[_tableau->getM()];
+    _work = new double[new_alloc];
     if ( !_work )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Engine::work" );
+    _work_alloc = new_alloc;
 }
 
 bool Engine::solve( unsigned timeoutInSeconds )
@@ -212,6 +220,12 @@ bool Engine::solve( unsigned timeoutInSeconds )
             {
                 _smtCore.performSplit();
                 splitJustPerformed = true;
+
+                _precisionRestorer.restoreTableau( *this, *_tableau, _smtCore, PrecisionRestorer::RESTORE_BASICS );
+                _basisRestorationRequired = Engine::RESTORATION_NOT_NEEDED;
+                _rowBoundTightener->clear();
+                _constraintBoundTightener->resetBounds();
+
                 continue;
             }
 
@@ -1008,7 +1022,7 @@ void Engine::initializeTableau( const double *constraintMatrix, const List<unsig
     unsigned m = equations.size();
     unsigned n = _preprocessedQuery.getNumberOfVariables();
 
-    _tableau->setDimensions( m, n );
+    _tableau->setDimensions( m, n, m, n );
 
     adjustWorkMemorySize();
 
diff --git a/src/engine/Engine.h b/src/engine/Engine.h
index d97ecff1e9..f9e692a63a 100644
--- a/src/engine/Engine.h
+++ b/src/engine/Engine.h
@@ -179,6 +179,8 @@ class Engine : public IEngine, public SignalHandler::Signalable
         PERFORMED_WEAK_RESTORATION = 2,
     };
 
+    int _work_alloc;
+
 
     /*
       Perform bound tightening operations that require
diff --git a/src/engine/ITableau.h b/src/engine/ITableau.h
index caa07036e9..433fc5126f 100644
--- a/src/engine/ITableau.h
+++ b/src/engine/ITableau.h
@@ -93,7 +93,7 @@ class ITableau
 
     virtual ~ITableau() {};
 
-    virtual void setDimensions( unsigned m, unsigned n ) = 0;
+    virtual void setDimensions( unsigned m, unsigned n, unsigned m_alloc, unsigned n_alloc ) = 0;
     virtual void setConstraintMatrix( const double *A ) = 0;
     virtual void setRightHandSide( const double *b ) = 0;
     virtual void setRightHandSide( unsigned index, double value ) = 0;
diff --git a/src/engine/PrecisionRestorer.cpp b/src/engine/PrecisionRestorer.cpp
index 14be91b34b..91d2c7f97d 100644
--- a/src/engine/PrecisionRestorer.cpp
+++ b/src/engine/PrecisionRestorer.cpp
@@ -65,7 +65,7 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
 
         bool dimensionsRestored = ( tableau.getN() == targetN ) && ( tableau.getM() == targetM );
 
-        ASSERT( dimensionsRestored || GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS );
+        /* ASSERT( dimensionsRestored || GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS ); */
 
         Set<unsigned> currentBasics = tableau.getBasicVariables();
 
@@ -107,7 +107,7 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
 
         // Tighten bounds if needed. The tableau will ignore these bounds if
         // tighter bounds are already known, somehow.
-        for ( unsigned i = 0; i < targetN; ++i )
+        for ( unsigned i = 0; i < tableau.getN(); ++i )
         {
             tableau.tightenLowerBound( i, lowerBounds[i] );
             tableau.tightenUpperBound( i, upperBounds[i] );
@@ -120,7 +120,7 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
         engine.setNumPlConstraintsDisabledByValidSplits
             ( targetEngineState._numPlConstraintsDisabledByValidSplits );
 
-        DEBUG({
+        /* DEBUG({
                 // Same dimensions
                 ASSERT( GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS || tableau.getN() == targetN );
                 ASSERT( GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS || tableau.getM() == targetM );
@@ -140,7 +140,7 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
                         targetEngineState._numPlConstraintsDisabledByValidSplits );
 
                 tableau.verifyInvariants();
-            });
+            });*/
     }
     catch ( ... )
     {
@@ -154,6 +154,133 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
     delete[] upperBounds;
 }
 
+void PrecisionRestorer::restoreTableau( IEngine &engine,
+                                        ITableau &tableau,
+                                        SmtCore &smtCore,
+                                        RestoreBasics restoreBasics )
+{
+    // Store the dimensions, bounds and basic variables in the current tableau, before restoring it
+    unsigned targetM = tableau.getM();
+    unsigned targetN = tableau.getN();
+
+    Set<unsigned> shouldBeBasic = tableau.getBasicVariables();
+
+    double *lowerBounds = new double[targetN];
+    double *upperBounds = new double[targetN];
+    memcpy( lowerBounds, tableau.getLowerBounds(), sizeof(double) * targetN );
+    memcpy( upperBounds, tableau.getUpperBounds(), sizeof(double) * targetN );
+
+    try
+    {
+        EngineState targetEngineState;
+        engine.storeState( targetEngineState, false );
+
+        // Store the case splits performed so far
+        List<PiecewiseLinearCaseSplit> targetSplits;
+        smtCore.allSplitsSoFar( targetSplits );
+
+        // Restore engine and tableau to their original form
+        engine.restoreState( _initialEngineState );
+
+        // At this point, the tableau has the appropriate dimensions. Restore the variable bounds
+        // and basic variables.
+        // Note that if column merging is enabled, the dimensions may not be precisely those before
+        // the resotration, because merging sometimes fails - in which case an equation is added. If
+        // we fail to restore the dimensions, we cannot restore the basics.
+
+        bool dimensionsRestored = ( tableau.getN() == targetN ) && ( tableau.getM() == targetM );
+
+        /* ASSERT( dimensionsRestored || GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS ); */
+
+        Set<unsigned> currentBasics = tableau.getBasicVariables();
+
+        if ( dimensionsRestored && restoreBasics == RESTORE_BASICS )
+        {
+            List<unsigned> shouldBeBasicList;
+            for ( const auto &basic : shouldBeBasic )
+                shouldBeBasicList.append( basic );
+
+            bool failed = false;
+            try
+            {
+                tableau.initializeTableau( shouldBeBasicList );
+            }
+            catch ( MalformedBasisException & )
+            {
+                failed = true;
+            }
+
+            if ( failed )
+            {
+                // The "restoreBasics" set leads to a malformed basis.
+                // Try again without this part of the restoration
+                shouldBeBasicList.clear();
+                for ( const auto &basic : currentBasics )
+                    shouldBeBasicList.append( basic );
+
+                try
+                {
+                    tableau.initializeTableau( shouldBeBasicList );
+                }
+                catch ( MalformedBasisException & )
+                {
+                    throw MarabouError( MarabouError::RESTORATION_FAILED_TO_REFACTORIZE_BASIS,
+                                         "Precision restoration failed - could not refactorize basis after setting basics" );
+                }
+            }
+        }
+
+        // Tighten bounds if needed. The tableau will ignore these bounds if
+        // tighter bounds are already known, somehow.
+        for ( unsigned i = 0; i < tableau.getN(); ++i )
+        {
+            tableau.tightenLowerBound( i, lowerBounds[i] );
+            tableau.tightenUpperBound( i, upperBounds[i] );
+        }
+
+        // Restore constraint status
+        for ( const auto &pair : targetEngineState._plConstraintToState )
+            pair.first->setActiveConstraint( pair.second->isActive() );
+
+        engine.setNumPlConstraintsDisabledByValidSplits
+            ( targetEngineState._numPlConstraintsDisabledByValidSplits );
+
+        /* DEBUG({
+                // Same dimensions
+                ASSERT( GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS || tableau.getN() == targetN );
+                ASSERT( GlobalConfiguration::USE_COLUMN_MERGING_EQUATIONS || tableau.getM() == targetM );
+
+                // Constraints should be in the same state before and after restoration
+                for ( const auto &pair : targetEngineState._plConstraintToState )
+                {
+                    ASSERT( pair.second->isActive() == pair.first->isActive() );
+                    ASSERT( pair.second->phaseFixed() == pair.first->phaseFixed() );
+                    ASSERT( pair.second->constraintObsolete() == pair.first->constraintObsolete() );
+                }
+
+                EngineState currentEngineState;
+                engine.storeState( currentEngineState, false );
+
+                ASSERT( currentEngineState._numPlConstraintsDisabledByValidSplits ==
+                        targetEngineState._numPlConstraintsDisabledByValidSplits );
+
+                tableau.verifyInvariants();
+            });*/
+    }
+    catch ( ... )
+    {
+        delete[] lowerBounds;
+        delete[] upperBounds;
+
+        throw;
+    }
+
+    delete[] lowerBounds;
+    delete[] upperBounds;
+}
+
+
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "
diff --git a/src/engine/PrecisionRestorer.h b/src/engine/PrecisionRestorer.h
index e0e04bc065..883ee0de51 100644
--- a/src/engine/PrecisionRestorer.h
+++ b/src/engine/PrecisionRestorer.h
@@ -35,6 +35,12 @@ class PrecisionRestorer
                            SmtCore &smtCore,
                            RestoreBasics restoreBasics );
 
+    void restoreTableau( IEngine &engine,
+                           ITableau &tableau,
+                           SmtCore &smtCore,
+                           RestoreBasics restoreBasics );
+
+
 private:
     EngineState _initialEngineState;
 };
diff --git a/src/engine/Tableau.cpp b/src/engine/Tableau.cpp
index bea8ac97b1..e6360538ce 100644
--- a/src/engine/Tableau.cpp
+++ b/src/engine/Tableau.cpp
@@ -33,7 +33,9 @@
 
 Tableau::Tableau()
     : _n ( 0 )
+    , _n_alloc( 0 )
     , _m ( 0 )
+    , _m_alloc( 0 )
     , _A( NULL )
     , _sparseColumnsOfA( NULL )
     , _sparseRowsOfA( NULL )
@@ -208,42 +210,44 @@ void Tableau::freeMemoryIfNeeded()
     }
 }
 
-void Tableau::setDimensions( unsigned m, unsigned n )
+void Tableau::setDimensions( unsigned m, unsigned n, unsigned alloc_m, unsigned alloc_n )
 {
     _m = m;
     _n = n;
+    _n_alloc = alloc_n;
+    _m_alloc = alloc_m;
 
     _A = new CSRMatrix();
     if ( !_A )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::A" );
 
-    _sparseColumnsOfA = new SparseUnsortedList *[n];
+    _sparseColumnsOfA = new SparseUnsortedList *[alloc_n];
     if ( !_sparseColumnsOfA )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::sparseColumnsOfA" );
 
-    for ( unsigned i = 0; i < n; ++i )
+    for ( unsigned i = 0; i < alloc_n; ++i )
     {
         _sparseColumnsOfA[i] = new SparseUnsortedList( _m );
         if ( !_sparseColumnsOfA[i] )
             throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::sparseColumnsOfA[i]" );
     }
 
-    _sparseRowsOfA = new SparseUnsortedList *[m];
+    _sparseRowsOfA = new SparseUnsortedList *[alloc_m];
     if ( !_sparseRowsOfA )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::sparseRowOfA" );
 
-    for ( unsigned i = 0; i < m; ++i )
+    for ( unsigned i = 0; i < alloc_m; ++i )
     {
         _sparseRowsOfA[i] = new SparseUnsortedList( _n );
         if ( !_sparseRowsOfA[i] )
             throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::sparseRowOfA[i]" );
     }
 
-    _denseA = new double[m*n];
+    _denseA = new double[_m_alloc*_n_alloc];
     if ( !_denseA )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::denseA" );
 
-    _changeColumn = new double[m];
+    _changeColumn = new double[alloc_m];
     if ( !_changeColumn )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::changeColumn" );
 
@@ -251,23 +255,23 @@ void Tableau::setDimensions( unsigned m, unsigned n )
     if ( !_pivotRow )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::pivotRow" );
 
-    _b = new double[m];
+    _b = new double[alloc_m];
     if ( !_b )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::b" );
 
-    _unitVector = new double[m];
+    _unitVector = new double[alloc_m];
     if ( !_unitVector )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::unitVector" );
 
-    _multipliers = new double[m];
+    _multipliers = new double[alloc_m];
     if ( !_multipliers )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::multipliers" );
 
-    _basicIndexToVariable = new unsigned[m];
+    _basicIndexToVariable = new unsigned[alloc_m];
     if ( !_basicIndexToVariable )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::basicIndexToVariable" );
 
-    _variableToIndex = new unsigned[n];
+    _variableToIndex = new unsigned[alloc_n];
     if ( !_variableToIndex )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::variableToIndex" );
 
@@ -279,21 +283,21 @@ void Tableau::setDimensions( unsigned m, unsigned n )
     if ( !_nonBasicAssignment )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::nonBasicAssignment" );
 
-    _lowerBounds = new double[n];
+    _lowerBounds = new double[alloc_n];
     if ( !_lowerBounds )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::lowerBounds" );
-    std::fill_n( _lowerBounds, n, FloatUtils::negativeInfinity() );
+    std::fill_n( _lowerBounds, alloc_n, FloatUtils::negativeInfinity() );
 
-    _upperBounds = new double[n];
+    _upperBounds = new double[alloc_n];
     if ( !_upperBounds )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::upperBounds" );
-    std::fill_n( _upperBounds, n, FloatUtils::infinity() );
+    std::fill_n( _upperBounds, alloc_n, FloatUtils::infinity() );
 
-    _basicAssignment = new double[m];
+    _basicAssignment = new double[alloc_m];
     if ( !_basicAssignment )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::assignment" );
 
-    _basicStatus = new unsigned[m];
+    _basicStatus = new unsigned[alloc_m];
     if ( !_basicStatus )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::basicStatus" );
 
@@ -302,11 +306,11 @@ void Tableau::setDimensions( unsigned m, unsigned n )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::basisFactorization" );
     _basisFactorization->setStatistics( _statistics );
 
-    _workM = new double[m];
+    _workM = new double[alloc_m];
     if ( !_workM )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::work" );
 
-    _workN = new double[n];
+    _workN = new double[alloc_n];
     if ( !_workN )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::work" );
 
@@ -321,9 +325,9 @@ void Tableau::setConstraintMatrix( const double *A )
     for ( unsigned column = 0; column < _n; ++column )
     {
         for ( unsigned row = 0; row < _m; ++row )
-            _denseA[column*_m + row] = A[row*_n + column];
+            _denseA[column*_m_alloc + row] = A[row*_n + column];
 
-        _sparseColumnsOfA[column]->initialize( _denseA + ( column * _m ), _m );
+        _sparseColumnsOfA[column]->initialize( _denseA + ( column * _m_alloc ), _m );
     }
 
     for ( unsigned row = 0; row < _m; ++row )
@@ -1547,7 +1551,7 @@ const SparseMatrix *Tableau::getSparseA() const
 
 const double *Tableau::getAColumn( unsigned variable ) const
 {
-    return _denseA + ( variable * _m );
+    return _denseA + ( variable * _m_alloc );
 }
 
 void Tableau::getSparseAColumn( unsigned variable, SparseUnsortedList *result ) const
@@ -1587,7 +1591,7 @@ void Tableau::dumpEquations()
 void Tableau::storeState( TableauState &state ) const
 {
     // Set the dimensions
-    state.setDimensions( _m, _n, *this );
+    state.setDimensions( _m, _n, _m_alloc, _n_alloc, *this );
 
     // Store matrix A
     _A->storeIntoOther( state._A );
@@ -1595,7 +1599,7 @@ void Tableau::storeState( TableauState &state ) const
         _sparseColumnsOfA[i]->storeIntoOther( state._sparseColumnsOfA[i] );
     for ( unsigned i = 0; i < _m; ++i )
         _sparseRowsOfA[i]->storeIntoOther( state._sparseRowsOfA[i] );
-    memcpy( state._denseA, _denseA, sizeof(double) * _m * _n );
+    memcpy( state._denseA, _denseA, sizeof(double) * _m_alloc * _n_alloc );
 
     // Store right hand side vector _b
     memcpy( state._b, _b, sizeof(double) * _m );
@@ -1629,16 +1633,33 @@ void Tableau::storeState( TableauState &state ) const
 
 void Tableau::restoreState( const TableauState &state )
 {
-    freeMemoryIfNeeded();
-    setDimensions( state._m, state._n );
+    if ( (state._m_alloc > _m_alloc) || (state._n_alloc > _n_alloc) ) {
+        freeMemoryIfNeeded();
+        setDimensions( state._m, state._n, state._m_alloc, state._n_alloc );
+    } else {
+        _n = state._n;
+        _m = state._m;
+
+        // The only thing needed from freeMemoryIfNeeded and setDimensions
+        _pivotRow->reset();
+
+        if ( _basisFactorization ) delete _basisFactorization;
+        _basisFactorization = BasisFactorizationFactory::createBasisFactorization( _m, *this );
+        if ( !_basisFactorization )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::basisFactorization" );
+        _basisFactorization->setStatistics( _statistics );
+    }
 
     // Restore matrix A
     state._A->storeIntoOther( _A );
     for ( unsigned i = 0; i < _n; ++i )
         state._sparseColumnsOfA[i]->storeIntoOther( _sparseColumnsOfA[i] );
     for ( unsigned i = 0; i < _m; ++i )
-        state._sparseRowsOfA[i]->storeIntoOther( _sparseRowsOfA[i] );
-    memcpy( _denseA, state._denseA, sizeof(double) * _m * _n );
+        state._sparseRowsOfA[i]->storeIntoOther( _sparseRowsOfA[i] ); 
+
+    for ( unsigned column = 0; column < _n; ++column ) {
+        memcpy( _denseA + ( column * _m_alloc ), state._denseA + ( column * state._m_alloc ), sizeof(double) * _m );
+    }
 
     // Restore right hand side vector _b
     memcpy( _b, state._b, sizeof(double) * _m );
@@ -1782,13 +1803,13 @@ unsigned Tableau::addEquation( const Equation &equation )
         _workN[addend._variable] = addend._coefficient;
         _sparseColumnsOfA[addend._variable]->set( _m - 1, addend._coefficient );
         _sparseRowsOfA[_m - 1]->set( addend._variable, addend._coefficient );
-        _denseA[(addend._variable * _m) + _m - 1] = addend._coefficient;
+        _denseA[(addend._variable * _m_alloc) + _m - 1] = addend._coefficient;
     }
 
     _workN[auxVariable] = 1;
     _sparseColumnsOfA[auxVariable]->set( _m - 1, 1 );
     _sparseRowsOfA[_m - 1]->set( auxVariable, 1 );
-    _denseA[(auxVariable * _m) + _m - 1] = 1;
+    _denseA[(auxVariable * _m_alloc) + _m - 1] = 1;
     _A->addLastRow( _workN );
 
     // Invalidate the cost function, so that it is recomputed in the next iteration.
@@ -1891,6 +1912,12 @@ void Tableau::addRow()
     unsigned newM = _m + 1;
     unsigned newN = _n + 1;
 
+    bool n_realloc = newN > _n_alloc;
+    bool m_realloc = newM > _m_alloc;
+
+    unsigned new_n_alloc = n_realloc ? newN : _n_alloc;
+    unsigned new_m_alloc = m_realloc ? newM : _m_alloc;
+
     /*
       This function increases the sizes of the data structures used by
       the tableau to match newM and newN. Notice that newM = _m + 1 and
@@ -1899,130 +1926,174 @@ void Tableau::addRow()
     */
 
     // Allocate a larger _sparseColumnsOfA, keep old ones
-    SparseUnsortedList **newSparseColumnsOfA = new SparseUnsortedList *[newN];
-    if ( !newSparseColumnsOfA )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newSparseColumnsOfA" );
+    if ( n_realloc ) {
+        SparseUnsortedList **newSparseColumnsOfA = new SparseUnsortedList *[newN];
+        if ( !newSparseColumnsOfA )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newSparseColumnsOfA" );
 
-    for ( unsigned i = 0; i < _n; ++i )
-    {
-        newSparseColumnsOfA[i] = _sparseColumnsOfA[i];
-        newSparseColumnsOfA[i]->incrementSize();
-    }
+        for ( unsigned i = 0; i < _n; ++i )
+        {
+            newSparseColumnsOfA[i] = _sparseColumnsOfA[i];
+            newSparseColumnsOfA[i]->incrementSize();
+        }
 
-    newSparseColumnsOfA[newN - 1] = new SparseUnsortedList( newM );
-    if ( !newSparseColumnsOfA[newN - 1] )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newSparseColumnsOfA[newN-1]" );
+        newSparseColumnsOfA[newN - 1] = new SparseUnsortedList( newM );
+        if ( !newSparseColumnsOfA[newN - 1] )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newSparseColumnsOfA[newN-1]" );
 
-    delete[] _sparseColumnsOfA;
-    _sparseColumnsOfA = newSparseColumnsOfA;
+        delete[] _sparseColumnsOfA;
+        _sparseColumnsOfA = newSparseColumnsOfA;
+    } else {
+        for ( unsigned i = 0; i < _n; ++i ) {
+            _sparseColumnsOfA[i]->incrementSize();
+        }
+        _sparseColumnsOfA[newN - 1]->initialize(newM);
+    }
 
     // Allocate a larger _sparseRowsOfA, keep old ones
-    SparseUnsortedList **newSparseRowsOfA = new SparseUnsortedList *[newM];
-    if ( !newSparseRowsOfA )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newSparseRowsOfA" );
+    if ( m_realloc ) {
+        SparseUnsortedList **newSparseRowsOfA = new SparseUnsortedList *[newM];
+        if ( !newSparseRowsOfA )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newSparseRowsOfA" );
 
-    for ( unsigned i = 0; i < _m; ++i )
-    {
-        newSparseRowsOfA[i] = _sparseRowsOfA[i];
-        newSparseRowsOfA[i]->incrementSize();
-    }
+        for ( unsigned i = 0; i < _m; ++i )
+        {
+            newSparseRowsOfA[i] = _sparseRowsOfA[i];
+            newSparseRowsOfA[i]->incrementSize();
+        }
 
-    newSparseRowsOfA[newM - 1] = new SparseUnsortedList( newN );
-    if ( !newSparseRowsOfA[newM - 1] )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newSparseRowsOfA[newN-1]" );
+        newSparseRowsOfA[newM - 1] = new SparseUnsortedList( newN );
+        if ( !newSparseRowsOfA[newM - 1] )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newSparseRowsOfA[newN-1]" );
 
-    delete[] _sparseRowsOfA;
-    _sparseRowsOfA = newSparseRowsOfA;
+        delete[] _sparseRowsOfA;
+        _sparseRowsOfA = newSparseRowsOfA;
+    } else {
+        for ( unsigned i = 0; i < _m; ++ i ) {
+            _sparseRowsOfA[i]->incrementSize();
+        }
+        _sparseRowsOfA[newM - 1]->initialize( newN );
+    }
 
-    // Allocate a larger _denseA, keep old entries
-    double *newDenseA = new double[newM * newN];
-    if ( !newDenseA )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newDenseA" );
+    if ( m_realloc || n_realloc ) {
+        // Allocate a larger _denseA, keep old entries
+        double *newDenseA = new double[new_m_alloc*new_n_alloc];
+        if ( !newDenseA )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newDenseA" );
 
-    for ( unsigned column = 0; column < _n; ++column )
-    {
-        memcpy( newDenseA + ( column * newM ), _denseA + ( column * _m ), sizeof(double) * _m );
-        newDenseA[column*newM + newM - 1] = 0.0;
-    }
-    std::fill_n( newDenseA + ( newN - 1 ) * newM, newM, 0.0 );
+        for ( unsigned column = 0; column < _n; ++column )
+        {
+            memcpy( newDenseA + ( column * new_m_alloc ), _denseA + ( column * _m_alloc ), sizeof(double) * _m );
+            newDenseA[column*new_m_alloc + newM - 1] = 0.0;
+        }
+        std::fill_n( newDenseA + ( newN - 1 ) * new_m_alloc, newM, 0.0 );
 
-    delete[] _denseA;
-    _denseA = newDenseA;
+        delete[] _denseA;
+        _denseA = newDenseA;
+    } else {
+        for ( unsigned column = 0; column < _n; ++column )
+        {
+            _denseA[column*_m_alloc + newM - 1] = 0.0;
+        }
+        std::fill_n( _denseA + ( newN - 1 ) * _m_alloc, newM, 0.0 );
+    }
 
     // Allocate a new changeColumn. Don't need to initialize
-    double *newChangeColumn = new double[newM];
-    if ( !newChangeColumn )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newChangeColumn" );
-    delete[] _changeColumn;
-    _changeColumn = newChangeColumn;
+    if ( m_realloc ) {
+        double *newChangeColumn = new double[newM];
+        if ( !newChangeColumn )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newChangeColumn" );
+        delete[] _changeColumn;
+        _changeColumn = newChangeColumn;
+    }
 
     // Allocate a new b and copy the old values
-    double *newB = new double[newM];
-    if ( !newB )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newB" );
-    std::fill( newB + _m, newB + newM, 0.0 );
-    memcpy( newB, _b, _m * sizeof(double) );
-    delete[] _b;
-    _b = newB;
+    if ( m_realloc ) {
+        double *newB = new double[newM];
+        if ( !newB )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newB" );
+        std::fill( newB + _m, newB + newM, 0.0 );
+        memcpy( newB, _b, _m * sizeof(double) );
+        delete[] _b;
+        _b = newB;
+    } else {
+        std::fill( _b + _m, _b + newM, 0.0 );
+    }
 
     // Allocate a new unit vector. Don't need to initialize
-    double *newUnitVector = new double[newM];
-    if ( !newUnitVector )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newUnitVector" );
-    delete[] _unitVector;
-    _unitVector = newUnitVector;
+    if ( m_realloc ) {
+        double *newUnitVector = new double[newM];
+        if ( !newUnitVector )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newUnitVector" );
+        delete[] _unitVector;
+        _unitVector = newUnitVector;
+    }
 
     // Allocate new multipliers. Don't need to initialize
-    double *newMultipliers = new double[newM];
-    if ( !newMultipliers )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newMultipliers" );
-    delete[] _multipliers;
-    _multipliers = newMultipliers;
+    if ( m_realloc ) {
+        double *newMultipliers = new double[newM];
+        if ( !newMultipliers )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newMultipliers" );
+        delete[] _multipliers;
+        _multipliers = newMultipliers;
+    }
 
     // Allocate new index arrays. Copy old indices, but don't assign indices to new variables yet.
-    unsigned *newBasicIndexToVariable = new unsigned[newM];
-    if ( !newBasicIndexToVariable )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newBasicIndexToVariable" );
-    memcpy( newBasicIndexToVariable, _basicIndexToVariable, _m * sizeof(unsigned) );
-    delete[] _basicIndexToVariable;
-    _basicIndexToVariable = newBasicIndexToVariable;
-
-    unsigned *newVariableToIndex = new unsigned[newN];
-    if ( !newVariableToIndex )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newVariableToIndex" );
-    memcpy( newVariableToIndex, _variableToIndex, _n * sizeof(unsigned) );
-    delete[] _variableToIndex;
-    _variableToIndex = newVariableToIndex;
+    if ( m_realloc ) {
+        unsigned *newBasicIndexToVariable = new unsigned[newM];
+        if ( !newBasicIndexToVariable )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newBasicIndexToVariable" );
+        memcpy( newBasicIndexToVariable, _basicIndexToVariable, _m * sizeof(unsigned) );
+        delete[] _basicIndexToVariable;
+        _basicIndexToVariable = newBasicIndexToVariable;
+    }
+
+    if ( n_realloc ) {
+        unsigned *newVariableToIndex = new unsigned[newN];
+        if ( !newVariableToIndex )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newVariableToIndex" );
+        memcpy( newVariableToIndex, _variableToIndex, _n * sizeof(unsigned) );
+        delete[] _variableToIndex;
+        _variableToIndex = newVariableToIndex;
+    }
 
     // Allocate a new basic assignment vector, copy old values
-    double *newBasicAssignment = new double[newM];
-    if ( !newBasicAssignment )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newAssignment" );
-    memcpy( newBasicAssignment, _basicAssignment, sizeof(double) * _m );
-    delete[] _basicAssignment;
-    _basicAssignment = newBasicAssignment;
-
-    unsigned *newBasicStatus = new unsigned[newM];
-    if ( !newBasicStatus )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newBasicStatus" );
-    memcpy( newBasicStatus, _basicStatus, sizeof(unsigned) * _m );
-    delete[] _basicStatus;
-    _basicStatus = newBasicStatus;
+    if ( m_realloc ) {
+        double *newBasicAssignment = new double[newM];
+        if ( !newBasicAssignment )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newAssignment" );
+        memcpy( newBasicAssignment, _basicAssignment, sizeof(double) * _m );
+        delete[] _basicAssignment;
+        _basicAssignment = newBasicAssignment;
+    }
+
+    if ( m_realloc ) {
+        unsigned *newBasicStatus = new unsigned[newM];
+        if ( !newBasicStatus )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newBasicStatus" );
+        memcpy( newBasicStatus, _basicStatus, sizeof(unsigned) * _m );
+        delete[] _basicStatus;
+        _basicStatus = newBasicStatus;
+    }
 
     // Allocate new lower and upper bound arrays, and copy old values
-    double *newLowerBounds = new double[newN];
-    if ( !newLowerBounds )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newLowerBounds" );
-    memcpy( newLowerBounds, _lowerBounds, _n * sizeof(double) );
-    delete[] _lowerBounds;
-    _lowerBounds = newLowerBounds;
-
-    double *newUpperBounds = new double[newN];
-    if ( !newUpperBounds )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newUpperBounds" );
-    memcpy( newUpperBounds, _upperBounds, _n * sizeof(double) );
-    delete[] _upperBounds;
-    _upperBounds = newUpperBounds;
+    if ( n_realloc ) {
+        double *newLowerBounds = new double[newN];
+        if ( !newLowerBounds )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newLowerBounds" );
+        memcpy( newLowerBounds, _lowerBounds, _n * sizeof(double) );
+        delete[] _lowerBounds;
+        _lowerBounds = newLowerBounds;
+    }
+
+    if ( n_realloc ) {
+        double *newUpperBounds = new double[newN];
+        if ( !newUpperBounds )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newUpperBounds" );
+        memcpy( newUpperBounds, _upperBounds, _n * sizeof(double) );
+        delete[] _upperBounds;
+        _upperBounds = newUpperBounds;
+    }
 
     // Mark the new variable as unbounded
     _lowerBounds[_n] = FloatUtils::negativeInfinity();
@@ -2038,20 +2109,28 @@ void Tableau::addRow()
     _basisFactorization->setStatistics( _statistics );
 
     // Allocate a larger _workM and _workN. Don't need to initialize.
-    double *newWorkM = new double[newM];
-    if ( !newWorkM )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newWorkM" );
-    delete[] _workM;
-    _workM = newWorkM;
-
-    double *newWorkN = new double[newN];
-    if ( !newWorkN )
-        throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newWorkN" );
-    delete[] _workN;
-    _workN = newWorkN;
+    if ( m_realloc ) {
+        double *newWorkM = new double[newM];
+        if ( !newWorkM )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newWorkM" );
+        delete[] _workM;
+        _workM = newWorkM;
+    }
+
+    if ( n_realloc ) {
+        double *newWorkN = new double[newN];
+        if ( !newWorkN )
+            throw MarabouError( MarabouError::ALLOCATION_FAILED, "Tableau::newWorkN" );
+        delete[] _workN;
+        _workN = newWorkN;
+    }
 
     _m = newM;
     _n = newN;
+
+    _m_alloc = new_m_alloc;
+    _n_alloc = new_n_alloc;
+
     _costFunctionManager->initialize();
 
     for ( const auto &watcher : _resizeWatchers )
@@ -2510,8 +2589,8 @@ void Tableau::mergeColumns( unsigned x1, unsigned x2 )
 
     // And the dense ones, too
     for ( unsigned i = 0; i < _m; ++i )
-        _denseA[x1*_m + i] += _denseA[x2*_m + i];
-    std::fill_n( _denseA + x2 * _m, _m, 0 );
+        _denseA[x1*_m_alloc + i] += _denseA[x2*_m_alloc + i];
+    std::fill_n( _denseA + x2 * _m_alloc, _m, 0 );
 
     computeAssignment();
     computeCostFunction();
diff --git a/src/engine/Tableau.h b/src/engine/Tableau.h
index de7e253b1c..bf6d824aa4 100644
--- a/src/engine/Tableau.h
+++ b/src/engine/Tableau.h
@@ -44,7 +44,7 @@ class Tableau : public ITableau, public IBasisFactorization::BasisColumnOracle
       n: total number of variables
       m: number of constraints (rows)
     */
-    void setDimensions( unsigned m, unsigned n );
+    void setDimensions( unsigned m, unsigned n, unsigned alloc_m, unsigned alloc_n );
 
     /*
       Initialize the constraint matrix
@@ -461,8 +461,8 @@ class Tableau : public ITableau, public IBasisFactorization::BasisColumnOracle
     /*
       The dimensions of matrix A
     */
-    unsigned _n;
-    unsigned _m;
+    unsigned _n, _n_alloc;
+    unsigned _m, _m_alloc;
 
     /*
       The constraint matrix A, and a collection of its
diff --git a/src/engine/TableauRow.cpp b/src/engine/TableauRow.cpp
index 5c3fae5874..1084b695e6 100644
--- a/src/engine/TableauRow.cpp
+++ b/src/engine/TableauRow.cpp
@@ -29,6 +29,13 @@ TableauRow::~TableauRow()
     delete[] _row;
 }
 
+void TableauRow::reset() {
+    for (unsigned i = 0; i < _size; ++i) {
+        _row[i]._var = 0;
+        _row[i]._coefficient = 0.0;
+   }
+}
+
 double TableauRow::operator[]( unsigned index ) const
 {
     return _row[index]._coefficient;
diff --git a/src/engine/TableauRow.h b/src/engine/TableauRow.h
index c2d95ec65f..f0e25d8a56 100644
--- a/src/engine/TableauRow.h
+++ b/src/engine/TableauRow.h
@@ -61,6 +61,7 @@ class TableauRow
     double operator[]( unsigned index ) const;
 
     void dump() const;
+    void reset();
 };
 
 #endif // __TableauRow_h__
diff --git a/src/engine/TableauState.cpp b/src/engine/TableauState.cpp
index 47c5d18508..1fcb38bced 100644
--- a/src/engine/TableauState.cpp
+++ b/src/engine/TableauState.cpp
@@ -135,54 +135,56 @@ TableauState::~TableauState()
     }
 }
 
-void TableauState::setDimensions( unsigned m, unsigned n, const IBasisFactorization::BasisColumnOracle &oracle )
+void TableauState::setDimensions( unsigned m, unsigned n, unsigned m_alloc, unsigned n_alloc, const IBasisFactorization::BasisColumnOracle &oracle )
 {
     _m = m;
     _n = n;
+    _m_alloc = m_alloc;
+    _n_alloc = n_alloc;
 
     _A = new CSRMatrix();
     if ( !_A )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::A" );
 
-    _sparseColumnsOfA = new SparseUnsortedList *[n];
+    _sparseColumnsOfA = new SparseUnsortedList *[n_alloc];
     if ( !_sparseColumnsOfA )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::sparseColumnsOfA" );
 
-    for ( unsigned i = 0; i < n; ++i )
+    for ( unsigned i = 0; i < n_alloc; ++i )
     {
         _sparseColumnsOfA[i] = new SparseUnsortedList;
         if ( !_sparseColumnsOfA[i] )
             throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::sparseColumnsOfA[i]" );
     }
 
-    _sparseRowsOfA = new SparseUnsortedList *[m];
+    _sparseRowsOfA = new SparseUnsortedList *[m_alloc];
     if ( !_sparseRowsOfA )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::sparseRowsOfA" );
 
-    for ( unsigned i = 0; i < m; ++i )
+    for ( unsigned i = 0; i < m_alloc; ++i )
     {
         _sparseRowsOfA[i] = new SparseUnsortedList;
         if ( !_sparseRowsOfA[i] )
             throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::sparseRowsOfA[i]" );
     }
 
-    _denseA = new double[m*n];
+    _denseA = new double[m_alloc*n_alloc];
     if ( !_denseA )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::denseA" );
 
-    _b = new double[m];
+    _b = new double[m_alloc];
     if ( !_b )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::b" );
 
-    _lowerBounds = new double[n];
+    _lowerBounds = new double[n_alloc];
     if ( !_lowerBounds )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::lowerBounds" );
 
-    _upperBounds = new double[n];
+    _upperBounds = new double[n_alloc];
     if ( !_upperBounds )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::upperBounds" );
 
-    _basicAssignment = new double[m];
+    _basicAssignment = new double[m_alloc];
     if ( !_basicAssignment )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::assignment" );
 
@@ -190,7 +192,7 @@ void TableauState::setDimensions( unsigned m, unsigned n, const IBasisFactorizat
     if ( !_nonBasicAssignment )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::nonBasicAssignment" );
 
-    _basicIndexToVariable = new unsigned[m];
+    _basicIndexToVariable = new unsigned[m_alloc];
     if ( !_basicIndexToVariable )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::basicIndexToVariable" );
 
@@ -198,7 +200,7 @@ void TableauState::setDimensions( unsigned m, unsigned n, const IBasisFactorizat
     if ( !_nonBasicIndexToVariable )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::nonBasicIndexToVariable" );
 
-    _variableToIndex = new unsigned[n];
+    _variableToIndex = new unsigned[n_alloc];
     if ( !_variableToIndex )
         throw MarabouError( MarabouError::ALLOCATION_FAILED, "TableauState::variableToIndex" );
 
diff --git a/src/engine/TableauState.h b/src/engine/TableauState.h
index a83ff6b6ed..9789573f4a 100644
--- a/src/engine/TableauState.h
+++ b/src/engine/TableauState.h
@@ -41,13 +41,15 @@ class TableauState
     TableauState();
     ~TableauState();
 
-    void setDimensions( unsigned m, unsigned n, const IBasisFactorization::BasisColumnOracle &oracle );
+    void setDimensions( unsigned m, unsigned n, unsigned m_alloc, unsigned n_alloc, const IBasisFactorization::BasisColumnOracle &oracle );
 
     /*
       The dimensions of matrix A
     */
     unsigned _m;
     unsigned _n;
+    unsigned _m_alloc;
+    unsigned _n_alloc;
 
     /*
       The matrix
diff --git a/src/engine/tests/MockTableau.h b/src/engine/tests/MockTableau.h
index a95e196de0..6e17f8cb2f 100644
--- a/src/engine/tests/MockTableau.h
+++ b/src/engine/tests/MockTableau.h
@@ -111,13 +111,15 @@ class MockTableau : public ITableau
     bool setDimensionsCalled;
     unsigned lastM;
     unsigned lastN;
-    void setDimensions( unsigned m, unsigned n )
+    void setDimensions( unsigned m, unsigned n, unsigned alloc_m, unsigned alloc_n )
     {
         TS_ASSERT( !initializeTableauCalled );
         setDimensionsCalled = true;
         lastRightHandSide = new double[m];
         lastM = m;
         lastN = n;
+        (void)alloc_m;
+        (void)alloc_n;
         lastEntries = new double[m*n];
         std::fill( lastEntries, lastEntries + ( n * m ), 0.0 );
 
diff --git a/src/engine/tests/Test_ConstraintBoundTightener.h b/src/engine/tests/Test_ConstraintBoundTightener.h
index d90ee05304..170c2c6ae6 100644
--- a/src/engine/tests/Test_ConstraintBoundTightener.h
+++ b/src/engine/tests/Test_ConstraintBoundTightener.h
@@ -45,7 +45,7 @@ class ConstraintBoundTightenerTestSuite : public CxxTest::TestSuite
     {
         ConstraintBoundTightener tightener( *tableau );
 
-        tableau->setDimensions( 2, 5 );
+        tableau->setDimensions( 2, 5, 2, 5 );
 
         // Current bounds:
         //  0 <= x0 <= 0
diff --git a/src/engine/tests/Test_CostFunctionManager.h b/src/engine/tests/Test_CostFunctionManager.h
index 2e18e425d3..a239d7bf01 100644
--- a/src/engine/tests/Test_CostFunctionManager.h
+++ b/src/engine/tests/Test_CostFunctionManager.h
@@ -62,7 +62,7 @@ class CostFunctionManagerTestSuite : public CxxTest::TestSuite
 
         unsigned n = 5;
         unsigned m = 3;
-        tableau.setDimensions( m, n );
+        tableau.setDimensions( m, n, m, n );
 
         TS_ASSERT( manager = new CostFunctionManager( &tableau ) );
         TS_ASSERT_THROWS_NOTHING( manager->initialize() );
@@ -122,7 +122,7 @@ class CostFunctionManagerTestSuite : public CxxTest::TestSuite
 
         unsigned n = 5;
         unsigned m = 3;
-        tableau.setDimensions( m, n );
+        tableau.setDimensions( m, n, m, n );
 
         TS_ASSERT( manager = new CostFunctionManager( &tableau ) );
         TS_ASSERT_THROWS_NOTHING( manager->initialize() );
diff --git a/src/engine/tests/Test_DantzigsRule.h b/src/engine/tests/Test_DantzigsRule.h
index 3f3dba12b4..df909322da 100644
--- a/src/engine/tests/Test_DantzigsRule.h
+++ b/src/engine/tests/Test_DantzigsRule.h
@@ -54,7 +54,7 @@ class DantzigsRuleTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( !dantzigsRule.select( *tableau, candidates, excluded ) );
 
-        tableau->setDimensions( 10, 100 );
+        tableau->setDimensions( 10, 100, 10, 100 );
 
         candidates.append( 2 );
         candidates.append( 3 );
diff --git a/src/engine/tests/Test_ProjectedSteepestEdge.h b/src/engine/tests/Test_ProjectedSteepestEdge.h
index db66776468..b177ddd751 100644
--- a/src/engine/tests/Test_ProjectedSteepestEdge.h
+++ b/src/engine/tests/Test_ProjectedSteepestEdge.h
@@ -41,7 +41,7 @@ class ProjectedSteepestEdgeTestSuite : public CxxTest::TestSuite
     void test_variable_selection()
     {
         MockTableau tableau;
-        tableau.setDimensions( 2, 5 );
+        tableau.setDimensions( 2, 5, 2, 5 );
 
         ProjectedSteepestEdgeRule pse;
 
diff --git a/src/engine/tests/Test_RowBoundTightener.h b/src/engine/tests/Test_RowBoundTightener.h
index 1babd86b39..0003d5139f 100644
--- a/src/engine/tests/Test_RowBoundTightener.h
+++ b/src/engine/tests/Test_RowBoundTightener.h
@@ -45,7 +45,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
     {
         RowBoundTightener tightener( *tableau );
 
-        tableau->setDimensions( 2, 5 );
+        tableau->setDimensions( 2, 5, 2, 5 );
 
         // Current bounds:
         //  0 <= x0 <= 0
@@ -107,7 +107,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
     {
         RowBoundTightener tightener( *tableau );
 
-        tableau->setDimensions( 2, 5 );
+        tableau->setDimensions( 2, 5, 2, 5 );
 
         // Current bounds:
         //    0  <= x0 <= 0
@@ -158,7 +158,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
     {
         RowBoundTightener tightener( *tableau );
 
-        tableau->setDimensions( 2, 5 );
+        tableau->setDimensions( 2, 5, 2, 5 );
 
         tableau->setLowerBound( 0, -200 );
         tableau->setUpperBound( 0, 0 );
@@ -203,7 +203,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
     {
         RowBoundTightener tightener( *tableau );
 
-        tableau->setDimensions( 2, 5 );
+        tableau->setDimensions( 2, 5, 2, 5 );
 
         tableau->setLowerBound( 0, -112 );
         tableau->setUpperBound( 0, 101 );
@@ -240,7 +240,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
     {
         RowBoundTightener tightener( *tableau );
 
-        tableau->setDimensions( 1, 5 );
+        tableau->setDimensions( 1, 5, 1, 5 );
 
         tableau->setLowerBound( 0, 0 );
         tableau->setUpperBound( 0, 3 );
@@ -301,7 +301,7 @@ class RowBoundTightenerTestSuite : public CxxTest::TestSuite
     {
         RowBoundTightener tightener( *tableau );
 
-        tableau->setDimensions( 2, 5 );
+        tableau->setDimensions( 2, 5, 2, 5 );
 
         tableau->setLowerBound( 0, 0 );
         tableau->setUpperBound( 0, 3 );
diff --git a/src/engine/tests/Test_Tableau.h b/src/engine/tests/Test_Tableau.h
index 9f160c8877..7dc59a8dc6 100644
--- a/src/engine/tests/Test_Tableau.h
+++ b/src/engine/tests/Test_Tableau.h
@@ -114,7 +114,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         initializeTableauValues( *tableau );
 
         for ( unsigned i = 0; i < tableau->getN(); ++i )
@@ -132,7 +132,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         initializeTableauValues( *tableau );
 
         for ( unsigned i = 0; i < 4; ++i )
@@ -177,7 +177,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         initializeTableauValues( *tableau );
 
         for ( unsigned i = 0; i < 4; ++i )
@@ -234,7 +234,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -286,7 +286,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -338,7 +338,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -449,7 +449,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -511,7 +511,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -589,7 +589,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -798,7 +798,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -1001,7 +1001,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         // Initialization steps
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -1129,7 +1129,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -1286,7 +1286,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );
 
@@ -1363,7 +1363,7 @@ class TableauTestSuite : public CxxTest::TestSuite
 
         TS_ASSERT( tableau = new Tableau );
 
-        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7 ) );
+        TS_ASSERT_THROWS_NOTHING( tableau->setDimensions( 3, 7, 3, 7 ) );
         tableau->registerCostFunctionManager( &costFunctionManager );
         initializeTableauValues( *tableau );