diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp
index e8ea7305e..1c492718b 100644
--- a/src/engine/AbsoluteValueConstraint.cpp
+++ b/src/engine/AbsoluteValueConstraint.cpp
@@ -148,7 +148,7 @@ void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound
                 // If phase is not fixed, both bonds are stored and checker should check the max of the two
                 if ( proofs && !phaseFixed() )
                     _boundManager->addLemmaExplanationAndTightenBound( _f, fUpperBound, BoundType::UPPER,
-                                                                      {variable, variable}, BoundType::UPPER, getType() );
+                                                                      { variable, variable }, BoundType::UPPER, getType() );
                 else if ( proofs && phaseFixed() )
                 {
                     std::shared_ptr<TableauRow> tighteningRow = fUpperBound == getUpperBound( _b ) ? _posTighteningRow : _negTighteningRow;
@@ -222,7 +222,7 @@ void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound
                 // If phase is not fixed, both bonds are stored and checker should check the max of the two
                 if ( proofs && !phaseFixed() )
                     _boundManager->addLemmaExplanationAndTightenBound( _f, fUpperBound, BoundType::UPPER,
-                                                                      {variable, variable}, BoundType::UPPER, getType() );
+                                                                      { variable, variable }, BoundType::UPPER, getType() );
                 else if ( proofs && phaseFixed() )
                 {
                     std::shared_ptr<TableauRow> tighteningRow = fUpperBound == bound ? _posTighteningRow : _negTighteningRow;
@@ -807,7 +807,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
     {
         setPhaseStatus( ABS_PHASE_POSITIVE );
         if ( proofs )
-            _boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, {_b},
+            _boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, { _b },
                                                                BoundType::LOWER, getType() );
         return;
     }
@@ -817,7 +817,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
     {
         setPhaseStatus( ABS_PHASE_NEGATIVE );
         if ( proofs )
-            _boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, {_b},
+            _boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, { _b },
                                                                BoundType::UPPER, getType() );
         return;
     }
@@ -831,7 +831,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
     {
         setPhaseStatus( ABS_PHASE_NEGATIVE );
         if ( proofs )
-            _boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, {_b, _f},
+            _boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, { _b, _f },
                                                                BoundType::UPPER, getType() );
         return;
     }
@@ -842,7 +842,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
     {
         setPhaseStatus( ABS_PHASE_POSITIVE );
         if ( proofs )
-            _boundManager->addLemmaExplanationAndTightenBound(  _posAux, 0, BoundType::UPPER, {_b, _f},
+            _boundManager->addLemmaExplanationAndTightenBound(  _posAux, 0, BoundType::UPPER, { _b, _f },
                                                                 BoundType::LOWER, getType() );
         return;
     }
@@ -861,7 +861,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
         {
             setPhaseStatus( ABS_PHASE_NEGATIVE );
             if ( proofs )
-                _boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, {_posAux},
+                _boundManager->addLemmaExplanationAndTightenBound( _negAux, 0, BoundType::UPPER, { _posAux },
                                                                    BoundType::LOWER, getType() );
             return;
         }
@@ -878,7 +878,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
         {
             setPhaseStatus( ABS_PHASE_POSITIVE );
             if ( proofs )
-                _boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, {_negAux},
+                _boundManager->addLemmaExplanationAndTightenBound( _posAux, 0, BoundType::UPPER, { _negAux },
                                                                   BoundType::LOWER, getType() );
             return;
         }
diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp
index c53cf8346..6be58f9d0 100644
--- a/src/engine/ReluConstraint.cpp
+++ b/src/engine/ReluConstraint.cpp
@@ -172,7 +172,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
             {
                 // If we're in the active phase, aux should be 0
                 if ( proofs && _auxVarInUse )
-                    _boundManager->addLemmaExplanationAndTightenBound( _aux, 0, BoundType::UPPER, {variable},
+                    _boundManager->addLemmaExplanationAndTightenBound( _aux, 0, BoundType::UPPER, { variable },
                                                                       BoundType::LOWER, getType() );
                 else if ( !proofs && _auxVarInUse )
                     _boundManager->tightenUpperBound( _aux, 0 );
@@ -186,7 +186,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
             else if ( _auxVarInUse && variable == _b && FloatUtils::isZero( bound ) )
             {
                 if ( proofs && _auxVarInUse )
-                    _boundManager->addLemmaExplanationAndTightenBound( _aux, 0, BoundType::UPPER, {variable},
+                    _boundManager->addLemmaExplanationAndTightenBound( _aux, 0, BoundType::UPPER, { variable },
                                                                       BoundType::LOWER, getType() );
 			    else if ( !proofs && _auxVarInUse )
                     _boundManager->tightenUpperBound( _aux, 0 );
@@ -197,7 +197,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
             else if ( _auxVarInUse && variable == _aux && bound > 0 )
             {
                 if ( proofs )
-                    _boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::UPPER, {variable},
+                    _boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::UPPER, { variable },
                                                                       BoundType::LOWER, getType() );
                 else
                     _boundManager->tightenUpperBound( _f, 0 );
@@ -215,7 +215,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
                     if ( _phaseStatus == RELU_PHASE_INACTIVE )
                         _boundManager->tightenUpperBound( _aux, -bound, *_tighteningRow );
                     else if ( _phaseStatus == PHASE_NOT_FIXED )
-                        _boundManager->addLemmaExplanationAndTightenBound( _aux, -bound, BoundType::UPPER, {variable},
+                        _boundManager->addLemmaExplanationAndTightenBound( _aux, -bound, BoundType::UPPER, { variable },
                                                                           BoundType::LOWER, getType() );
                 }
                 else
@@ -227,7 +227,7 @@ void ReluConstraint::notifyLowerBound( unsigned variable, double newBound )
             else if ( bound < 0 && variable == _f )
             {
                 if ( proofs )
-                    _boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::LOWER, {variable},
+                    _boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::LOWER, { variable },
                                                                       BoundType::LOWER, getType() );
                 else
                     _boundManager->tightenLowerBound( _f, 0 );
@@ -272,7 +272,7 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
                     else
                     {
                         if ( FloatUtils::isZero( bound ) )
-                            _boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::UPPER, {variable},
+                            _boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::UPPER, { variable },
                                                                               BoundType::UPPER, getType() );
                         // Bound cannot be negative if ReLU is inactive
                         else if ( FloatUtils::isNegative( bound ) )
@@ -289,7 +289,7 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
                 {
                     // If b has a non-positive upper bound, f's upper bound is 0
                     if ( proofs )
-                        _boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::UPPER, {variable},
+                        _boundManager->addLemmaExplanationAndTightenBound( _f, 0, BoundType::UPPER, { variable },
                                                                           BoundType::UPPER, getType() );
                     else
                         _boundManager->tightenUpperBound( _f, 0 );
@@ -308,7 +308,7 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
                         if ( _phaseStatus == RELU_PHASE_ACTIVE )
                             _boundManager->tightenUpperBound( _f, bound, *_tighteningRow );
                         else if ( _phaseStatus == PHASE_NOT_FIXED )
-                            _boundManager->addLemmaExplanationAndTightenBound( _f, bound, BoundType::UPPER, {variable},
+                            _boundManager->addLemmaExplanationAndTightenBound( _f, bound, BoundType::UPPER, { variable },
                                                                               BoundType::UPPER, getType() );
                     }
                     else
@@ -324,7 +324,7 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
                     else
                     {
                         if ( FloatUtils::isZero( bound ) )
-                            _boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::LOWER, {variable},
+                            _boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::LOWER, { variable },
                                                                               BoundType::UPPER, getType() );
                         // Bound cannot be negative if ReLU is active
                         else if ( FloatUtils::isNegative( bound ) )
diff --git a/src/engine/SignConstraint.cpp b/src/engine/SignConstraint.cpp
index 50002936f..47b248163 100644
--- a/src/engine/SignConstraint.cpp
+++ b/src/engine/SignConstraint.cpp
@@ -403,9 +403,9 @@ void SignConstraint::notifyLowerBound( unsigned variable, double bound )
                 if ( FloatUtils::gt( bound, 1 ) )
                     throw InfeasibleQueryException();
 
-                _boundManager->addLemmaExplanationAndTightenBound( _f, 1, BoundType::LOWER, {variable},
+                _boundManager->addLemmaExplanationAndTightenBound( _f, 1, BoundType::LOWER, { variable },
                                                                    BoundType::LOWER, getType() );
-                _boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::LOWER, {variable},
+                _boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::LOWER, { variable },
                                                                    BoundType::LOWER, getType() );
             }
             else
@@ -421,7 +421,7 @@ void SignConstraint::notifyLowerBound( unsigned variable, double bound )
         if ( _boundManager != nullptr )
         {
             if ( _boundManager->shouldProduceProofs() )
-                _boundManager->addLemmaExplanationAndTightenBound( _f, 1, BoundType::LOWER, {variable},
+                _boundManager->addLemmaExplanationAndTightenBound( _f, 1, BoundType::LOWER, { variable },
                                                                    BoundType::LOWER, getType() );
             else
                 _boundManager->tightenLowerBound( _f, 1 );
@@ -455,9 +455,9 @@ void SignConstraint::notifyUpperBound( unsigned variable, double bound )
                 if ( FloatUtils::lt( bound, -1 )  )
                     throw InfeasibleQueryException();
 
-                _boundManager->addLemmaExplanationAndTightenBound( _f, -1, BoundType::UPPER, {variable},
+                _boundManager->addLemmaExplanationAndTightenBound( _f, -1, BoundType::UPPER, { variable },
                                                                   BoundType::UPPER, getType() );
-                _boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::UPPER, {variable},
+                _boundManager->addLemmaExplanationAndTightenBound( _b, 0, BoundType::UPPER, { variable },
                                                                    BoundType::UPPER, getType() );
             }
             else
@@ -473,7 +473,7 @@ void SignConstraint::notifyUpperBound( unsigned variable, double bound )
         if ( _boundManager != nullptr )
         {
             if ( _boundManager->shouldProduceProofs() )
-                _boundManager->addLemmaExplanationAndTightenBound( _f, -1, BoundType::UPPER, {variable},
+                _boundManager->addLemmaExplanationAndTightenBound( _f, -1, BoundType::UPPER, { variable },
                                                                   BoundType::UPPER, getType() );
             else
                 _boundManager->tightenUpperBound( _f, -1 );