diff --git a/src/configuration/GlobalConfiguration.cpp b/src/configuration/GlobalConfiguration.cpp
index c6986cd98..d5e4013dd 100644
--- a/src/configuration/GlobalConfiguration.cpp
+++ b/src/configuration/GlobalConfiguration.cpp
@@ -69,6 +69,7 @@ const double GlobalConfiguration::PSE_GAMMA_ERROR_THRESHOLD = 0.001;
 const double GlobalConfiguration::PSE_GAMMA_UPDATE_TOLERANCE = 0.000000001;
 
 const double GlobalConfiguration::RELU_CONSTRAINT_COMPARISON_TOLERANCE = 0.001;
+const double GlobalConfiguration::ABS_CONSTRAINT_COMPARISON_TOLERANCE = 0.001;
 
 const bool GlobalConfiguration::ONLY_AUX_INITIAL_BASIS = false;
 
diff --git a/src/configuration/GlobalConfiguration.h b/src/configuration/GlobalConfiguration.h
index d8e217947..6786c50e4 100644
--- a/src/configuration/GlobalConfiguration.h
+++ b/src/configuration/GlobalConfiguration.h
@@ -131,9 +131,12 @@ class GlobalConfiguration
     // PSE's Gamma function's update tolerance
     static const double PSE_GAMMA_UPDATE_TOLERANCE;
 
-    // The tolerance for checking whether f = Relu( b ), to determine a ReLU's statisfaction
+    // The tolerance for checking whether f = Relu( b )
     static const double RELU_CONSTRAINT_COMPARISON_TOLERANCE;
 
+    // The tolerance for checking whether f = Abs( b )
+    static const double ABS_CONSTRAINT_COMPARISON_TOLERANCE;
+
     // Should the initial basis be comprised only of auxiliary (row) variables?
     static const bool ONLY_AUX_INITIAL_BASIS;
 
diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp
new file mode 100644
index 000000000..e5d9d540c
--- /dev/null
+++ b/src/engine/AbsoluteValueConstraint.cpp
@@ -0,0 +1,440 @@
+/*********************                                                        */
+/*! \file ReluConstraint.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Shiran Aziz, Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ **/
+
+#include "AbsoluteValueConstraint.h"
+#include "ConstraintBoundTightener.h"
+#include "Debug.h"
+#include "FloatUtils.h"
+#include "ITableau.h"
+#include "MStringf.h"
+#include "MarabouError.h"
+#include "PiecewiseLinearCaseSplit.h"
+#include "Statistics.h"
+
+AbsoluteValueConstraint::AbsoluteValueConstraint( unsigned b, unsigned f )
+    : _b( b )
+    , _f( f )
+    , _haveEliminatedVariables( false )
+{
+    setPhaseStatus( PhaseStatus::PHASE_NOT_FIXED );
+}
+
+PiecewiseLinearConstraint *AbsoluteValueConstraint::duplicateConstraint() const
+{
+    AbsoluteValueConstraint *clone = new AbsoluteValueConstraint( _b, _f );
+    *clone = *this;
+    return clone;
+}
+
+void AbsoluteValueConstraint::restoreState( const PiecewiseLinearConstraint *state )
+{
+    const AbsoluteValueConstraint *abs = dynamic_cast<const AbsoluteValueConstraint *>( state );
+    *this = *abs;
+}
+
+void AbsoluteValueConstraint::registerAsWatcher( ITableau *tableau )
+{
+    tableau->registerToWatchVariable( this, _b );
+    tableau->registerToWatchVariable( this, _f );
+}
+
+void AbsoluteValueConstraint::unregisterAsWatcher( ITableau *tableau )
+{
+    tableau->unregisterToWatchVariable( this, _b );
+    tableau->unregisterToWatchVariable( this, _f );
+}
+
+void AbsoluteValueConstraint::notifyVariableValue( unsigned variable, double value )
+{
+    _assignment[variable] = value;
+}
+
+void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound )
+{
+    if ( _statistics )
+        _statistics->incNumBoundNotificationsPlConstraints();
+
+    if ( _lowerBounds.exists( variable ) &&
+         !FloatUtils::gt( bound, _lowerBounds[variable] ) )
+        return;
+
+    _lowerBounds[variable] = bound;
+
+    // Check whether the phase has become fixed
+    fixPhaseIfNeeded();
+
+    // Update partner's bound
+    if ( isActive() && _constraintBoundTightener )
+    {
+        if ( variable == _b )
+        {
+            if ( bound < 0 )
+            {
+                double fUpperBound = FloatUtils::max( -bound, _upperBounds[_b] );
+                _constraintBoundTightener->registerTighterUpperBound( _f, fUpperBound );
+            }
+            else
+            {
+                // Phase is fixed, don't care about this case
+            }
+        }
+        else
+        {
+            // F's lower bound can only cause bound propagations if it
+            // fixes the phase of the constraint, so no need to
+            // bother.  The only exception is if the lower bound is,
+            // for some reason, negative
+            if ( bound < 0 )
+                _constraintBoundTightener->registerTighterLowerBound( _f, 0 );
+        }
+    }
+}
+
+void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound )
+{
+    if ( _statistics )
+        _statistics->incNumBoundNotificationsPlConstraints();
+
+    if ( _upperBounds.exists( variable ) && !FloatUtils::lt( bound, _upperBounds[variable] ) )
+        return;
+
+    _upperBounds[variable] = bound;
+
+    // Check whether the phase has become fixed
+    fixPhaseIfNeeded();
+
+    // Update partner's bound
+    if ( isActive() && _constraintBoundTightener )
+    {
+        if ( variable == _b )
+        {
+            if ( bound > 0 )
+            {
+                double fUpperBound = FloatUtils::max( bound, -_lowerBounds[_b] );
+                _constraintBoundTightener->registerTighterUpperBound( _f, fUpperBound );
+            }
+            else
+            {
+                // Phase is fixed, don't care about this case
+            }
+        }
+        else
+        {
+            // F's upper bound can restrict both bounds of B
+            if ( bound < _upperBounds[_b] )
+                _constraintBoundTightener->registerTighterUpperBound( _b, bound );
+
+            if ( -bound > _lowerBounds[_b] )
+                _constraintBoundTightener->registerTighterLowerBound( _b, -bound );
+        }
+    }
+}
+
+bool AbsoluteValueConstraint::participatingVariable(unsigned variable ) const
+{
+    return ( variable == _b ) || ( variable == _f );
+}
+
+List<unsigned> AbsoluteValueConstraint::getParticipatingVariables() const
+{
+    return List<unsigned>( { _b, _f } );
+}
+
+bool AbsoluteValueConstraint::satisfied() const
+{
+    if ( !( _assignment.exists( _b ) && _assignment.exists( _f ) ) )
+        throw MarabouError( MarabouError::PARTICIPATING_VARIABLES_ABSENT );
+
+    double bValue = _assignment.get( _b );
+    double fValue = _assignment.get( _f );
+
+    // Possible violations:
+    //   1. f is negative
+    //   2. f is positive, abs(b) and f are not equal
+
+    if ( fValue < 0 )
+        return false;
+
+    return FloatUtils::areEqual( FloatUtils::abs( bValue ),
+                                 fValue,
+                                 GlobalConfiguration::ABS_CONSTRAINT_COMPARISON_TOLERANCE );
+}
+
+List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getPossibleFixes() const
+{
+    ASSERT( !satisfied() );
+    ASSERT( _assignment.exists( _b ) );
+    ASSERT( _assignment.exists( _f ) );
+
+    double bValue = _assignment.get( _b );
+    double fValue = _assignment.get( _f );
+
+    ASSERT( !FloatUtils::isNegative( fValue ) );
+
+    List<PiecewiseLinearConstraint::Fix> fixes;
+
+    // Possible violations:
+    //   1. f is positive, b is positive, b and f are unequal
+    //   2. f is positive, b is negative, -b and f are unequal
+
+    fixes.append( PiecewiseLinearConstraint::Fix( _b, fValue ) );
+    fixes.append( PiecewiseLinearConstraint::Fix( _b, -fValue ) );
+    fixes.append( PiecewiseLinearConstraint::Fix( _f, FloatUtils::abs( bValue ) ) );
+
+    return fixes;
+}
+
+List<PiecewiseLinearConstraint::Fix> AbsoluteValueConstraint::getSmartFixes( ITableau */* tableau */ ) const
+{
+    return getPossibleFixes();
+}
+
+List<PiecewiseLinearCaseSplit> AbsoluteValueConstraint::getCaseSplits() const
+{
+    ASSERT( _phaseStatus == PhaseStatus::PHASE_NOT_FIXED );
+
+    List<PiecewiseLinearCaseSplit> splits;
+    splits.append( getNegativeSplit() );
+    splits.append( getPositiveSplit() );
+
+    return splits;
+}
+
+PiecewiseLinearCaseSplit AbsoluteValueConstraint::getNegativeSplit() const
+{
+    PiecewiseLinearCaseSplit negativePhase;
+
+    // Negative phase: b <= 0, b + f = 0
+    negativePhase.storeBoundTightening( Tightening( _b, 0.0, Tightening::UB ) );
+
+    Equation negativeEquation( Equation::EQ );
+    negativeEquation.addAddend( 1, _b );
+    negativeEquation.addAddend( 1, _f );
+    negativeEquation.setScalar( 0 );
+    negativePhase.addEquation( negativeEquation );
+
+    return negativePhase;
+}
+
+PiecewiseLinearCaseSplit AbsoluteValueConstraint::getPositiveSplit() const
+{
+    PiecewiseLinearCaseSplit positivePhase;
+
+    // Positive phase: b >= 0, b - f = 0
+    positivePhase.storeBoundTightening( Tightening( _b, 0.0, Tightening::LB ) );
+
+    //b - f = 0
+    Equation positiveEquation( Equation::EQ );
+    positiveEquation.addAddend( 1, _b );
+    positiveEquation.addAddend( -1, _f );
+    positiveEquation.setScalar( 0 );
+    positivePhase.addEquation( positiveEquation );
+
+    return positivePhase;
+}
+
+bool AbsoluteValueConstraint::phaseFixed() const
+{
+    return _phaseStatus != PhaseStatus::PHASE_NOT_FIXED;
+}
+
+PiecewiseLinearCaseSplit AbsoluteValueConstraint::getValidCaseSplit() const
+{
+    ASSERT( _phaseStatus != PhaseStatus::PHASE_NOT_FIXED );
+
+    if ( _phaseStatus == PhaseStatus::PHASE_POSITIVE )
+        return getPositiveSplit();
+
+    return getNegativeSplit();
+}
+
+void AbsoluteValueConstraint::eliminateVariable( unsigned /* variable */, double /* fixedValue */ )
+{
+    // In an absolute value constraint, if a variable is removed the
+    // entire constraint can be discarded
+    _haveEliminatedVariables = true;
+}
+
+void AbsoluteValueConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )
+{
+    ASSERT( oldIndex == _b || oldIndex == _f );
+    ASSERT( !_assignment.exists( newIndex ) &&
+            !_lowerBounds.exists( newIndex ) &&
+            !_upperBounds.exists( newIndex ) &&
+            newIndex != _b && newIndex != _f );
+
+    if ( _assignment.exists( oldIndex ) )
+    {
+        _assignment[newIndex] = _assignment.get( oldIndex );
+        _assignment.erase( oldIndex );
+    }
+
+    if ( _lowerBounds.exists( oldIndex ) )
+    {
+        _lowerBounds[newIndex] = _lowerBounds.get( oldIndex );
+        _lowerBounds.erase( oldIndex );
+    }
+
+    if ( _upperBounds.exists( oldIndex ) )
+    {
+        _upperBounds[newIndex] = _upperBounds.get( oldIndex );
+        _upperBounds.erase( oldIndex );
+    }
+
+    if ( oldIndex == _b )
+        _b = newIndex;
+    else
+        _f = newIndex;
+}
+
+bool AbsoluteValueConstraint::constraintObsolete() const
+{
+    return _haveEliminatedVariables;
+}
+
+void AbsoluteValueConstraint::getEntailedTightenings( List<Tightening> &tightenings ) const
+{
+    ASSERT( _lowerBounds.exists( _b ) && _lowerBounds.exists( _f ) &&
+            _upperBounds.exists( _b ) && _upperBounds.exists( _f ) );
+
+    // Upper bounds
+    double bUpperBound = _upperBounds[_b];
+    double fUpperBound = _upperBounds[_f];
+    // Lower bounds
+    double bLowerBound = _lowerBounds[_b];
+    double fLowerBound = _lowerBounds[_f];
+
+    // F's lower bound should always be non-negative
+    if ( fLowerBound < 0 )
+    {
+        tightenings.append( Tightening( _f, 0.0, Tightening::LB ) );
+        fLowerBound = 0;
+    }
+
+    if ( bLowerBound >= 0 )
+    {
+        // Positive phase, all bounds much match
+        tightenings.append( Tightening( _f, bLowerBound, Tightening::LB ) );
+        tightenings.append( Tightening( _b, fLowerBound, Tightening::LB ) );
+
+        tightenings.append( Tightening( _f, bUpperBound, Tightening::UB ) );
+        tightenings.append( Tightening( _b, fUpperBound, Tightening::UB ) );
+    }
+
+    else if ( bUpperBound <= 0 )
+    {
+        // Negative phase, all bounds must match
+
+        tightenings.append( Tightening( _f, -bUpperBound, Tightening::LB ) );
+        tightenings.append( Tightening( _b, -fUpperBound, Tightening::LB ) );
+
+        tightenings.append( Tightening( _f, -bLowerBound, Tightening::UB ) );
+        tightenings.append( Tightening( _b, -fLowerBound, Tightening::UB ) );
+    }
+
+    else if ( bLowerBound < 0 && bUpperBound >= 0 && FloatUtils::isZero( fLowerBound ) )
+    {
+        // Phase undetermined, b can be either positive or negative, f can be 0
+        tightenings.append( Tightening( _b, -fUpperBound , Tightening::LB ) );
+        tightenings.append( Tightening( _b, fUpperBound, Tightening::UB ) );
+        tightenings.append( Tightening( _f, FloatUtils::max( -bLowerBound , bUpperBound ), Tightening::UB ) );
+    }
+
+    else if ( bLowerBound < 0 && bUpperBound >= 0 && fLowerBound > 0 )
+    {
+        // Phase undetermined, b can be either positive or negative, f strictly positive
+        tightenings.append( Tightening( _b, -fUpperBound, Tightening::LB ) );
+        tightenings.append( Tightening( _b, fUpperBound, Tightening::UB ) );
+        tightenings.append( Tightening( _f, FloatUtils::max( -bLowerBound, bUpperBound ), Tightening::UB ) );
+
+        // Below we test if the phase has actually become fixed
+        if ( fLowerBound > -bLowerBound )
+        {
+            // Positive phase
+            tightenings.append( Tightening( _b, fLowerBound, Tightening::LB ) );
+        }
+
+        if ( fLowerBound > bUpperBound )
+        {
+            // Negative phase
+            tightenings.append( Tightening( _b, -fLowerBound, Tightening::UB ) );
+        }
+
+    }
+}
+
+void AbsoluteValueConstraint::getAuxiliaryEquations( List<Equation> &/* newEquations */ ) const
+{
+    // Currently unsupported
+}
+
+String AbsoluteValueConstraint::serializeToString() const
+{
+    // Output format is: Abs,f,b
+    return Stringf( "absoluteValue,%u,%u", _f, _b );
+}
+
+void AbsoluteValueConstraint::fixPhaseIfNeeded()
+{
+    // Option 1: b's range is strictly positive
+    if ( _lowerBounds.exists( _b ) && _lowerBounds[_b] >= 0 )
+    {
+        setPhaseStatus( PHASE_POSITIVE );
+        return;
+    }
+
+    // Option 2: b's range is strictly negative:
+    if ( _upperBounds.exists( _b ) && _upperBounds[_b] <= 0 )
+    {
+        setPhaseStatus( PHASE_NEGATIVE );
+        return;
+    }
+
+    if ( !_lowerBounds.exists( _f ) )
+        return;
+
+    // Option 3: f's range is strictly disjoint from b's positive
+    // range
+    if ( _upperBounds.exists( _b ) && _lowerBounds[_f] > _upperBounds[_b] )
+    {
+        setPhaseStatus( PHASE_NEGATIVE );
+        return;
+    }
+
+    // Option 4: f's range is strictly disjoint from b's negative
+    // range, in absolute value
+    if ( _lowerBounds.exists( _b ) && _lowerBounds[_f] > -_lowerBounds[_b] )
+    {
+        setPhaseStatus( PHASE_POSITIVE );
+        return;
+    }
+}
+
+void AbsoluteValueConstraint::setPhaseStatus( PhaseStatus phaseStatus )
+{
+    _phaseStatus = phaseStatus;
+}
+
+bool AbsoluteValueConstraint::supportsSymbolicBoundTightening() const
+{
+    return false;
+}
+
+//
+// Local Variables:
+// compile-command: "make -C ../.. "
+// tags-file-name: "../../TAGS"
+// c-basic-offset: 4
+// End:
+//
diff --git a/src/engine/AbsoluteValueConstraint.h b/src/engine/AbsoluteValueConstraint.h
new file mode 100644
index 000000000..a652c0b1d
--- /dev/null
+++ b/src/engine/AbsoluteValueConstraint.h
@@ -0,0 +1,172 @@
+/*********************                                                        */
+/*! \file ReluConstraint.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Shiran Aziz, Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+ **/
+
+#ifndef __AbsoluteValueConstraint_h__
+#define __AbsoluteValueConstraint_h__
+
+#include "PiecewiseLinearConstraint.h"
+
+class AbsoluteValueConstraint : public PiecewiseLinearConstraint
+{
+
+public:
+    enum PhaseStatus {
+        PHASE_NOT_FIXED = 0,
+        PHASE_POSITIVE = 1,
+        PHASE_NEGATIVE = 2,
+    };
+
+    AbsoluteValueConstraint( unsigned b, unsigned f );
+
+    /*
+      Return a clone of the constraint.
+    */
+    PiecewiseLinearConstraint *duplicateConstraint() const;
+
+    /*
+      Restore the state of this constraint from the given one.
+    */
+    void restoreState( const PiecewiseLinearConstraint *state );
+
+    /*
+      Register/unregister the constraint with a talbeau.
+     */
+    void registerAsWatcher( ITableau *tableau);
+    void unregisterAsWatcher( ITableau *tableau);
+
+    /*
+      These callbacks are invoked when a watched variable's value
+      changes, or when its bounds change.
+    */
+    void notifyVariableValue( unsigned variable, double value );
+    void notifyLowerBound( unsigned variable, double bound );
+    void notifyUpperBound( unsigned variable, double bound );
+
+    /*
+       Returns true iff the variable participates in this piecewise
+       linear constraint.
+     */
+    bool participatingVariable( unsigned variable ) const;
+
+    /*
+      Get the list of variables participating in this constraint.
+    */
+    List<unsigned> getParticipatingVariables() const;
+
+    /*
+      Returns true iff the assignment satisfies the constraint
+    */
+    bool satisfied() const;
+
+    /*
+      Returns a list of possible fixes for the violated constraint.
+    */
+    List<PiecewiseLinearConstraint::Fix> getPossibleFixes() const;
+
+    /*
+      Return a list of smart fixes for violated constraint.
+      Currently not implemented, just calls getPossibleFixes().
+    */
+    List<PiecewiseLinearConstraint::Fix> getSmartFixes( ITableau *tableau ) const;
+
+    /*
+      Returns the list of case splits that this piecewise linear
+      constraint breaks into:
+
+      y = |x| <-->
+         ( x <= 0 /\ y = -x ) \/ ( x >= 0 /\ y = x )
+    */
+    List<PiecewiseLinearCaseSplit> getCaseSplits() const;
+
+    /*
+      Check whether the constraint's phase has been fixed.
+    */
+    void fixPhaseIfNeeded();
+    bool phaseFixed() const;
+
+    /*
+     * If the constraint's phase has been fixed, get the (valid) case split.
+     */
+    PiecewiseLinearCaseSplit getValidCaseSplit() const;
+
+    /*
+      Preprocessing related functions, to inform that a variable has
+      been eliminated completely because it was fixed to some value,
+      or that a variable's index has changed (e.g., x4 is now called
+      x2). constraintObsolete() returns true iff and the constraint
+      has become obsolote as a result of variable eliminations.
+     */
+    void eliminateVariable( unsigned variable, double fixedValue );
+    void updateVariableIndex( unsigned oldIndex, unsigned newIndex );
+    bool constraintObsolete() const;
+
+    /*
+      Get the tightenings entailed by the constraint.
+    */
+    void getEntailedTightenings( List<Tightening> &tightenings ) const;
+
+    /*
+      For preprocessing: get any auxiliary equations that this
+      constraint would like to add to the equation pool. In the ReLU
+      case, this is an equation of the form aux = f - b, where aux is
+      non-negative.
+    */
+    void getAuxiliaryEquations( List<Equation> &newEquations ) const;
+
+    /*
+      Returns string with shape: absoluteValue,_f,_b
+     */
+    String serializeToString() const;
+
+    /*
+      Return true if and only if this piecewise linear constraint supports
+      symbolic bound tightening.
+    */
+    bool supportsSymbolicBoundTightening() const;
+
+private:
+    /*
+      The variables that make up this constraint; _f = | _b |.
+    */
+    unsigned _b, _f;
+
+    /*
+      True iff _b or _f have been eliminated.
+    */
+    bool _haveEliminatedVariables;
+
+    /*
+      The phase status of this constraint: positive, negative, or not
+      yet fixed.
+    */
+    PhaseStatus _phaseStatus;
+    void setPhaseStatus( PhaseStatus phaseStatus );
+
+    /*
+      The two case splits.
+    */
+    PiecewiseLinearCaseSplit getPositiveSplit() const;
+    PiecewiseLinearCaseSplit getNegativeSplit() const;
+};
+
+#endif // __AbsoluteValueConstraint_h__
+
+//
+// Local Variables:
+// compile-command: "make -C ../.. "
+// tags-file-name: "../../TAGS"
+// c-basic-offset: 4
+// End:
+//
diff --git a/src/engine/CMakeLists.txt b/src/engine/CMakeLists.txt
index e2e4229eb..46122d992 100644
--- a/src/engine/CMakeLists.txt
+++ b/src/engine/CMakeLists.txt
@@ -16,6 +16,7 @@ macro(engine_add_unit_test name)
         USE_MOCK_ENGINE "unit")
 endmacro()
 
+engine_add_unit_test(AbsoluteValueConstraint)
 engine_add_unit_test(BlandsRule)
 engine_add_unit_test(ConstraintBoundTightener)
 engine_add_unit_test(ConstraintMatrixAnalyzer)
diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
index 0f539d96b..fc48b43e8 100644
--- a/src/engine/Engine.cpp
+++ b/src/engine/Engine.cpp
@@ -1125,6 +1125,8 @@ void Engine::extractSolution( InputQuery &inputQuery )
             if ( _preprocessor.variableIsFixed( variable ) )
             {
                 inputQuery.setSolutionValue( i, _preprocessor.getFixedValue( variable ) );
+                inputQuery.setLowerBound( i, _preprocessor.getFixedValue( variable ) );
+                inputQuery.setUpperBound( i, _preprocessor.getFixedValue( variable ) );
                 continue;
             }
 
@@ -1134,10 +1136,14 @@ void Engine::extractSolution( InputQuery &inputQuery )
 
             // Finally, set the assigned value
             inputQuery.setSolutionValue( i, _tableau->getValue( variable ) );
+            inputQuery.setLowerBound( i, _tableau->getLowerBound( variable ) );
+            inputQuery.setUpperBound( i, _tableau->getUpperBound( variable ) );
         }
         else
         {
             inputQuery.setSolutionValue( i, _tableau->getValue( i ) );
+            inputQuery.setLowerBound( i, _tableau->getLowerBound( i ) );
+            inputQuery.setUpperBound( i, _tableau->getUpperBound( i ) );
         }
     }
 }
diff --git a/src/engine/InputQuery.cpp b/src/engine/InputQuery.cpp
index 3bdbf9553..70ad73951 100644
--- a/src/engine/InputQuery.cpp
+++ b/src/engine/InputQuery.cpp
@@ -343,7 +343,7 @@ void InputQuery::saveQuery( const String &fileName )
     // Lower Bounds
     for ( const auto &lb : _lowerBounds )
         queryFile->write( Stringf( "\n%d,%f", lb.first, lb.second ) );
-    
+
     // Upper Bounds
     for ( const auto &ub : _upperBounds )
         queryFile->write( Stringf( "\n%d,%f", ub.first, ub.second ) );
@@ -431,6 +431,29 @@ List<unsigned> InputQuery::getOutputVariables() const
     return result;
 }
 
+void InputQuery::printAllBounds() const
+{
+    printf( "InputQuery: Dumping all bounds\n" );
+
+    for ( unsigned i = 0; i < _numberOfVariables; ++i )
+    {
+        printf( "\tx%u: [", i );
+        if ( _lowerBounds.exists( i ) )
+            printf( "%lf, ", _lowerBounds[i] );
+        else
+            printf( "-INF, " );
+
+        if ( _upperBounds.exists( i ) )
+            printf( "%lf]", _upperBounds[i] );
+        else
+            printf( "+INF]" );
+        printf( "\n" );
+
+    }
+
+    printf( "\n\n" );
+}
+
 void InputQuery::printInputOutputBounds() const
 {
     printf( "Dumping bounds of the input and output variables:\n" );
diff --git a/src/engine/InputQuery.h b/src/engine/InputQuery.h
index 9a5530767..a2603b980 100644
--- a/src/engine/InputQuery.h
+++ b/src/engine/InputQuery.h
@@ -57,7 +57,7 @@ class InputQuery
       Methods for handling input and output variables
     */
     void markInputVariable( unsigned variable, unsigned inputIndex );
-    void markOutputVariable( unsigned variable, unsigned inputIndex );
+    void markOutputVariable( unsigned variable, unsigned outputIndex );
     unsigned inputVariableByIndex( unsigned index ) const;
     unsigned outputVariableByIndex( unsigned index ) const;
     unsigned getNumInputVariables() const;
@@ -118,6 +118,7 @@ class InputQuery
     */
     void printInputOutputBounds() const;
     void dump() const;
+    void printAllBounds() const;
 
     /*
       Adjsut the input/output variable mappings because variables have been merged
diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h
index 4988d273b..844263d83 100644
--- a/src/engine/PiecewiseLinearConstraint.h
+++ b/src/engine/PiecewiseLinearConstraint.h
@@ -236,6 +236,19 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher
         _score = score;
     }
 
+    /*
+      Retrieve the current lower and upper bounds
+    */
+    double getLowerBound( unsigned i ) const
+    {
+        return _lowerBounds[i];
+    }
+
+    double getUpperBound( unsigned i ) const
+    {
+        return _upperBounds[i];
+    }
+
 protected:
     bool _constraintActive;
 	Map<unsigned, double> _assignment;
diff --git a/src/engine/Preprocessor.cpp b/src/engine/Preprocessor.cpp
index c30bbea7a..09e931758 100644
--- a/src/engine/Preprocessor.cpp
+++ b/src/engine/Preprocessor.cpp
@@ -69,7 +69,6 @@ InputQuery Preprocessor::preprocess( const InputQuery &query, bool attemptVariab
     {
         continueTightening = processEquations();
         continueTightening = processConstraints() || continueTightening;
-
         if ( attemptVariableElimination )
             continueTightening = processIdenticalVariables() || continueTightening;
 
diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp
index 681f88c0a..a8008ee3b 100644
--- a/src/engine/ReluConstraint.cpp
+++ b/src/engine/ReluConstraint.cpp
@@ -46,7 +46,7 @@ ReluConstraint::ReluConstraint( const String &serializedRelu )
     String constraintType = serializedRelu.substring( 0, 4 );
     ASSERT( constraintType == String( "relu" ) );
 
-    // remove the constraint type in serialized form
+    // Remove the constraint type in serialized form
     String serializedValues = serializedRelu.substring( 5, serializedRelu.length() - 5 );
     List<String> values = serializedValues.tokenize( "," );
 
diff --git a/src/engine/ReluConstraint.h b/src/engine/ReluConstraint.h
index f8ac26798..b6c7bc861 100644
--- a/src/engine/ReluConstraint.h
+++ b/src/engine/ReluConstraint.h
@@ -100,10 +100,11 @@ class ReluConstraint : public PiecewiseLinearConstraint
     PiecewiseLinearCaseSplit getValidCaseSplit() const;
 
     /*
-      Preprocessing related functions, to inform that a variable has been eliminated completely
-      because it was fixed to some value, or that a variable's index has changed (e.g., x4 is now
-      called x2). constraintObsolete() returns true iff and the constraint has become obsolote
-      as a result of variable eliminations.
+      Preprocessing related functions, to inform that a variable has
+      been eliminated completely because it was fixed to some value,
+      or that a variable's index has changed (e.g., x4 is now called
+      x2). constraintObsolete() returns true iff and the constraint
+      has become obsolote as a result of variable eliminations.
     */
     void eliminateVariable( unsigned variable, double fixedValue );
     void updateVariableIndex( unsigned oldIndex, unsigned newIndex );
diff --git a/src/engine/tests/Test_AbsoluteValueConstraint.h b/src/engine/tests/Test_AbsoluteValueConstraint.h
new file mode 100644
index 000000000..a33defee0
--- /dev/null
+++ b/src/engine/tests/Test_AbsoluteValueConstraint.h
@@ -0,0 +1,1059 @@
+/*********************                                                        */
+/*! \file Test_ReluConstraint.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Shiran Aziz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+**/
+
+#include <cxxtest/TestSuite.h>
+
+#include "AbsoluteValueConstraint.h"
+#include "MarabouError.h"
+#include "MockErrno.h"
+#include "MockTableau.h"
+#include "PiecewiseLinearCaseSplit.h"
+#include <iostream>
+#include <string.h>
+
+class MockForAbsoluteValueConstraint : public MockErrno
+{
+public:
+};
+
+class AbsoluteValueConstraintTestSuite : public CxxTest::TestSuite
+{
+public:
+    MockForAbsoluteValueConstraint *mock;
+
+    void setUp()
+    {
+        TS_ASSERT( mock = new MockForAbsoluteValueConstraint );
+    }
+
+    void tearDown()
+    {
+        TS_ASSERT_THROWS_NOTHING( delete mock );
+    }
+
+    void test_abs_duplicate_and_restore()
+    {
+        AbsoluteValueConstraint abs1( 4, 6 );
+        abs1.setActiveConstraint( false );
+        abs1.notifyVariableValue( 4, 1.0 );
+        abs1.notifyVariableValue( 6, 1.0 );
+
+        abs1.notifyLowerBound( 4, -8.0 );
+        abs1.notifyUpperBound( 4, 8.0 );
+
+        abs1.notifyLowerBound( 6, 0.0 );
+        abs1.notifyUpperBound( 6, 8.0 );
+
+        PiecewiseLinearConstraint *abs2 = abs1.duplicateConstraint();
+
+        abs1.notifyVariableValue( 4, -2 );
+
+        TS_ASSERT( !abs1.satisfied() );
+
+        TS_ASSERT( !abs2->isActive() );
+        TS_ASSERT( abs2->satisfied() );
+
+        abs2->restoreState( &abs1 );
+        TS_ASSERT( !abs2->satisfied() );
+
+        TS_ASSERT_THROWS_NOTHING( delete abs2 );
+    }
+
+    void test_register_and_unregister_as_watcher()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        MockTableau tableau;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        TS_ASSERT_THROWS_NOTHING( abs.registerAsWatcher( &tableau ) );
+
+        TS_ASSERT_EQUALS( tableau.lastRegisteredVariableToWatcher.size(), 2U );
+        TS_ASSERT( tableau.lastUnregisteredVariableToWatcher.empty() );
+        TS_ASSERT_EQUALS( tableau.lastRegisteredVariableToWatcher[b].size(), 1U );
+        TS_ASSERT( tableau.lastRegisteredVariableToWatcher[b].exists( &abs ) );
+        TS_ASSERT_EQUALS( tableau.lastRegisteredVariableToWatcher[f].size(), 1U );
+        TS_ASSERT( tableau.lastRegisteredVariableToWatcher[f].exists( &abs ) );
+
+        tableau.lastRegisteredVariableToWatcher.clear();
+
+        TS_ASSERT_THROWS_NOTHING( abs.unregisterAsWatcher( &tableau ) );
+
+        TS_ASSERT( tableau.lastRegisteredVariableToWatcher.empty() );
+        TS_ASSERT_EQUALS( tableau.lastUnregisteredVariableToWatcher.size(), 2U );
+        TS_ASSERT_EQUALS( tableau.lastUnregisteredVariableToWatcher[b].size(), 1U );
+        TS_ASSERT( tableau.lastUnregisteredVariableToWatcher[b].exists( &abs ) );
+        TS_ASSERT_EQUALS( tableau.lastUnregisteredVariableToWatcher[f].size(), 1U );
+        TS_ASSERT( tableau.lastUnregisteredVariableToWatcher[f].exists( &abs ) );
+    }
+
+    void test_participating_variables()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        List<unsigned> participatingVariables;
+
+        TS_ASSERT_THROWS_NOTHING( participatingVariables = abs.getParticipatingVariables() );
+        TS_ASSERT_EQUALS( participatingVariables.size(), 2U );
+        auto it = participatingVariables.begin();
+        TS_ASSERT_EQUALS( *it, b );
+        ++it;
+        TS_ASSERT_EQUALS( *it, f );
+
+        TS_ASSERT_EQUALS( abs.getParticipatingVariables(), List<unsigned>( {1,4} ) );
+
+        TS_ASSERT( abs.participatingVariable( b ) );
+        TS_ASSERT( abs.participatingVariable( f ) );
+        TS_ASSERT( !abs.participatingVariable( 2 ) );
+        TS_ASSERT( !abs.participatingVariable( 0 ) );
+        TS_ASSERT( !abs.participatingVariable( 5 ) );
+    }
+
+    void test_abs_notify_variable_value_and_satisfied()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        abs.notifyVariableValue( b, 5 );
+        abs.notifyVariableValue( f, 5 );
+        TS_ASSERT( abs.satisfied() );
+
+        abs.notifyVariableValue( b, -5 );
+        abs.notifyVariableValue( f, 5 );
+        TS_ASSERT( abs.satisfied() );
+
+        abs.notifyVariableValue( b, 5 );
+        abs.notifyVariableValue( f, -5 );
+        TS_ASSERT( !abs.satisfied() );
+
+        abs.notifyVariableValue( f, -1 );
+        abs.notifyVariableValue( b, -5 );
+        TS_ASSERT( !abs.satisfied() );
+
+        abs.notifyVariableValue( b, 1 );
+        TS_ASSERT( !abs.satisfied() );
+
+        abs.notifyVariableValue( b, 5 );
+        abs.notifyVariableValue( f, 4 );
+        TS_ASSERT( !abs.satisfied() );
+
+        abs.notifyVariableValue( b, -4 );
+        abs.notifyVariableValue( f, -5 );
+        TS_ASSERT( !abs.satisfied() );
+
+        abs.notifyVariableValue( f, 1 );
+        abs.notifyVariableValue( b, -2 );
+        TS_ASSERT( !abs.satisfied() );
+
+        abs.notifyVariableValue( f, -1 );
+        abs.notifyVariableValue( b, -2 );
+        TS_ASSERT( !abs.satisfied() );
+    }
+
+    void test_abs_update_variable_index()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        // Changing variable indices
+        abs.notifyVariableValue( b, 1 );
+        abs.notifyVariableValue( f, 1 );
+        TS_ASSERT( abs.satisfied() );
+
+        unsigned newB = 12;
+        unsigned newF = 14;
+
+        TS_ASSERT_THROWS_NOTHING( abs.updateVariableIndex( b, newB ) );
+        TS_ASSERT_THROWS_NOTHING( abs.updateVariableIndex( f, newF ) );
+
+        TS_ASSERT( abs.satisfied() );
+
+        abs.notifyVariableValue( newF, 2 );
+
+        TS_ASSERT( !abs.satisfied() );
+
+        abs.notifyVariableValue( newB, 2 );
+
+        TS_ASSERT( abs.satisfied() );
+    }
+
+    void test_abs_getPossibleFixes()
+    {
+        // Possible violations:
+        //   1. f is positive, b is positive, b and f are unequal
+        //   2. f is positive, b is negative, -b and f are unequal
+
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        List<PiecewiseLinearConstraint::Fix> fixes;
+        List<PiecewiseLinearConstraint::Fix>::iterator it;
+
+        //   1. f is positive, b is positive, b and f are unequal
+
+        abs.notifyVariableValue( b, 2 );
+        abs.notifyVariableValue( f, 1 );
+
+        fixes = abs.getPossibleFixes();
+        TS_ASSERT_EQUALS( fixes.size(), 3U );
+        it = fixes.begin();
+        TS_ASSERT_EQUALS( it->_variable, b );
+        TS_ASSERT_EQUALS( it->_value, 1 );
+        ++it;
+        TS_ASSERT_EQUALS( it->_variable, b );
+        TS_ASSERT_EQUALS( it->_value, -1 );
+        ++it;
+        TS_ASSERT_EQUALS( it->_variable, f );
+        TS_ASSERT_EQUALS( it->_value, 2 );
+
+        //   2. f is positive, b is negative, -b and f are unequal
+        abs.notifyVariableValue( b, -2 );
+        abs.notifyVariableValue( f, 1 );
+
+        fixes = abs.getPossibleFixes();
+        TS_ASSERT_EQUALS( fixes.size(), 3U );
+        it = fixes.begin();
+        TS_ASSERT_EQUALS( it->_variable, b );
+        TS_ASSERT_EQUALS( it->_value, 1 );
+        ++it;
+        TS_ASSERT_EQUALS( it->_variable, b );
+        TS_ASSERT_EQUALS( it->_value, -1 );
+        ++it;
+        TS_ASSERT_EQUALS( it->_variable, f );
+        TS_ASSERT_EQUALS( it->_value, 2 );
+    }
+
+    void test_eliminate_variable_b()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        MockTableau tableau;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        abs.registerAsWatcher( &tableau );
+
+        TS_ASSERT( !abs.constraintObsolete() );
+        TS_ASSERT_THROWS_NOTHING( abs.eliminateVariable( b, 5 ) );
+        TS_ASSERT( abs.constraintObsolete() );
+    }
+
+    void test_eliminate_variable_f()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        MockTableau tableau;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        abs.registerAsWatcher( &tableau );
+
+        TS_ASSERT( !abs.constraintObsolete() );
+        TS_ASSERT_THROWS_NOTHING( abs.eliminateVariable( f, 5 ) );
+        TS_ASSERT( abs.constraintObsolete() );
+    }
+
+    void test_abs_entailed_tightenings_positive_phase_1()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List<Tightening> entailedTightenings;
+
+        abs.notifyLowerBound( b, 1 );
+        abs.notifyLowerBound( f, 2 );
+        abs.notifyUpperBound( b, 7 );
+        abs.notifyUpperBound( f, 7 );
+
+        // 1 < x_b < 7 , 2 < x_f < 7 -> 2 < x_b
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 1, 2, 7, 7, entailedTightenings );
+
+        abs.notifyLowerBound( b, 3 );
+        // 3 < x_b < 7 , 2 < x_f < 7
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 3, 2, 7, 7, entailedTightenings );
+
+        abs.notifyLowerBound( f, 3 );
+        abs.notifyUpperBound( b, 6 );
+        // 3 < x_b < 6 , 3 < x_f < 7
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 3, 3, 6, 7, entailedTightenings );
+
+        abs.notifyUpperBound( f, 6 );
+        abs.notifyUpperBound( b, 7 );
+        // 3 < x_b < 6 , 3 < x_f < 6
+        //  --> x_b < 6
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 3, 3, 6, 6, entailedTightenings );
+
+        abs.notifyLowerBound( f, -3 );
+        // 3 < x_b < 6 , 3 < x_f < 6
+        // --> 3 < x_f
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 3, 3, 6, 6, entailedTightenings );
+
+        abs.notifyLowerBound( b, 5 );
+        abs.notifyUpperBound( f, 5 );
+        // 5 < x_b < 6 , 3 < x_f < 5
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 5, 3, 6, 5, entailedTightenings );
+    }
+
+    void test_abs_entailed_tightenings_positive_phase_2()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List<Tightening> entailedTightenings;
+
+        // 8 < b < 18, 48 < f < 64
+        abs.notifyUpperBound( b, 18 );
+        abs.notifyUpperBound( f, 64 );
+        abs.notifyLowerBound( b, 8 );
+        abs.notifyLowerBound( f, 48 );
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 8, 48, 18, 64, entailedTightenings );
+    }
+
+    void test_abs_entailed_tightenings_positive_phase_3()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List<Tightening> entailedTightenings;
+
+        // 3 < b < 4, 1 < f < 2
+        abs.notifyUpperBound( b, 4 );
+        abs.notifyUpperBound( f, 2 );
+        abs.notifyLowerBound( b, 3 );
+        abs.notifyLowerBound( f, 1 );
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 3, 1, 4, 2, entailedTightenings );
+    }
+
+    void test_abs_entailed_tightenings_positive_phase_4()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List <Tightening> entailedTightenings;
+        List<Tightening>::iterator it;
+
+        abs.notifyUpperBound( b, 7 );
+        abs.notifyUpperBound( f, 6 );
+        abs.notifyLowerBound( b, 0 );
+        abs.notifyLowerBound( f, 0 );
+
+        // 0 < x_b < 7 ,0 < x_f < 6
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 0, 0, 7, 6, entailedTightenings );
+
+        abs.notifyUpperBound( b, 5 );
+        // 0 < x_b < 5 ,0 < x_f < 6
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 0, 0, 5, 6, entailedTightenings );
+
+        abs.notifyLowerBound( b, 1 );
+        // 1 < x_b < 5 ,0 < x_f < 6
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 1, 0, 5, 6, entailedTightenings );
+
+        abs.notifyUpperBound( f, 4 );
+        // 1 < x_b < 5 ,0 < x_f < 4
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 1, 0, 5, 4, entailedTightenings );
+
+        // Non overlap
+        abs.notifyUpperBound( f, 2 );
+        abs.notifyLowerBound( b, 3 );
+
+        // 3 < x_b < 5 ,0 < x_f < 2
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        TS_ASSERT_EQUALS( entailedTightenings.size(), 4U );
+        assert_lower_upper_bound( f, b, 3, 0, 5, 2, entailedTightenings );
+    }
+
+    void test_abs_entailed_tightenings_positive_phase_5()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List <Tightening> entailedTightenings;
+
+        abs.notifyUpperBound( b, 6 );
+        abs.notifyUpperBound( f, 5 );
+        abs.notifyLowerBound( b, 4 );
+        abs.notifyLowerBound( f, 3 );
+
+        // 4 < x_b < 6 ,3 < x_f < 5
+        entailedTightenings.clear();
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_lower_upper_bound( f, b, 4, 3, 6, 5, entailedTightenings );
+    }
+
+    void test_abs_entailed_tightenings_positive_phase_6()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List<Tightening> entailedTightenings;
+        List<Tightening>::iterator it;
+
+        abs.notifyLowerBound( b, 5 );
+        abs.notifyUpperBound( b, 10 );
+        abs.notifyLowerBound( f, -1 );
+        abs.notifyUpperBound( f, 10 );
+
+        TS_ASSERT( abs.phaseFixed() );
+        abs.getEntailedTightenings( entailedTightenings );
+
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( f, 0, Tightening::LB ),
+
+                                      Tightening( b, 0, Tightening::LB ),
+                                      Tightening( b, 10, Tightening::UB ),
+                                      Tightening( f, 5, Tightening::LB ),
+                                      Tightening( f, 10, Tightening::UB ),
+                                  }) );
+    }
+
+    void test_abs_entailed_tightenings_phase_not_fixed_f_strictly_positive()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List <Tightening> entailedTightenings;
+        List<Tightening>::iterator it;
+
+        abs.notifyLowerBound( b, -6 );
+        abs.notifyUpperBound( b, 3 );
+        abs.notifyLowerBound( f, 2 );
+        abs.notifyUpperBound( f, 4 );
+
+        // -6 < x_b < 3 ,2 < x_f < 4
+        abs.getEntailedTightenings( entailedTightenings );
+
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -4, Tightening::LB ),
+                                      Tightening( b, 4, Tightening::UB ),
+                                      Tightening( f, 6, Tightening::UB ),
+                                  }) );
+
+        entailedTightenings.clear();
+
+        // -6 < x_b < 2 ,2 < x_f < 4
+        abs.notifyUpperBound( b, 2 );
+        abs.getEntailedTightenings( entailedTightenings );
+
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -4, Tightening::LB ),
+                                      Tightening( b, 4, Tightening::UB ),
+                                      Tightening( f, 6, Tightening::UB ),
+                                  }) );
+
+        entailedTightenings.clear();
+
+        // -6 < x_b < 1 ,2 < x_f < 4, now stuck in negative phase
+        abs.notifyUpperBound( b, 1 );
+        abs.getEntailedTightenings( entailedTightenings );
+
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -4, Tightening::LB ),
+                                      Tightening( b, 4, Tightening::UB ),
+                                      Tightening( f, 6, Tightening::UB ),
+                                      Tightening( b, -2, Tightening::UB ),
+                                  }) );
+    }
+
+    void test_abs_entailed_tightenings_phase_not_fixed_f_strictly_positive_2()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List <Tightening> entailedTightenings;
+        List<Tightening>::iterator it;
+
+        abs.notifyLowerBound( b, -5 );
+        abs.notifyUpperBound( b, 10 );
+        abs.notifyLowerBound( f, 3 );
+        abs.notifyUpperBound( f, 7 );
+
+        // -5 < x_b < 10 ,3 < x_f < 7
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -7, Tightening::LB ),
+                                      Tightening( b, 7, Tightening::UB ),
+                                      Tightening( f, 10, Tightening::UB ),
+                                  }) );
+
+        entailedTightenings.clear();
+
+        // -5 < x_b < 10 ,6 < x_f < 7, positive phase
+        abs.notifyLowerBound( f, 6 );
+
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -7, Tightening::LB ),
+                                      Tightening( b, 7, Tightening::UB ),
+                                      Tightening( f, 10, Tightening::UB ),
+                                      Tightening( b, 6, Tightening::LB ),
+                                  }) );
+
+        entailedTightenings.clear();
+
+        // -5 < x_b < 3 ,6 < x_f < 7
+
+        // Extreme case, disjoint ranges
+
+        abs.notifyUpperBound( b, 3 );
+
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -7, Tightening::LB ),
+                                      Tightening( b, 7, Tightening::UB ),
+                                      Tightening( f, 5, Tightening::UB ),
+                                      Tightening( b, 6, Tightening::LB ),
+                                      Tightening( b, -6, Tightening::UB ),
+                                  }) );
+    }
+
+    void test_abs_entailed_tightenings_phase_not_fixed_f_strictly_positive_3()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs(b, f);
+        List <Tightening> entailedTightenings;
+        List<Tightening>::iterator it;
+
+        abs.notifyLowerBound( b, -1 );
+        abs.notifyUpperBound( b, 1 );
+        abs.notifyLowerBound( f, 2 );
+        abs.notifyUpperBound( f, 4 );
+
+        // -1 < x_b < 1 ,2 < x_f < 4
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -4, Tightening::LB ),
+                                      Tightening( b, 4, Tightening::UB ),
+                                      Tightening( f, 1, Tightening::UB ),
+                                      Tightening( b, 2, Tightening::LB ),
+                                      Tightening( b, -2, Tightening::UB ),
+                                  }) );
+    }
+
+    void test_abs_entailed_tightenings_phase_not_fixed_f_non_negative()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List <Tightening> entailedTightenings;
+        List<Tightening>::iterator it;
+
+        abs.notifyLowerBound( b, -7 );
+        abs.notifyUpperBound( b, 7 );
+        abs.notifyLowerBound( f, 0 );
+        abs.notifyUpperBound( f, 6 );
+
+        // -7 < x_b < 7 ,0 < x_f < 6
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -6, Tightening::LB ),
+                                      Tightening( b, 6, Tightening::UB ),
+                                      Tightening( f, 7, Tightening::UB ),
+                                  }) );
+
+
+        entailedTightenings.clear();
+
+        // -7 < x_b < 5 ,0 < x_f < 6
+        abs.notifyUpperBound( b, 5 );
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -6, Tightening::LB ),
+                                      Tightening( b, 6, Tightening::UB ),
+                                      Tightening( f, 7, Tightening::UB ),
+                                  }) );
+
+        entailedTightenings.clear();
+        // 0 < x_b < 5 ,0 < x_f < 6
+        abs.notifyLowerBound( b, 0 );
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, 0, Tightening::LB ),
+                                      Tightening( b, 6, Tightening::UB ),
+                                      Tightening( f, 0, Tightening::LB ),
+                                      Tightening( f, 5, Tightening::UB ),
+                                  }) );
+
+
+        entailedTightenings.clear();
+
+        // 3 < x_b < 5 ,0 < x_f < 6
+        abs.notifyLowerBound( b, 3 );
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, 0, Tightening::LB ),
+                                      Tightening( b, 6, Tightening::UB ),
+                                      Tightening( f, 3, Tightening::LB ),
+                                      Tightening( f, 5, Tightening::UB ),
+                                  }) );
+    }
+
+    void test_abs_entailed_tightenings_negative_phase()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List <Tightening> entailedTightenings;
+        List<Tightening>::iterator it;
+
+        abs.notifyLowerBound( b, -20 );
+        abs.notifyUpperBound( b, -2 );
+        abs.notifyLowerBound( f, 0 );
+        abs.notifyUpperBound( f, 15 );
+
+        // -20 < x_b < -2 ,0 < x_f < 15
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -15, Tightening::LB ),
+                                      Tightening( b, 0, Tightening::UB ),
+                                      Tightening( f, 2, Tightening::LB ),
+                                      Tightening( f, 20, Tightening::UB ),
+                                  }) );
+
+
+        entailedTightenings.clear();
+
+        // -20 < x_b < -2 ,7 < x_f < 15
+        abs.notifyLowerBound( f, 7 );
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -15, Tightening::LB ),
+                                      Tightening( b, -7, Tightening::UB ),
+                                      Tightening( f, 2, Tightening::LB ),
+                                      Tightening( f, 20, Tightening::UB ),
+                                  }) );
+
+        entailedTightenings.clear();
+
+        // -12 < x_b < -2 ,7 < x_f < 15
+        abs.notifyLowerBound( b, -12 );
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -15, Tightening::LB ),
+                                      Tightening( b, -7, Tightening::UB ),
+                                      Tightening( f, 2, Tightening::LB ),
+                                      Tightening( f, 12, Tightening::UB ),
+                                  }) );
+
+        entailedTightenings.clear();
+
+        // -12 < x_b < -8 ,7 < x_f < 15
+        abs.notifyUpperBound( b, -8 );
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -15, Tightening::LB ),
+                                      Tightening( b, -7, Tightening::UB ),
+                                      Tightening( f, 8, Tightening::LB ),
+                                      Tightening( f, 12, Tightening::UB ),
+                                  }) );
+    }
+
+    void test_abs_entailed_tightenings_negative_phase_2()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+        List <Tightening> entailedTightenings;
+        List<Tightening>::iterator it;
+
+        abs.notifyLowerBound( b, -20 );
+        abs.notifyUpperBound( b, -2 );
+        abs.notifyLowerBound( f, 25 );
+        abs.notifyUpperBound( f, 30 );
+
+        // -20 < x_b < -2 ,25 < x_f < 30
+        abs.getEntailedTightenings( entailedTightenings );
+        assert_tightenings_match( entailedTightenings,
+                                  List<Tightening>
+                                  ({
+                                      Tightening( b, -30, Tightening::LB ),
+                                      Tightening( b, -25, Tightening::UB ),
+                                      Tightening( f, 2, Tightening::LB ),
+                                      Tightening( f, 20, Tightening::UB ),
+                                  }) );
+    }
+
+    void test_abs_case_splits()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        List<PiecewiseLinearConstraint::Fix> fixes;
+        List<PiecewiseLinearConstraint::Fix>::iterator it;
+
+        List<PiecewiseLinearCaseSplit> splits = abs.getCaseSplits();
+
+        Equation positiveEquation, negativeEquation;
+
+        TS_ASSERT_EQUALS( splits.size(), 2U );
+
+        List<PiecewiseLinearCaseSplit>::iterator split1 = splits.begin();
+        List<PiecewiseLinearCaseSplit>::iterator split2 = split1;
+        ++split2;
+
+        TS_ASSERT( isPositiveSplit( b, f, split1 ) || isPositiveSplit( b, f, split2 ) );
+        TS_ASSERT( isNegativeSplit( b, f, split1 ) || isNegativeSplit( b, f, split2 ) );
+    }
+
+    bool isPositiveSplit( unsigned b, unsigned f, List<PiecewiseLinearCaseSplit>::iterator &split )
+    {
+        List<Tightening> bounds = split->getBoundTightenings();
+
+        auto bound = bounds.begin();
+        Tightening bound1 = *bound;
+
+        TS_ASSERT_EQUALS( bound1._variable, b );
+        TS_ASSERT_EQUALS( bound1._value, 0.0 );
+
+        if ( bound1._type != Tightening::LB )
+            return false;
+
+        TS_ASSERT_EQUALS( bounds.size(), 1U );
+
+        Equation positiveEquation;
+        auto equations = split->getEquations();
+        TS_ASSERT_EQUALS( equations.size(), 1U );
+        positiveEquation = split->getEquations().front();
+        TS_ASSERT_EQUALS( positiveEquation._addends.size(), 2U );
+        TS_ASSERT_EQUALS( positiveEquation._scalar, 0.0 );
+
+        auto addend = positiveEquation._addends.begin();
+        TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
+        TS_ASSERT_EQUALS( addend->_variable, b );
+
+        ++addend;
+        TS_ASSERT_EQUALS( addend->_coefficient, -1.0 );
+        TS_ASSERT_EQUALS( addend->_variable, f );
+
+        TS_ASSERT_EQUALS( positiveEquation._type, Equation::EQ );
+
+        return true;
+    }
+
+    bool isNegativeSplit( unsigned b, unsigned f, List<PiecewiseLinearCaseSplit>::iterator &split )
+    {
+        List<Tightening> bounds = split->getBoundTightenings();
+
+        auto bound = bounds.begin();
+        Tightening bound1 = *bound;
+
+        TS_ASSERT_EQUALS( bound1._variable, b );
+        TS_ASSERT_EQUALS( bound1._value, 0.0 );
+
+        if ( bound1._type != Tightening::UB )
+            return false;
+
+        Equation negativeEquation;
+        auto equations = split->getEquations();
+        TS_ASSERT_EQUALS( equations.size(), 1U );
+        negativeEquation = split->getEquations().front();
+        TS_ASSERT_EQUALS( negativeEquation._addends.size(), 2U );
+        TS_ASSERT_EQUALS( negativeEquation._scalar, 0.0 );
+
+        auto addend = negativeEquation._addends.begin();
+        TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
+        TS_ASSERT_EQUALS( addend->_variable, b );
+
+        ++addend;
+        TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
+        TS_ASSERT_EQUALS( addend->_variable, f );
+
+        TS_ASSERT_EQUALS( negativeEquation._type, Equation::EQ );
+        return true;
+    }
+
+    void test_constraint_phase_gets_fixed()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        MockTableau tableau;
+
+        // Upper bounds
+        {
+            AbsoluteValueConstraint abs( b, f );
+            TS_ASSERT( !abs.phaseFixed() );
+            abs.notifyUpperBound( b, -1.0 );
+            TS_ASSERT( abs.phaseFixed() );
+        }
+
+        {
+            AbsoluteValueConstraint abs( b, f );
+            TS_ASSERT( !abs.phaseFixed() );
+            abs.notifyUpperBound( b, 0.0 );
+            TS_ASSERT( abs.phaseFixed() );
+        }
+
+        {
+            AbsoluteValueConstraint abs( b, f );
+            TS_ASSERT( !abs.phaseFixed() );
+            abs.notifyUpperBound( f, 5 );
+            TS_ASSERT( !abs.phaseFixed() );
+        }
+
+        {
+            AbsoluteValueConstraint abs( b, f );
+            TS_ASSERT( !abs.phaseFixed() );
+            abs.notifyUpperBound( b, 3.0 );
+            TS_ASSERT( !abs.phaseFixed() );
+        }
+
+        // Lower bounds
+        {
+            AbsoluteValueConstraint abs( b, f );
+            TS_ASSERT( !abs.phaseFixed() );
+            abs.notifyLowerBound( b, 3.0 );
+            TS_ASSERT( abs.phaseFixed() );
+        }
+
+        {
+            AbsoluteValueConstraint abs( b, f );
+            TS_ASSERT( !abs.phaseFixed() );
+            abs.notifyLowerBound( b, 0.0 );
+            TS_ASSERT( abs.phaseFixed() );
+        }
+
+        {
+            AbsoluteValueConstraint abs( b, f );
+            TS_ASSERT( !abs.phaseFixed() );
+            abs.notifyLowerBound( f, 6.0 );
+            TS_ASSERT( !abs.phaseFixed() );
+        }
+
+        {
+            AbsoluteValueConstraint abs( b, f );
+            TS_ASSERT( !abs.phaseFixed() );
+            abs.notifyLowerBound( b, -2.5 );
+            TS_ASSERT( !abs.phaseFixed() );
+        }
+    }
+
+    void test_valid_split_abs_phase_fixed_to_active()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        List<PiecewiseLinearConstraint::Fix> fixes;
+        List<PiecewiseLinearConstraint::Fix>::iterator it;
+
+        TS_ASSERT( !abs.phaseFixed() );
+        TS_ASSERT_THROWS_NOTHING( abs.notifyLowerBound( b, 5 ) );
+        TS_ASSERT( abs.phaseFixed() );
+
+        PiecewiseLinearCaseSplit split;
+        TS_ASSERT_THROWS_NOTHING( split = abs.getValidCaseSplit() );
+
+        Equation activeEquation;
+
+        List<Tightening> bounds = split.getBoundTightenings();
+
+        TS_ASSERT_EQUALS( bounds.size(), 1U );
+        auto bound = bounds.begin();
+        Tightening bound1 = *bound;
+
+        TS_ASSERT_EQUALS( bound1._variable, b );
+        TS_ASSERT_EQUALS( bound1._type, Tightening::LB );
+        TS_ASSERT_EQUALS( bound1._value, 0.0 );
+
+        auto equations = split.getEquations();
+        TS_ASSERT_EQUALS( equations.size(), 1U );
+        activeEquation = split.getEquations().front();
+        TS_ASSERT_EQUALS( activeEquation._addends.size(), 2U );
+        TS_ASSERT_EQUALS( activeEquation._scalar, 0.0 );
+
+        auto addend = activeEquation._addends.begin();
+        TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
+        TS_ASSERT_EQUALS( addend->_variable, b );
+
+        ++addend;
+        TS_ASSERT_EQUALS( addend->_coefficient, -1.0 );
+        TS_ASSERT_EQUALS( addend->_variable, f );
+
+        TS_ASSERT_EQUALS( activeEquation._type, Equation::EQ );
+    }
+
+    void test_valid_split_abs_phase_fixed_to_inactive()
+    {
+        unsigned b = 1;
+        unsigned f = 4;
+
+        AbsoluteValueConstraint abs( b, f );
+
+        List<PiecewiseLinearConstraint::Fix> fixes;
+        List<PiecewiseLinearConstraint::Fix>::iterator it;
+
+        TS_ASSERT( !abs.phaseFixed() );
+        TS_ASSERT_THROWS_NOTHING( abs.notifyUpperBound( b, -2 ) );
+        TS_ASSERT( abs.phaseFixed() );
+
+        PiecewiseLinearCaseSplit split;
+        TS_ASSERT_THROWS_NOTHING( split = abs.getValidCaseSplit() );
+
+        Equation activeEquation;
+
+        List<Tightening> bounds = split.getBoundTightenings();
+
+        TS_ASSERT_EQUALS( bounds.size(), 1U );
+        auto bound = bounds.begin();
+        Tightening bound1 = *bound;
+
+        TS_ASSERT_EQUALS( bound1._variable, b );
+        TS_ASSERT_EQUALS( bound1._type, Tightening::UB );
+        TS_ASSERT_EQUALS( bound1._value, 0.0 );
+
+        auto equations = split.getEquations();
+        TS_ASSERT_EQUALS( equations.size(), 1U );
+        activeEquation = split.getEquations().front();
+        TS_ASSERT_EQUALS( activeEquation._addends.size(), 2U );
+        TS_ASSERT_EQUALS( activeEquation._scalar, 0.0 );
+
+        auto addend = activeEquation._addends.begin();
+        TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
+        TS_ASSERT_EQUALS( addend->_variable, b );
+
+        ++addend;
+        TS_ASSERT_EQUALS( addend->_coefficient, 1.0 );
+        TS_ASSERT_EQUALS( addend->_variable, f );
+
+        TS_ASSERT_EQUALS( activeEquation._type, Equation::EQ );
+    }
+
+    void assert_lower_upper_bound( unsigned f,
+                                   unsigned b,
+                                   double fLower,
+                                   double bLower,
+                                   double fUpper,
+                                   double bUpper,
+                                   List<Tightening> entailedTightenings )
+    {
+        List<Tightening>::iterator it;
+        it = entailedTightenings.begin();
+
+        TS_ASSERT_EQUALS( entailedTightenings.size(),4U );
+        TS_ASSERT_EQUALS( it->_variable, f );
+        TS_ASSERT_EQUALS( it->_value, fLower );
+        TS_ASSERT_EQUALS( it->_type, Tightening::LB );
+        it++;
+        TS_ASSERT_EQUALS( it->_variable, b );
+        TS_ASSERT_EQUALS( it->_value, bLower );
+        TS_ASSERT_EQUALS( it->_type, Tightening::LB );
+        it++;
+        TS_ASSERT_EQUALS( it->_variable, f );
+        TS_ASSERT_EQUALS( it->_value, fUpper );
+        TS_ASSERT_EQUALS( it->_type, Tightening::UB );
+        it++;
+        TS_ASSERT_EQUALS( it->_variable, b );
+        TS_ASSERT_EQUALS( it->_value, bUpper);
+        TS_ASSERT_EQUALS( it->_type, Tightening::UB );
+    }
+
+    void assert_tightenings_match( List<Tightening> a, List<Tightening> b )
+    {
+        TS_ASSERT_EQUALS( a.size(), b.size() );
+
+        for ( const auto &it : a )
+            TS_ASSERT( b.exists( it ) );
+    }
+};
+
+//
+// Local Variables:
+// compile-command: "make -C ../../.. "
+// tags-file-name: "../../../TAGS"
+// c-basic-offset: 4
+// End:
+//
diff --git a/src/engine/tests/Test_ReluConstraint.h b/src/engine/tests/Test_ReluConstraint.h
index ce597d489..061b361b9 100644
--- a/src/engine/tests/Test_ReluConstraint.h
+++ b/src/engine/tests/Test_ReluConstraint.h
@@ -1225,7 +1225,6 @@ class ReluConstraintTestSuite : public CxxTest::TestSuite
     }
 };
 
-
 //
 // Local Variables:
 // compile-command: "make -C ../../.. "
diff --git a/src/system_tests/CMakeLists.txt b/src/system_tests/CMakeLists.txt
index d801097b1..317dfc8e3 100644
--- a/src/system_tests/CMakeLists.txt
+++ b/src/system_tests/CMakeLists.txt
@@ -12,6 +12,8 @@ add_system_test(max)
 add_system_test(mps)
 add_system_test(relu)
 add_system_test(Disjunction)
+add_system_test(AbsoluteValue)
+
 file(COPY "${RESOURCES_DIR}/mps/lp_feasible_1.mps" DESTINATION ${CMAKE_BINARY_DIR})
 file(COPY "${RESOURCES_DIR}/mps/lp_infeasible_1.mps" DESTINATION ${CMAKE_BINARY_DIR})
 file(COPY ${ACAS_REGRESS_NET} DESTINATION ${CMAKE_BINARY_DIR})
diff --git a/src/system_tests/Test_AbsoluteValue.h b/src/system_tests/Test_AbsoluteValue.h
new file mode 100644
index 000000000..e3ed45212
--- /dev/null
+++ b/src/system_tests/Test_AbsoluteValue.h
@@ -0,0 +1,246 @@
+/*********************                                                        */
+/*! \file Test_Bsolutevalue.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+**/
+
+#include <cxxtest/TestSuite.h>
+
+#include "AbsoluteValueConstraint.h"
+#include "AcasParser.h"
+#include "Engine.h"
+#include "FloatUtils.h"
+#include "InputQuery.h"
+
+class AbsoluteValueTestSuite : public CxxTest::TestSuite
+{
+public:
+    void setUp()
+    {
+    }
+
+    void tearDown()
+    {
+    }
+
+    void test_absoluate_value_unsat()
+    {
+        InputQuery inputQuery;
+        inputQuery.setNumberOfVariables( 6 );
+
+        inputQuery.setLowerBound( 0, -1 );
+        inputQuery.setUpperBound( 0, 1 );
+
+        inputQuery.setLowerBound( 5, 5 );
+        inputQuery.setUpperBound( 5, 6 );
+
+        Equation equation1;
+        equation1.addAddend( 1, 0 );
+        equation1.addAddend( -1, 1 );
+        equation1.setScalar( 0 );
+        inputQuery.addEquation( equation1 );
+
+        Equation equation2;
+        equation2.addAddend( 1, 0 );
+        equation2.addAddend( 1, 3 );
+        equation2.setScalar( 0 );
+        inputQuery.addEquation( equation2 );
+
+        Equation equation3;
+        equation3.addAddend( 1, 2 );
+        equation3.addAddend( 1, 4 );
+        equation3.addAddend( -1, 5 );
+        equation3.setScalar( 0 );
+        inputQuery.addEquation( equation3 );
+
+        AbsoluteValueConstraint *abs1 = new AbsoluteValueConstraint( 1, 2 );
+        AbsoluteValueConstraint *abs2 = new AbsoluteValueConstraint( 3, 4 );
+
+        inputQuery.addPiecewiseLinearConstraint( abs1 );
+        inputQuery.addPiecewiseLinearConstraint( abs2 );
+
+        Engine engine;
+        if ( !engine.processInputQuery( inputQuery ) )
+        {
+            // Expected result
+            return;
+        }
+
+        TS_ASSERT( !engine.solve() );
+    }
+
+    void test_absoluate_value_sat()
+    {
+        InputQuery inputQuery;
+        inputQuery.setNumberOfVariables( 6 );
+
+        inputQuery.setLowerBound( 0, -1 );
+        inputQuery.setUpperBound( 0, 1 );
+
+        inputQuery.setLowerBound( 5, 0.5 );
+        inputQuery.setUpperBound( 5, 6 );
+
+        Equation equation1;
+        equation1.addAddend( 1, 0 );
+        equation1.addAddend( -1, 1 );
+        equation1.setScalar( 0 );
+        inputQuery.addEquation( equation1 );
+
+        Equation equation2;
+        equation2.addAddend( 1, 0 );
+        equation2.addAddend( 1, 3 );
+        equation2.setScalar( 0 );
+        inputQuery.addEquation( equation2 );
+
+        Equation equation3;
+        equation3.addAddend( 1, 2 );
+        equation3.addAddend( 1, 4 );
+        equation3.addAddend( -1, 5 );
+        equation3.setScalar( 0 );
+        inputQuery.addEquation( equation3 );
+
+        AbsoluteValueConstraint *abs1 = new AbsoluteValueConstraint( 1, 2 );
+        AbsoluteValueConstraint *abs2 = new AbsoluteValueConstraint( 3, 4 );
+
+        inputQuery.addPiecewiseLinearConstraint( abs1 );
+        inputQuery.addPiecewiseLinearConstraint( abs2 );
+
+        Engine engine;
+        TS_ASSERT( engine.processInputQuery( inputQuery ) );
+        TS_ASSERT( engine.solve() );
+
+        engine.extractSolution( inputQuery );
+
+        double value_x0 = inputQuery.getSolutionValue( 0 );
+        double value_x1b = inputQuery.getSolutionValue( 1 );
+        double value_x1f = inputQuery.getSolutionValue( 2 );
+        double value_x2b = inputQuery.getSolutionValue( 3 );
+        double value_x2f = inputQuery.getSolutionValue( 4 );
+        double value_x3 = inputQuery.getSolutionValue( 5 );
+
+        TS_ASSERT( FloatUtils::areEqual( value_x0, value_x1b ) );
+        TS_ASSERT( FloatUtils::areEqual( value_x0, -value_x2b ) );
+        TS_ASSERT( FloatUtils::areEqual( value_x3, value_x1f + value_x2f ) );
+
+        TS_ASSERT( FloatUtils::gte( value_x0, -1 ) && FloatUtils::lte( value_x0, 1 ) );
+        TS_ASSERT( FloatUtils::gte( value_x1f, 0 ) && FloatUtils::lte( value_x1f, 1 ) );
+        TS_ASSERT( FloatUtils::gte( value_x3, 0.5 ) && FloatUtils::lte( value_x1f, 6 ) );
+
+        TS_ASSERT( FloatUtils::areEqual( FloatUtils::abs( value_x1b ), value_x1f ) );
+        TS_ASSERT( FloatUtils::areEqual( FloatUtils::abs( value_x2b ), value_x2f ) );
+    }
+
+    void test_absoluate_value_on_acas()
+    {
+        InputQuery inputQuery;
+        AcasParser acasParser( RESOURCES_DIR "/nnet/acasxu/ACASXU_experimental_v2a_1_1.nnet" );
+        acasParser.generateQuery( inputQuery );
+
+        // We run an adversarial-robustness-like query around 0, by
+        // bounding the expression
+        //
+        //   \sum_{i=1}^5 | x_i |
+        //
+        // where x_i are the input nodes. This requires adding 6 new
+        // variables to the query:
+        //
+        //    5 variables for x'_i = abs( x_i )
+        //    1 variable for sum( x'i )
+
+        unsigned numVariables = inputQuery.getNumberOfVariables();
+        inputQuery.setNumberOfVariables( numVariables + 6 );
+
+        // Individual absolute values
+        for ( unsigned i = 0; i < 5; ++i )
+        {
+            unsigned inputVariable = acasParser.getInputVariable( i );
+            AbsoluteValueConstraint *abs = new AbsoluteValueConstraint
+                ( inputVariable, numVariables + i );
+            inputQuery.addPiecewiseLinearConstraint( abs );
+        }
+
+        // Sum of absolute values
+        Equation equation;
+        equation.addAddend( -1, numVariables + 5 );
+        for ( unsigned i = 0; i < 5; ++i )
+        {
+            equation.addAddend( 1, numVariables + i );
+        }
+        inputQuery.addEquation( equation );
+
+        // Bound the maximal L1 change (delta)
+        const double delta = 0.01;
+        inputQuery.setUpperBound( numVariables + 5, delta );
+
+        // Output constraint: we seek a point in which output 0 gets
+        // a lower score than output 1
+        unsigned minimalOutputVar = acasParser.getOutputVariable( 0 );
+        unsigned largerOutputVar = acasParser.getOutputVariable( 1 );
+
+        Equation equationOut;
+        equationOut.setType( Equation::LE );
+
+        // minimal - larger <= 0    -->     larger >= minimal
+        equationOut.addAddend( 1 , minimalOutputVar );
+        equationOut.addAddend( -1, largerOutputVar );
+        equationOut.setScalar( 0 );
+        inputQuery.addEquation( equationOut );
+
+        // Run the query
+        Engine engine;
+        if( !engine.processInputQuery( inputQuery ) )
+        {
+            // No counter example found, this is acceptable
+            return;
+        }
+
+        bool result = engine.solve();
+        if ( !result )
+        {
+            // No counter example found, this is acceptable
+            return;
+        }
+
+        engine.extractSolution( inputQuery );
+
+        // Run through the original network to check correctness
+        Vector<double> inputs;
+        for ( unsigned i = 0; i < 5; ++i )
+        {
+            inputs.append( inputQuery.getSolutionValue( i ) );
+        }
+
+        Vector<double> outputs;
+        acasParser.evaluate( inputs, outputs );
+
+        double minimalOutputValue = outputs[0];
+        double largerOutputValue = outputs[1];
+
+        // Check whether minVar >= runnerUp, as we asked
+        TS_ASSERT( FloatUtils::gte( largerOutputValue, minimalOutputValue ) );
+
+        // Check whether the sum of inptus <= delta
+        double sum = 0.0;
+        for ( unsigned i = 0; i < 5; ++i )
+            sum += FloatUtils::abs( inputs[i] );
+
+        TS_ASSERT( FloatUtils::gte( delta, sum, 0.001 ) );
+    }
+};
+
+//
+// Local Variables:
+// compile-command: "make -C ../../.. "
+// tags-file-name: "../../../TAGS"
+// c-basic-offset: 4
+// End:
+//