diff --git a/.gitignore b/.gitignore
index afd5e86479..334109fb3b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -35,6 +35,7 @@ _deps
 /tools/protobuf*
 /tools/OpenBLAS*
 /tools/onnx*
+/tools/libtorch*
 
 
 build
diff --git a/CHANGELOG.md b/CHANGELOG.md
index cf5f7c56eb..eedb42fdba 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -39,6 +39,9 @@
 * Added support for creating constraints using the overloaded syntax `<=`, `==` etc. in
   the Python backend. See `maraboupy/examples/7_PythonicAPI.py` for details.
 
+* Added support for adversarial attacks to quickly produce a counterexample, in the case
+* of satisfiable queries.
+
 ## Version 1.0.0
 
 * Initial versioned release
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 32ce965f35..9358365ca6 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -20,9 +20,9 @@ option(RUN_SYSTEM_TEST "Run system tests on build" OFF)
 option(RUN_MEMORY_TEST "Run cxxtest testing with ASAN ON" ON)
 option(RUN_PYTHON_TEST "Run Python API tests if building with Python" OFF)
 option(ENABLE_GUROBI "Enable use the Gurobi optimizer" OFF)
-option(ENABLE_OPENBLAS "Do symbolic bound tighting using blas" ON) # Not available on Windows
+option(ENABLE_OPENBLAS "Do symbolic bound tighting using blas" OFF) # Not available on Windows
 option(CODE_COVERAGE "Add code coverage" OFF)  # Available only in debug mode
-
+option(BUILD_TORCH "Build libtorch" OFF)
 ###################
 ## Git variables ##
 ###################
@@ -30,19 +30,19 @@ option(CODE_COVERAGE "Add code coverage" OFF)  # Available only in debug mode
 
 # Get the name of the working branch
 execute_process(
-  COMMAND git rev-parse --abbrev-ref HEAD
-  WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
-  OUTPUT_VARIABLE GIT_BRANCH
-  OUTPUT_STRIP_TRAILING_WHITESPACE
+        COMMAND git rev-parse --abbrev-ref HEAD
+        WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
+        OUTPUT_VARIABLE GIT_BRANCH
+        OUTPUT_STRIP_TRAILING_WHITESPACE
 )
 add_definitions("-DGIT_BRANCH=\"${GIT_BRANCH}\"")
 
 # Get the latest abbreviated commit hash of the working branch
 execute_process(
-  COMMAND git log -1 --format=%h
-  WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
-  OUTPUT_VARIABLE GIT_COMMIT_HASH
-  OUTPUT_STRIP_TRAILING_WHITESPACE
+        COMMAND git log -1 --format=%h
+        WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
+        OUTPUT_VARIABLE GIT_COMMIT_HASH
+        OUTPUT_STRIP_TRAILING_WHITESPACE
 )
 add_definitions("-DGIT_COMMIT_HASH=\"${GIT_COMMIT_HASH}\"")
 
@@ -60,9 +60,9 @@ set(COMMON_DIR "${SRC_DIR}/common")
 set(BASIS_DIR "${SRC_DIR}/basis_factorization")
 
 if (MSVC)
-  set(SCRIPT_EXTENSION bat)
+    set(SCRIPT_EXTENSION bat)
 else()
-  set(SCRIPT_EXTENSION sh)
+    set(SCRIPT_EXTENSION sh)
 endif()
 
 ##########
@@ -85,20 +85,20 @@ add_definitions(-DBOOST_NO_CXX98_FUNCTION_BASE)
 set(BOOST_VERSION 1.84.0)
 set(BOOST_DIR "${TOOLS_DIR}/boost-${BOOST_VERSION}")
 if (MSVC)
-  set(BOOST_ROOT "${BOOST_DIR}/win_installed")
-  set(Boost_NAMESPACE libboost)
+    set(BOOST_ROOT "${BOOST_DIR}/win_installed")
+    set(Boost_NAMESPACE libboost)
 elseif (${CMAKE_SIZEOF_VOID_P} EQUAL 4 AND NOT MSVC)
-  set(BOOST_ROOT "${BOOST_DIR}/installed32")
+    set(BOOST_ROOT "${BOOST_DIR}/installed32")
 else()
-  set(BOOST_ROOT "${BOOST_DIR}/installed")
+    set(BOOST_ROOT "${BOOST_DIR}/installed")
 endif()
 
 set(Boost_USE_DEBUG_RUNTIME FALSE)
 find_package(Boost ${BOOST_VERSION} COMPONENTS program_options timer chrono thread)
 # Find boost
 if (NOT ${Boost_FOUND})
-  execute_process(COMMAND ${TOOLS_DIR}/download_boost.${SCRIPT_EXTENSION} ${BOOST_VERSION})
-  find_package(Boost ${BOOST_VERSION} REQUIRED COMPONENTS program_options timer chrono thread)
+    execute_process(COMMAND ${TOOLS_DIR}/download_boost.${SCRIPT_EXTENSION} ${BOOST_VERSION})
+    find_package(Boost ${BOOST_VERSION} REQUIRED COMPONENTS program_options timer chrono thread)
 endif()
 set(LIBS_INCLUDES ${Boost_INCLUDE_DIRS})
 list(APPEND LIBS ${Boost_LIBRARIES})
@@ -146,36 +146,62 @@ endif()
 file(GLOB DEPS_ONNX "${ONNX_DIR}/*.cc")
 include_directories(SYSTEM ${ONNX_DIR})
 
+#############
+## Pytorch ##
+#############
+
+if (${BUILD_TORCH})
+    message(STATUS "Using pytorch")
+    if (NOT DEFINED BUILD_TORCH)
+        set(BUILD_TORCH $ENV{TORCH_HOME})
+        add_definitions(-DBUILD_TORCH)
+    endif()
+    add_compile_definitions(BUILD_TORCH)
+    set(PYTORCH_VERSION 2.2.1)
+    find_package(Torch ${PYTORCH_VERSION} QUIET)
+    if (NOT Torch_FOUND)
+        set(PYTORCH_DIR "${TOOLS_DIR}/libtorch-${PYTORCH_VERSION}")
+        list(APPEND CMAKE_PREFIX_PATH ${PYTORCH_DIR})
+        if(NOT EXISTS "${PYTORCH_DIR}")
+            execute_process(COMMAND ${TOOLS_DIR}/download_libtorch.sh ${PYTORCH_VERSION})
+        endif()
+        set(Torch_DIR ${PYTORCH_DIR}/share/cmake/Torch)
+        find_package(Torch ${PYTORCH_VERSION} REQUIRED)
+    endif()
+    set(TORCH_CXX_FLAGS "-Wno-error=array-bounds")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${TORCH_CXX_FLAGS}")
+    list(APPEND LIBS ${TORCH_LIBRARIES})
+endif ()
 ############
 ## Gurobi ##
 ############
 
 if (${ENABLE_GUROBI})
-  message(STATUS "Using Gurobi for LP relaxation for bound tightening")
-  if (NOT DEFINED GUROBI_DIR)
-    set(GUROBI_DIR $ENV{GUROBI_HOME})
-  endif()
-  add_compile_definitions(ENABLE_GUROBI)
-
-  set(GUROBI_LIB1 "gurobi_c++")
-  set(GUROBI_LIB2 "gurobi95")
-
-  add_library(${GUROBI_LIB1} SHARED IMPORTED)
-  set_target_properties(${GUROBI_LIB1} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi_c++.a)
-  list(APPEND LIBS ${GUROBI_LIB1})
-  target_include_directories(${GUROBI_LIB1} INTERFACE ${GUROBI_DIR}/include/)
-
-  add_library(${GUROBI_LIB2} SHARED IMPORTED)
-
-  # MACOSx uses .dylib instead of .so for its Gurobi downloads.
-  if (APPLE)
-    set_target_properties(${GUROBI_LIB2} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi95.dylib)
-  else()
-    set_target_properties(${GUROBI_LIB2} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi95.so)
-  endif ()
-
-  list(APPEND LIBS ${GUROBI_LIB2})
-  target_include_directories(${GUROBI_LIB2} INTERFACE ${GUROBI_DIR}/include/)
+    message(STATUS "Using Gurobi for LP relaxation for bound tightening")
+    if (NOT DEFINED GUROBI_DIR)
+        set(GUROBI_DIR $ENV{GUROBI_HOME})
+    endif()
+    add_compile_definitions(ENABLE_GUROBI)
+
+    set(GUROBI_LIB1 "gurobi_c++")
+    set(GUROBI_LIB2 "gurobi110")
+
+    add_library(${GUROBI_LIB1} SHARED IMPORTED)
+    set_target_properties(${GUROBI_LIB1} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi_c++.a)
+    list(APPEND LIBS ${GUROBI_LIB1})
+    target_include_directories(${GUROBI_LIB1} INTERFACE ${GUROBI_DIR}/include/)
+
+    add_library(${GUROBI_LIB2} SHARED IMPORTED)
+
+    # MACOSx uses .dylib instead of .so for its Gurobi downloads.
+    if (APPLE)
+        set_target_properties(${GUROBI_LIB2} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi110.dylib)
+    else()
+        set_target_properties(${GUROBI_LIB2} PROPERTIES IMPORTED_LOCATION ${GUROBI_DIR}/lib/libgurobi110.so)
+    endif ()
+
+    list(APPEND LIBS ${GUROBI_LIB2})
+    target_include_directories(${GUROBI_LIB2} INTERFACE ${GUROBI_DIR}/include/)
 endif()
 
 ##############
@@ -183,30 +209,30 @@ endif()
 ##############
 
 if (NOT MSVC AND ${ENABLE_OPENBLAS})
-  set(OPENBLAS_VERSION 0.3.19)
-
-  set(OPENBLAS_LIB openblas)
-  set(OPENBLAS_DEFAULT_DIR "${TOOLS_DIR}/OpenBLAS-${OPENBLAS_VERSION}")
-  if (NOT OPENBLAS_DIR)
-      set(OPENBLAS_DIR ${OPENBLAS_DEFAULT_DIR})
-  endif()
-
-  message(STATUS "Using OpenBLAS for matrix multiplication")
-  add_compile_definitions(ENABLE_OPENBLAS)
-  if(NOT EXISTS "${OPENBLAS_DIR}/installed/lib/libopenblas.a")
-    message("Can't find OpenBLAS, installing. If OpenBLAS is installed please use the OPENBLAS_DIR parameter to pass the path")
-      if (${OPENBLAS_DIR} STREQUAL ${OPENBLAS_DEFAULT_DIR})
-        message("Installing OpenBLAS")
-        execute_process(COMMAND ${TOOLS_DIR}/download_openBLAS.sh ${OPENBLAS_VERSION})
-      else()
-        message(FATAL_ERROR "Can't find OpenBLAS in the supplied directory")
-      endif()
-  endif()
-
-  add_library(${OPENBLAS_LIB} SHARED IMPORTED)
-  set_target_properties(${OPENBLAS_LIB} PROPERTIES IMPORTED_LOCATION ${OPENBLAS_DIR}/installed/lib/libopenblas.a)
-  list(APPEND LIBS ${OPENBLAS_LIB})
-  target_include_directories(${OPENBLAS_LIB} INTERFACE ${OPENBLAS_DIR}/installed/include)
+    set(OPENBLAS_VERSION 0.3.19)
+
+    set(OPENBLAS_LIB openblas)
+    set(OPENBLAS_DEFAULT_DIR "${TOOLS_DIR}/OpenBLAS-${OPENBLAS_VERSION}")
+    if (NOT OPENBLAS_DIR)
+        set(OPENBLAS_DIR ${OPENBLAS_DEFAULT_DIR})
+    endif()
+
+    message(STATUS "Using OpenBLAS for matrix multiplication")
+    add_compile_definitions(ENABLE_OPENBLAS)
+    if(NOT EXISTS "${OPENBLAS_DIR}/installed/lib/libopenblas.a")
+        message("Can't find OpenBLAS, installing. If OpenBLAS is installed please use the OPENBLAS_DIR parameter to pass the path")
+        if (${OPENBLAS_DIR} STREQUAL ${OPENBLAS_DEFAULT_DIR})
+            message("Installing OpenBLAS")
+            execute_process(COMMAND ${TOOLS_DIR}/download_openBLAS.sh ${OPENBLAS_VERSION})
+        else()
+            message(FATAL_ERROR "Can't find OpenBLAS in the supplied directory")
+        endif()
+    endif()
+
+    add_library(${OPENBLAS_LIB} SHARED IMPORTED)
+    set_target_properties(${OPENBLAS_LIB} PROPERTIES IMPORTED_LOCATION ${OPENBLAS_DIR}/installed/lib/libopenblas.a)
+    list(APPEND LIBS ${OPENBLAS_LIB})
+    target_include_directories(${OPENBLAS_LIB} INTERFACE ${OPENBLAS_DIR}/installed/include)
 endif()
 
 ###########
@@ -239,7 +265,7 @@ set(INPUT_PARSERS_DIR input_parsers)
 include(ProcessorCount)
 ProcessorCount(CTEST_NTHREADS)
 if(CTEST_NTHREADS EQUAL 0)
-  set(CTEST_NTHREADS 1)
+    set(CTEST_NTHREADS 1)
 endif()
 
 # --------------- set build type ----------------------------
@@ -247,20 +273,20 @@ set(BUILD_TYPES Release Debug MinSizeRel RelWithDebInfo)
 
 # Set the default build type to Production
 if(NOT CMAKE_BUILD_TYPE)
-  set(CMAKE_BUILD_TYPE
-      Release CACHE STRING "Options are: Release Debug MinSizeRel RelWithDebInfo" FORCE)
-  # Provide drop down menu options in cmake-gui
-  set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
+    set(CMAKE_BUILD_TYPE
+            Release CACHE STRING "Options are: Release Debug MinSizeRel RelWithDebInfo" FORCE)
+    # Provide drop down menu options in cmake-gui
+    set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 endif()
 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 
 #-------------------------set code coverage----------------------------------#
 # Allow coverage only in debug mode only in gcc
 if(CODE_COVERAGE AND CMAKE_CXX_COMPILER_ID MATCHES "GNU" AND CMAKE_BUILD_TYPE MATCHES Debug)
-  message(STATUS "Building with code coverage")
-  set(COVERAGE_COMPILER_FLAGS "-g -O0 --coverage" CACHE INTERNAL "")
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${COVERAGE_COMPILER_FLAGS}")
-  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage")
+    message(STATUS "Building with code coverage")
+    set(COVERAGE_COMPILER_FLAGS "-g -O0 --coverage" CACHE INTERNAL "")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${COVERAGE_COMPILER_FLAGS}")
+    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} --coverage")
 endif()
 
 # We build a static library that is the core of the project, the link it to the
@@ -273,7 +299,7 @@ set(MARABOU_EXE Marabou${CMAKE_EXECUTABLE_SUFFIX})
 add_executable(${MARABOU_EXE} "${ENGINE_DIR}/main.cpp")
 set(MARABOU_EXE_PATH "${BIN_DIR}/${MARABOU_EXE}")
 add_custom_command(TARGET ${MARABOU_EXE} POST_BUILD
-    COMMAND ${CMAKE_COMMAND} -E copy $<TARGET_FILE:${MARABOU_EXE}> ${MARABOU_EXE_PATH} )
+        COMMAND ${CMAKE_COMMAND} -E copy $<TARGET_FILE:${MARABOU_EXE}> ${MARABOU_EXE_PATH} )
 
 set(MPS_PARSER_PATH "${BIN_DIR}/${MPS_PARSER}")
 
@@ -314,10 +340,10 @@ find_package(Threads REQUIRED)
 list(APPEND LIBS Threads::Threads)
 
 if (BUILD_STATIC_MARABOU)
-  # build a static library
-  target_link_libraries(${MARABOU_LIB} ${LIBS} -static)
+    # build a static library
+    target_link_libraries(${MARABOU_LIB} ${LIBS} -static)
 else()
-  target_link_libraries(${MARABOU_LIB} ${LIBS})
+    target_link_libraries(${MARABOU_LIB} ${LIBS})
 endif()
 
 target_include_directories(${MARABOU_LIB} PRIVATE ${LIBS_INCLUDES})
@@ -347,10 +373,10 @@ endif()
 set(PYTHON32 FALSE)
 if(${BUILD_PYTHON})
     execute_process(COMMAND "${PYTHON_EXECUTABLE}" "-c"
-        "import struct; print(struct.calcsize('@P'));"
-    RESULT_VARIABLE _PYTHON_SUCCESS
-    OUTPUT_VARIABLE PYTHON_SIZEOF_VOID_P
-    ERROR_VARIABLE _PYTHON_ERROR_VALUE)
+            "import struct; print(struct.calcsize('@P'));"
+            RESULT_VARIABLE _PYTHON_SUCCESS
+            OUTPUT_VARIABLE PYTHON_SIZEOF_VOID_P
+            ERROR_VARIABLE _PYTHON_ERROR_VALUE)
     # message("PYTHON SIZEOF VOID p ${PYTHON_SIZEOF_VOID_P}")
     if (PYTHON_SIZEOF_VOID_P EQUAL 4 AND NOT ${FORCE_PYTHON_BUILD})
         set(PYTHON32 TRUE)
@@ -370,8 +396,8 @@ endif()
 
 # Actually build Python
 if (${BUILD_PYTHON})
-   set(PYBIND11_VERSION 2.10.4)
-   set(PYBIND11_DIR "${TOOLS_DIR}/pybind11-${PYBIND11_VERSION}")
+    set(PYBIND11_VERSION 2.10.4)
+    set(PYBIND11_DIR "${TOOLS_DIR}/pybind11-${PYBIND11_VERSION}")
 
     # This is suppose to set the PYTHON_EXECUTABLE variable
     # First try to find the default python version
@@ -383,7 +409,7 @@ if (${BUILD_PYTHON})
 
     if (NOT EXISTS ${PYBIND11_DIR})
         message("didnt find pybind, getting it")
-	execute_process(COMMAND ${TOOLS_DIR}/download_pybind11.${SCRIPT_EXTENSION} ${PYBIND11_VERSION})
+        execute_process(COMMAND ${TOOLS_DIR}/download_pybind11.${SCRIPT_EXTENSION} ${PYBIND11_VERSION})
     endif()
     add_subdirectory(${PYBIND11_DIR})
 
@@ -394,7 +420,7 @@ if (${BUILD_PYTHON})
     target_include_directories(${MARABOU_PY} PRIVATE ${LIBS_INCLUDES})
 
     set_target_properties(${MARABOU_PY} PROPERTIES
-        LIBRARY_OUTPUT_DIRECTORY ${PYTHON_LIBRARY_OUTPUT_DIRECTORY})
+            LIBRARY_OUTPUT_DIRECTORY ${PYTHON_LIBRARY_OUTPUT_DIRECTORY})
     if(NOT MSVC)
         target_compile_options(${MARABOU_LIB} PRIVATE -fPIC ${RELEASE_FLAGS})
     endif()
@@ -425,8 +451,8 @@ target_compile_options(${MARABOU_TEST_LIB} PRIVATE ${CXXTEST_FLAGS})
 add_custom_target(build-tests ALL)
 
 add_custom_target(check
-      COMMAND ctest --output-on-failure -j${CTEST_NTHREADS} $$ARGS
-      DEPENDS build-tests build_input_parsers ${MARABOU_EXE})
+        COMMAND ctest --output-on-failure -j${CTEST_NTHREADS} $$ARGS
+        DEPENDS build-tests build_input_parsers ${MARABOU_EXE})
 
 # Decide which tests to run and execute
 set(TESTS_TO_RUN "")
@@ -452,33 +478,33 @@ if (NOT ${TESTS_TO_RUN} STREQUAL "")
     # make ctest verbose
     set(CTEST_OUTPUT_ON_FAILURE 1)
     add_custom_command(
-        TARGET build-tests
-        POST_BUILD
-        COMMAND ctest --output-on-failure  -L "\"(${TESTS_TO_RUN})\"" -j${CTEST_NTHREADS} $$ARGS
+            TARGET build-tests
+            POST_BUILD
+            COMMAND ctest --output-on-failure  -L "\"(${TESTS_TO_RUN})\"" -j${CTEST_NTHREADS} $$ARGS
     )
 endif()
 
 if (${BUILD_PYTHON} AND ${RUN_PYTHON_TEST})
     if (MSVC)
         add_custom_command(
-            TARGET build-tests
-            POST_BUILD
-            COMMAND cp ${PYTHON_API_DIR}/Release/* ${PYTHON_API_DIR}
+                TARGET build-tests
+                POST_BUILD
+                COMMAND cp ${PYTHON_API_DIR}/Release/* ${PYTHON_API_DIR}
         )
     endif()
 
     add_custom_command(
-        TARGET build-tests
-        POST_BUILD
-        COMMAND ${PYTHON_EXECUTABLE} -m pytest ${PYTHON_API_DIR}/test
+            TARGET build-tests
+            POST_BUILD
+            COMMAND ${PYTHON_EXECUTABLE} -m pytest ${PYTHON_API_DIR}/test
     )
 endif()
 
 # Add the input parsers
 add_custom_target(build_input_parsers)
 add_dependencies(build_input_parsers ${MPS_PARSER} ${ACAS_PARSER}
-    ${BERKELEY_PARSER})
+        ${BERKELEY_PARSER})
 
 add_subdirectory(${SRC_DIR})
 add_subdirectory(${TOOLS_DIR})
-add_subdirectory(${REGRESS_DIR})
+add_subdirectory(${REGRESS_DIR})
\ No newline at end of file
diff --git a/maraboupy/MarabouCore.cpp b/maraboupy/MarabouCore.cpp
index 1b81804703..95173ada7f 100644
--- a/maraboupy/MarabouCore.cpp
+++ b/maraboupy/MarabouCore.cpp
@@ -296,6 +296,7 @@ struct MarabouOptions
         , _timeoutInSeconds( Options::get()->getInt( Options::TIMEOUT ) )
         , _splitThreshold( Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) )
         , _numSimulations( Options::get()->getInt( Options::NUMBER_OF_SIMULATIONS ) )
+        , _attackTimeout( Options::get()->getInt( Options::ATTACK_TIMEOUT ) )
         , _performLpTighteningAfterSplit(
               Options::get()->getBool( Options::PERFORM_LP_TIGHTENING_AFTER_SPLIT ) )
         , _timeoutFactor( Options::get()->getFloat( Options::TIMEOUT_FACTOR ) )
@@ -311,7 +312,8 @@ struct MarabouOptions
         , _milpTighteningString(
               Options::get()->getString( Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE ).ascii() )
         , _lpSolverString( Options::get()->getString( Options::LP_SOLVER ).ascii() )
-        , _produceProofs( Options::get()->getBool( Options::PRODUCE_PROOFS ) ){};
+        , _produceProofs( Options::get()->getBool( Options::PRODUCE_PROOFS ) )
+        , _runAttack( Options::get()->getBool( Options::RUN_ATTACK ) ){};
 
     void setOptions()
     {
@@ -356,6 +358,7 @@ struct MarabouOptions
     bool _dumpBounds;
     bool _performLpTighteningAfterSplit;
     bool _produceProofs;
+    bool _runAttack;
     unsigned _numWorkers;
     unsigned _numBlasThreads;
     unsigned _initialTimeout;
@@ -365,6 +368,7 @@ struct MarabouOptions
     unsigned _timeoutInSeconds;
     unsigned _splitThreshold;
     unsigned _numSimulations;
+    unsigned _attackTimeout;
     float _timeoutFactor;
     float _preprocessorBoundTolerance;
     float _milpSolverTimeout;
diff --git a/src/common/Debug.h b/src/common/Debug.h
index 55dfda4a92..01bcb30288 100644
--- a/src/common/Debug.h
+++ b/src/common/Debug.h
@@ -26,6 +26,8 @@
 #define DEBUG( x )
 #endif
 
+#undef LOG
+
 #ifndef NDEBUG
 #define LOG( x, f, y, ... )                                                                        \
     {                                                                                              \
diff --git a/src/configuration/GlobalConfiguration.cpp b/src/configuration/GlobalConfiguration.cpp
index c70ce013ef..e627fa4ee1 100644
--- a/src/configuration/GlobalConfiguration.cpp
+++ b/src/configuration/GlobalConfiguration.cpp
@@ -117,6 +117,12 @@ const bool GlobalConfiguration::WRITE_JSON_PROOF = false;
 const unsigned GlobalConfiguration::BACKWARD_BOUND_PROPAGATION_DEPTH = 3;
 const unsigned GlobalConfiguration::MAX_ROUNDS_OF_BACKWARD_ANALYSIS = 10;
 
+const GlobalConfiguration::PdgBoundType GlobalConfiguration::PGD_BOUND_TYPE =
+    GlobalConfiguration::PGD_INPUT;
+const unsigned GlobalConfiguration::PGD_DEFAULT_NUM_ITER = 100;
+const unsigned GlobalConfiguration::PGD_NUM_RESTARTS = 4;
+const double GlobalConfiguration::PGD_INPUT_RANGE = 1000;
+
 #ifdef ENABLE_GUROBI
 const unsigned GlobalConfiguration::GUROBI_NUMBER_OF_THREADS = 1;
 const bool GlobalConfiguration::GUROBI_LOGGING = false;
@@ -141,6 +147,8 @@ const bool GlobalConfiguration::ONNX_PARSER_LOGGING = false;
 const bool GlobalConfiguration::SOI_LOGGING = false;
 const bool GlobalConfiguration::SCORE_TRACKER_LOGGING = false;
 const bool GlobalConfiguration::CEGAR_LOGGING = false;
+const bool GlobalConfiguration::CUSTOM_DNN_LOGGING = false;
+const bool GlobalConfiguration::PGD_LOGGING = false;
 
 const bool GlobalConfiguration::USE_SMART_FIX = false;
 const bool GlobalConfiguration::USE_LEAST_FIX = false;
diff --git a/src/configuration/GlobalConfiguration.h b/src/configuration/GlobalConfiguration.h
index c89c1d54b3..01fc927102 100644
--- a/src/configuration/GlobalConfiguration.h
+++ b/src/configuration/GlobalConfiguration.h
@@ -257,6 +257,16 @@ class GlobalConfiguration
      */
     static const unsigned MAX_ROUNDS_OF_BACKWARD_ANALYSIS;
 
+    enum PdgBoundType {
+        PGD_INPUT = 0,
+        PGD_OUTPUT = 1
+    };
+    static const PdgBoundType PGD_BOUND_TYPE;
+    static const unsigned PGD_DEFAULT_NUM_ITER;
+    static const unsigned PGD_NUM_RESTARTS;
+    static const double PGD_INPUT_RANGE;
+
+
 #ifdef ENABLE_GUROBI
     /*
       The number of threads Gurobi spawns
@@ -286,6 +296,8 @@ class GlobalConfiguration
     static const bool SOI_LOGGING;
     static const bool SCORE_TRACKER_LOGGING;
     static const bool CEGAR_LOGGING;
+    static const bool CUSTOM_DNN_LOGGING;
+    static const bool PGD_LOGGING;
 };
 
 #endif // __GlobalConfiguration_h__
diff --git a/src/configuration/OptionParser.cpp b/src/configuration/OptionParser.cpp
index cd94bbc394..58c95bb2b1 100644
--- a/src/configuration/OptionParser.cpp
+++ b/src/configuration/OptionParser.cpp
@@ -137,6 +137,14 @@ void OptionParser::initialize()
         boost::program_options::bool_switch( &( ( *_boolOptions )[Options::PRODUCE_PROOFS] ) )
             ->default_value( ( *_boolOptions )[Options::PRODUCE_PROOFS] ),
         "Produce proofs of UNSAT and check them" )
+#ifdef BUILD_TORCH
+    (
+            "run-attack",
+            boost::program_options::bool_switch( &( ( *_boolOptions )[Options::RUN_ATTACK] ) )
+                ->default_value( ( *_boolOptions )[Options::RUN_ATTACK] ),
+            "Enable PGD adversarial attack run" )
+#endif
+
 #ifdef ENABLE_GUROBI
 #endif // ENABLE_GUROBI
         ;
diff --git a/src/configuration/Options.cpp b/src/configuration/Options.cpp
index bf3b9b913a..fe1a432cb4 100644
--- a/src/configuration/Options.cpp
+++ b/src/configuration/Options.cpp
@@ -55,6 +55,8 @@ void Options::initializeDefaultValues()
     _boolOptions[DEBUG_ASSIGNMENT] = false;
     _boolOptions[PRODUCE_PROOFS] = false;
     _boolOptions[DO_NOT_MERGE_CONSECUTIVE_WEIGHTED_SUM_LAYERS] = false;
+    _boolOptions[RUN_ATTACK] = false;
+
 
     /*
       Int options
@@ -71,6 +73,7 @@ void Options::initializeDefaultValues()
     _intOptions[SEED] = 1;
     _intOptions[NUM_BLAS_THREADS] = 1;
     _intOptions[NUM_CONSTRAINTS_TO_REFINE_INC_LIN] = 30;
+    _intOptions[ATTACK_TIMEOUT] = 60;
 
     /*
       Float options
diff --git a/src/configuration/Options.h b/src/configuration/Options.h
index 4dd4f31fd5..a615286afa 100644
--- a/src/configuration/Options.h
+++ b/src/configuration/Options.h
@@ -83,6 +83,9 @@ class Options
         // logically-consecutive weighted sum layers into a single
         // weighted sum layer, to reduce the number of variables
         DO_NOT_MERGE_CONSECUTIVE_WEIGHTED_SUM_LAYERS,
+
+        // Run adversarial attack before preprocess if the flag is true.
+        RUN_ATTACK,
     };
 
     enum IntOptions {
@@ -115,6 +118,9 @@ class Options
 
         // Maximal number of constraints to refine in incremental linearization
         NUM_CONSTRAINTS_TO_REFINE_INC_LIN,
+
+        // Adversarial attack timeout in seconds
+        ATTACK_TIMEOUT,
     };
 
     enum FloatOptions {
diff --git a/src/engine/CMakeLists.txt b/src/engine/CMakeLists.txt
index 707c6e1759..afe7d2ad6c 100644
--- a/src/engine/CMakeLists.txt
+++ b/src/engine/CMakeLists.txt
@@ -2,6 +2,7 @@ file(GLOB SRCS "*.cpp")
 file(GLOB HEADERS "*.h")
 
 
+
 target_sources(${MARABOU_LIB} PRIVATE ${SRCS})
 target_include_directories(${MARABOU_LIB} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}")
 
diff --git a/src/engine/CustomDNN.cpp b/src/engine/CustomDNN.cpp
new file mode 100644
index 0000000000..2744746dfc
--- /dev/null
+++ b/src/engine/CustomDNN.cpp
@@ -0,0 +1,275 @@
+#include "CustomDNN.h"
+#include "Vector.h"
+#ifdef BUILD_TORCH
+
+CustomRelu::CustomRelu( const NLR::NetworkLevelReasoner *nlr, unsigned layerIndex )
+    : _networkLevelReasoner( nlr )
+    , _reluLayerIndex( layerIndex )
+{
+}
+
+torch::Tensor CustomRelu::forward( torch::Tensor x ) const
+{
+    return CustomReluFunction::apply( x, _networkLevelReasoner, _reluLayerIndex );
+}
+
+CustomMaxPool::CustomMaxPool( const NLR::NetworkLevelReasoner *nlr, unsigned layerIndex )
+    : _networkLevelReasoner( nlr )
+    , _maxLayerIndex( layerIndex )
+{
+}
+
+torch::Tensor CustomMaxPool::forward( torch::Tensor x ) const
+{
+    return CustomMaxPoolFunction::apply( x, _networkLevelReasoner, _maxLayerIndex );
+}
+
+void CustomDNN::setWeightsAndBiases( torch::nn::Linear &linearLayer,
+                                     const NLR::Layer *layer,
+                                     unsigned sourceLayer,
+                                     unsigned inputSize,
+                                     unsigned outputSize )
+{
+    Vector<Vector<float>> layerWeights( outputSize, Vector<float>( inputSize ) );
+    Vector<float> layerBiases( outputSize );
+
+    // Fetch weights and biases from networkLevelReasoner
+    for ( unsigned j = 0; j < outputSize; j++ )
+    {
+        for ( unsigned k = 0; k < inputSize; k++ )
+        {
+            double weight_value = layer->getWeight( sourceLayer, k, j );
+            layerWeights[j][k] = static_cast<float>( weight_value );
+        }
+        double bias_value = layer->getBias( j );
+        layerBiases[j] = static_cast<float>( bias_value );
+    }
+
+    Vector<float> flattenedWeights;
+    for ( const auto &weight : layerWeights )
+    {
+        for ( const auto &w : weight )
+        {
+            flattenedWeights.append( w );
+        }
+    }
+
+    torch::Tensor weightTensor = torch::tensor( flattenedWeights.getContainer(), torch::kFloat )
+                                     .view( { outputSize, inputSize } );
+    torch::Tensor biasTensor = torch::tensor( layerBiases.getContainer(), torch::kFloat );
+
+    torch::NoGradGuard no_grad;
+    linearLayer->weight.set_( weightTensor );
+    linearLayer->bias.set_( biasTensor );
+}
+
+void CustomDNN::weightedSum( unsigned i, const NLR::Layer *layer )
+{
+    unsigned sourceLayer = i - 1;
+    const NLR::Layer *prevLayer = _networkLevelReasoner->getLayer( sourceLayer );
+    unsigned inputSize = prevLayer->getSize();
+    unsigned outputSize = layer->getSize();
+
+    if ( outputSize > 0 )
+    {
+        auto linearLayer = torch::nn::Linear( torch::nn::LinearOptions( inputSize, outputSize ) );
+        _linearLayers.append( linearLayer );
+
+        setWeightsAndBiases( linearLayer, layer, sourceLayer, inputSize, outputSize );
+
+        register_module( "linear" + std::to_string( i ), linearLayer );
+    }
+}
+
+
+CustomDNN::CustomDNN( const NLR::NetworkLevelReasoner *nlr )
+{
+    CUSTOM_DNN_LOG( "----- Construct Custom Network -----" );
+    _networkLevelReasoner = nlr;
+    _numberOfLayers = _networkLevelReasoner->getNumberOfLayers();
+    for ( unsigned i = 0; i < _numberOfLayers; i++ )
+    {
+        const NLR::Layer *layer = _networkLevelReasoner->getLayer( i );
+        _layerSizes.append( layer->getSize() );
+        NLR::Layer::Type layerType = layer->getLayerType();
+        _layersOrder.append( layerType );
+        switch ( layerType )
+        {
+        case NLR::Layer::INPUT:
+            break;
+        case NLR::Layer::WEIGHTED_SUM:
+            weightedSum( i, layer );
+            break;
+        case NLR::Layer::RELU:
+        {
+            auto reluLayer = std::make_shared<CustomRelu>( _networkLevelReasoner, i );
+            _reluLayers.append( reluLayer );
+            register_module( "ReLU" + std::to_string( i ), reluLayer );
+            break;
+        }
+        case NLR::Layer::LEAKY_RELU:
+        {
+            auto reluLayer = torch::nn::LeakyReLU( torch::nn::LeakyReLUOptions() );
+            _leakyReluLayers.append( reluLayer );
+            register_module( "leakyReLU" + std::to_string( i ), reluLayer );
+            break;
+        }
+        case NLR::Layer::MAX:
+        {
+            auto maxPoolLayer = std::make_shared<CustomMaxPool>( _networkLevelReasoner, i );
+            _maxPoolLayers.append( maxPoolLayer );
+            register_module( "maxPool" + std::to_string( i ), maxPoolLayer );
+            break;
+        }
+        case NLR::Layer::SIGMOID:
+        {
+            auto sigmoidLayer = torch::nn::Sigmoid();
+            _sigmoidLayers.append( sigmoidLayer );
+            register_module( "sigmoid" + std::to_string( i ), sigmoidLayer );
+            break;
+        }
+        default:
+            CUSTOM_DNN_LOG( "Unsupported layer type\n" );
+            throw MarabouError( MarabouError::DEBUGGING_ERROR );
+        }
+    }
+}
+
+torch::Tensor CustomDNN::forward( torch::Tensor x )
+{
+    unsigned linearIndex = 0;
+    unsigned reluIndex = 0;
+    unsigned maxPoolIndex = 0;
+    unsigned leakyReluIndex = 0;
+    unsigned sigmoidIndex = 0;
+    for ( unsigned i = 0; i < _numberOfLayers; i++ )
+    {
+        const NLR::Layer::Type layerType = _layersOrder[i];
+        switch ( layerType )
+        {
+        case NLR::Layer::INPUT:
+            break;
+        case NLR::Layer::WEIGHTED_SUM:
+            x = _linearLayers[linearIndex]->forward( x );
+            linearIndex++;
+            break;
+        case NLR::Layer::RELU:
+            x = _reluLayers[reluIndex]->forward( x );
+            reluIndex++;
+            break;
+        case NLR::Layer::MAX:
+            x = _maxPoolLayers[maxPoolIndex]->forward( x );
+            maxPoolIndex++;
+            break;
+        case NLR::Layer::LEAKY_RELU:
+            x = _leakyReluLayers[leakyReluIndex]->forward( x );
+            leakyReluIndex++;
+            break;
+        case NLR::Layer::SIGMOID:
+            x = _sigmoidLayers[sigmoidIndex]->forward( x );
+            sigmoidIndex++;
+            break;
+        default:
+            CUSTOM_DNN_LOG( "Unsupported layer type\n" );
+            throw MarabouError( MarabouError::DEBUGGING_ERROR );
+            break;
+        }
+    }
+    return x;
+}
+
+torch::Tensor CustomReluFunction::forward( torch::autograd::AutogradContext *ctx,
+                                           torch::Tensor x,
+                                           const NLR::NetworkLevelReasoner *nlr,
+                                           unsigned int layerIndex )
+{
+    ctx->save_for_backward( { x } );
+
+    const NLR::Layer *layer = nlr->getLayer( layerIndex );
+    torch::Tensor reluOutputs = torch::zeros( { 1, layer->getSize() } );
+    torch::Tensor reluGradients = torch::zeros( { 1, layer->getSize() } );
+
+    for ( unsigned neuron = 0; neuron < layer->getSize(); ++neuron )
+    {
+        auto sources = layer->getActivationSources( neuron );
+        ASSERT( sources.size() == 1 );
+        const NLR::NeuronIndex &sourceNeuron = sources.back();
+        int index = static_cast<int>( sourceNeuron._neuron );
+        reluOutputs.index_put_( { 0, static_cast<int>( neuron ) },
+                                torch::clamp_min( x.index( { 0, index } ), 0 ) );
+        reluGradients.index_put_( { 0, static_cast<int>( neuron ) }, x.index( { 0, index } ) > 0 );
+    }
+
+    ctx->saved_data["reluGradients"] = reluGradients;
+
+    return reluOutputs;
+}
+
+std::vector<torch::Tensor> CustomReluFunction::backward( torch::autograd::AutogradContext *ctx,
+                                                         std::vector<torch::Tensor> grad_output )
+{
+    auto saved = ctx->get_saved_variables();
+    auto input = saved[0];
+
+    auto reluGradients = ctx->saved_data["reluGradients"].toTensor();
+    auto grad_input = grad_output[0] * reluGradients[0];
+
+    return { grad_input, torch::Tensor(), torch::Tensor() };
+}
+
+torch::Tensor CustomMaxPoolFunction::forward( torch::autograd::AutogradContext *ctx,
+                                              torch::Tensor x,
+                                              const NLR::NetworkLevelReasoner *nlr,
+                                              unsigned int layerIndex )
+{
+    ctx->save_for_backward( { x } );
+
+    const NLR::Layer *layer = nlr->getLayer( layerIndex );
+    torch::Tensor maxOutputs = torch::zeros( { 1, layer->getSize() } );
+    torch::Tensor argMaxOutputs = torch::zeros( { 1, layer->getSize() }, torch::kInt64 );
+
+    for ( unsigned neuron = 0; neuron < layer->getSize(); ++neuron )
+    {
+        auto sources = layer->getActivationSources( neuron );
+        torch::Tensor sourceValues = torch::zeros( sources.size(), torch::kFloat );
+        torch::Tensor sourceIndices = torch::zeros( sources.size() );
+
+        for ( int i = sources.size() - 1; i >= 0; --i )
+        {
+            const NLR::NeuronIndex &activationNeuron = sources.back();
+            int index = static_cast<int>( activationNeuron._neuron );
+            sources.popBack();
+            sourceValues.index_put_( { i }, x.index( { 0, index } ) );
+            sourceIndices.index_put_( { i }, index );
+        }
+
+        maxOutputs.index_put_( { 0, static_cast<int>( neuron ) }, torch::max( sourceValues ) );
+        argMaxOutputs.index_put_( { 0, static_cast<int>( neuron ) },
+                                  sourceIndices.index( { torch::argmax( sourceValues ) } ) );
+    }
+
+    ctx->saved_data["argMaxOutputs"] = argMaxOutputs;
+
+    return maxOutputs;
+}
+
+std::vector<torch::Tensor> CustomMaxPoolFunction::backward( torch::autograd::AutogradContext *ctx,
+                                                            std::vector<torch::Tensor> grad_output )
+{
+    auto saved = ctx->get_saved_variables();
+    auto input = saved[0];
+
+    auto grad_input = torch::zeros_like( input );
+
+    auto indices = ctx->saved_data["argMaxOutputs"].toTensor();
+
+    grad_input[0].index_add_( 0, indices.flatten(), grad_output[0].flatten() );
+
+    return { grad_input, torch::Tensor(), torch::Tensor() };
+}
+
+const Vector<unsigned> &CustomDNN::getLayerSizes() const
+{
+    return _layerSizes;
+}
+#endif
\ No newline at end of file
diff --git a/src/engine/CustomDNN.h b/src/engine/CustomDNN.h
new file mode 100644
index 0000000000..d78d4be5d4
--- /dev/null
+++ b/src/engine/CustomDNN.h
@@ -0,0 +1,99 @@
+#ifdef BUILD_TORCH
+#ifndef __CustomDNN_h__
+#define __CustomDNN_h__
+
+#undef Warning
+#include <torch/torch.h>
+
+#include "NetworkLevelReasoner.h"
+#include <vector>
+
+#define CUSTOM_DNN_LOG( x, ... )                                                                   \
+    LOG( GlobalConfiguration::CUSTOM_DNN_LOGGING, "customDNN: %s\n", x )
+
+/*
+  Custom differentiation function for ReLU, implementing the forward and backward propagation
+  for the ReLU operation according to each variable's source layer as defined in the nlr.
+*/
+class CustomReluFunction : public torch::autograd::Function<CustomReluFunction>
+{
+public:
+    static torch::Tensor forward( torch::autograd::AutogradContext *ctx,
+                                  torch::Tensor x,
+                                  const NLR::NetworkLevelReasoner *nlr,
+                                  unsigned layerIndex );
+
+    static std::vector<torch::Tensor> backward( torch::autograd::AutogradContext *ctx,
+                                                std::vector<torch::Tensor> grad_output );
+};
+
+class CustomRelu : public torch::nn::Module
+{
+public:
+    CustomRelu( const NLR::NetworkLevelReasoner *nlr, unsigned layerIndex );
+    torch::Tensor forward( torch::Tensor x ) const;
+
+private:
+    const NLR::NetworkLevelReasoner *_networkLevelReasoner;
+    unsigned _reluLayerIndex;
+};
+
+/*
+  Custom differentiation function for max pooling, implementing the forward and backward propagation
+  for the max pooling operation according to each variable's source layer as defined in the nlr.
+*/
+class CustomMaxPoolFunction : public torch::autograd::Function<CustomMaxPoolFunction>
+{
+public:
+    static torch::Tensor forward( torch::autograd::AutogradContext *ctx,
+                                  torch::Tensor x,
+                                  const NLR::NetworkLevelReasoner *nlr,
+                                  unsigned layerIndex );
+
+    static std::vector<torch::Tensor> backward( torch::autograd::AutogradContext *ctx,
+                                                std::vector<torch::Tensor> grad_output );
+};
+
+class CustomMaxPool : public torch::nn::Module
+{
+public:
+    CustomMaxPool( const NLR::NetworkLevelReasoner *nlr, unsigned layerIndex );
+    torch::Tensor forward( torch::Tensor x ) const;
+
+private:
+    const NLR::NetworkLevelReasoner *_networkLevelReasoner;
+    unsigned _maxLayerIndex;
+};
+
+/*
+ torch implementation of the network according to the nlr.
+ */
+class CustomDNN : public torch::nn::Module
+{
+public:
+    static void setWeightsAndBiases( torch::nn::Linear &linearLayer,
+                                     const NLR::Layer *layer,
+                                     unsigned sourceLayer,
+                                     unsigned inputSize,
+                                     unsigned outputSize );
+    void weightedSum( unsigned i, const NLR::Layer *layer );
+    explicit CustomDNN( const NLR::NetworkLevelReasoner *networkLevelReasoner );
+
+    torch::Tensor forward( torch::Tensor x );
+    const Vector<unsigned> &getLayerSizes() const;
+
+private:
+    const NLR::NetworkLevelReasoner *_networkLevelReasoner;
+    Vector<unsigned> _layerSizes;
+    Vector<std::shared_ptr<CustomRelu>> _reluLayers;
+    Vector<torch::nn::LeakyReLU> _leakyReluLayers;
+    Vector<torch::nn::Sigmoid> _sigmoidLayers;
+    Vector<std::shared_ptr<CustomMaxPool>> _maxPoolLayers;
+    Vector<torch::nn::Linear> _linearLayers;
+    Vector<NLR::Layer::Type> _layersOrder;
+    unsigned _numberOfLayers;
+};
+
+
+#endif // __CustomDNN_h__
+#endif
\ No newline at end of file
diff --git a/src/engine/DnCManager.cpp b/src/engine/DnCManager.cpp
index 06f684dc43..44fa68ebdb 100644
--- a/src/engine/DnCManager.cpp
+++ b/src/engine/DnCManager.cpp
@@ -154,7 +154,13 @@ void DnCManager::solve()
     // Preprocess the input query and create an engine for each of the threads
     if ( !createEngines( numWorkers ) )
     {
-        _exitCode = DnCManager::UNSAT;
+        if ( _baseEngine->getExitCode() == Engine::ExitCode::SAT )
+        {
+            _exitCode = DnCManager::SAT;
+            _engineWithSATAssignment = _baseEngine;
+        }
+        else
+            _exitCode = DnCManager::UNSAT;
         return;
     }
 
diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
index 0fd7dfa688..447f76381c 100644
--- a/src/engine/Engine.cpp
+++ b/src/engine/Engine.cpp
@@ -14,11 +14,15 @@
  ** [[ Add lengthier description here ]]
  **/
 
-#include "Engine.h"
+#ifdef BUILD_TORCH
+#undef Warning
+#include <torch/torch.h>
+#endif
 
 #include "AutoConstraintMatrixAnalyzer.h"
 #include "Debug.h"
 #include "DisjunctionConstraint.h"
+#include "Engine.h"
 #include "EngineState.h"
 #include "InfeasibleQueryException.h"
 #include "InputQuery.h"
@@ -26,6 +30,7 @@
 #include "MalformedBasisException.h"
 #include "MarabouError.h"
 #include "NLRError.h"
+#include "PGD.h"
 #include "PiecewiseLinearConstraint.h"
 #include "Preprocessor.h"
 #include "TableauRow.h"
@@ -69,6 +74,9 @@ Engine::Engine()
     , _milpSolverBoundTighteningType( Options::get()->getMILPSolverBoundTighteningType() )
     , _sncMode( false )
     , _queryId( "" )
+#ifdef BUILD_TORCH
+    , _pgdAttack( nullptr )
+#endif
     , _produceUNSATProofs( Options::get()->getBool( Options::PRODUCE_PROOFS ) )
     , _groundBoundManager( _context )
     , _UNSATCertificate( NULL )
@@ -1439,6 +1447,47 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess )
         if ( _verbosity > 1 )
             printInputBounds( inputQuery );
         initializeNetworkLevelReasoning();
+        if ( _networkLevelReasoner )
+#ifdef BUILD_TORCH
+            if ( Options::get()->getBool( ( Options::RUN_ATTACK ) ) )
+            {
+                try
+                {
+                    std::string timeString = TimeUtils::now().ascii();
+                    ENGINE_LOG( Stringf( "Adversarial attack start time: %s\n", timeString.c_str() )
+                                    .ascii() );
+
+                    _pgdAttack = std::make_unique<PGDAttack>( _networkLevelReasoner );
+                    if ( _pgdAttack->runAttack() )
+                    {
+                        timeString = TimeUtils::now().ascii();
+                        ENGINE_LOG(
+                            Stringf( "Adversarial attack end time: %s\n", timeString.c_str() )
+                                .ascii() );
+                        _exitCode = Engine::SAT;
+                        _isAttackSuccessful = true;
+                        return false;
+                    }
+                    timeString = TimeUtils::now().ascii();
+                    ENGINE_LOG( Stringf( "Adversarial attack end time: %s\n", timeString.c_str() )
+                                    .ascii() );
+                }
+
+                catch ( MarabouError &e )
+                {
+                    std::string timeString = TimeUtils::now().ascii();
+                    ENGINE_LOG( Stringf( "Caught a MarabouError. Code: %u. Message: %s Adversarial "
+                                         "attack end time: %s\n",
+                                         e.getCode(),
+                                         e.getUserMessage(),
+                                         timeString.c_str() )
+                                    .ascii() );
+                }
+            }
+#endif
+        {
+        }
+
         if ( preprocess )
         {
             performSymbolicBoundTightening( &( *_preprocessedQuery ) );
@@ -1754,11 +1803,22 @@ void Engine::extractSolution( InputQuery &inputQuery, Preprocessor *preprocessor
             variable = preprocessorInUse->getNewIndex( variable );
 
             // Finally, set the assigned value
-            inputQuery.setSolutionValue( i, _tableau->getValue( variable ) );
+#ifdef BUILD_TORCH
+
+            if ( _isAttackSuccessful )
+                inputQuery.setSolutionValue( i, _pgdAttack->getAssignment( variable ) );
+            else
+                inputQuery.setSolutionValue( i, _tableau->getValue( variable ) );
+#endif
         }
         else
         {
-            inputQuery.setSolutionValue( i, _tableau->getValue( i ) );
+#ifdef BUILD_TORCH
+            if ( _isAttackSuccessful )
+                inputQuery.setSolutionValue( i, _pgdAttack->getAssignment( i ) );
+            else
+                inputQuery.setSolutionValue( i, _tableau->getValue( i ) );
+#endif
         }
     }
 
diff --git a/src/engine/Engine.h b/src/engine/Engine.h
index feb9ac1279..291975c159 100644
--- a/src/engine/Engine.h
+++ b/src/engine/Engine.h
@@ -51,6 +51,7 @@
 #include <atomic>
 #include <context/context.h>
 
+class PGDAttack;
 
 #ifdef _WIN32
 #undef ERROR
@@ -536,6 +537,11 @@ class Engine
 
     LinearExpression _heuristicCost;
 
+#ifdef BUILD_TORCH
+    std::unique_ptr<PGDAttack> _pgdAttack;
+    bool _isAttackSuccessful = false;
+#endif
+
     /*
       Perform a simplex step: compute the cost function, pick the
       entering and leaving variables and perform a pivot.
diff --git a/src/engine/Marabou.cpp b/src/engine/Marabou.cpp
index 2d2814cca3..053fa85380 100644
--- a/src/engine/Marabou.cpp
+++ b/src/engine/Marabou.cpp
@@ -219,8 +219,13 @@ void Marabou::solveQuery()
 
     struct timespec start = TimeUtils::sampleMicro();
     unsigned timeoutInSeconds = Options::get()->getInt( Options::TIMEOUT );
+
     if ( _engine->processInputQuery( _inputQuery ) )
     {
+        if ( _engine->getExitCode() == Engine::SAT )
+        {
+            return;
+        }
         _engine->solve( timeoutInSeconds );
         if ( _engine->shouldProduceProofs() && _engine->getExitCode() == Engine::UNSAT )
             _engine->certifyUNSATCertificate();
diff --git a/src/engine/MarabouError.h b/src/engine/MarabouError.h
index d70269426a..ef92c0524b 100644
--- a/src/engine/MarabouError.h
+++ b/src/engine/MarabouError.h
@@ -53,6 +53,7 @@ class MarabouError : public Error
         BOUNDS_NOT_UP_TO_DATE_IN_LP_SOLVER = 28,
         INVALID_LEAKY_RELU_SLOPE = 29,
         UNABLE_TO_RECONSTRUCT_SOLUTION_FOR_ELIMINATED_NEURONS = 30,
+        TIMEOUT = 31,
 
         // Error codes for Query Loader
         FILE_DOES_NOT_EXIST = 100,
diff --git a/src/engine/PGD.cpp b/src/engine/PGD.cpp
new file mode 100644
index 0000000000..9185570ff6
--- /dev/null
+++ b/src/engine/PGD.cpp
@@ -0,0 +1,305 @@
+#include "PGD.h"
+
+#include "InputQuery.h"
+
+#include <cmath>
+#ifdef BUILD_TORCH
+
+PGDAttack::PGDAttack( NLR::NetworkLevelReasoner *networkLevelReasoner )
+    : networkLevelReasoner( networkLevelReasoner )
+    , _device( torch::kCPU )
+    , _model( std::make_unique<CustomDNN>( networkLevelReasoner ) )
+    , _iters( GlobalConfiguration::PGD_DEFAULT_NUM_ITER )
+    , _restarts( GlobalConfiguration::PGD_NUM_RESTARTS )
+    , _adversarialInput( nullptr )
+    , _adversarialOutput( nullptr )
+{
+    _inputSize = _model->getLayerSizes().first();
+    getBounds( _inputBounds, GlobalConfiguration::PdgBoundType::PGD_INPUT );
+    getBounds( _outputBounds, GlobalConfiguration::PdgBoundType::PGD_OUTPUT );
+    std::pair<torch::Tensor, torch::Tensor> variables = generateSampleAndEpsilon();
+    _inputExample = variables.first;
+    _epsilon = variables.second;
+}
+
+PGDAttack::~PGDAttack()
+{
+    if ( _adversarialInput )
+        delete[] _adversarialInput;
+    if ( _adversarialOutput )
+        delete[] _adversarialOutput;
+}
+
+torch::Device PGDAttack::getDevice()
+{
+    if ( torch::cuda::is_available() )
+    {
+        PGD_LOG( "CUDA Device available. Using GPU" );
+        return { torch::kCUDA };
+    }
+    else
+    {
+        PGD_LOG( "CUDA Device not available. Using CPU" );
+        return { torch::kCPU };
+    }
+}
+
+void PGDAttack::getBounds( std::pair<Vector<double>, Vector<double>> &bounds,
+                           const signed type ) const
+{
+    unsigned layerIndex = type == GlobalConfiguration::PdgBoundType::PGD_INPUT
+                            ? 0
+                            : networkLevelReasoner->getNumberOfLayers() - 1;
+    const NLR::Layer *layer = networkLevelReasoner->getLayer( layerIndex );
+
+    for ( unsigned neuron = 0; neuron < layer->getSize(); ++neuron )
+    {
+        bounds.first.append( layer->getLb( neuron ) );
+        bounds.second.append( layer->getUb( neuron ) );
+    }
+}
+
+std::pair<torch::Tensor, torch::Tensor> PGDAttack::generateSampleAndEpsilon()
+{
+    Vector<double> sample( _inputSize, 0.0f );
+    Vector<double> epsilons( _inputSize, 0.0f );
+
+    for ( unsigned i = 0; i < _inputSize; i++ )
+    {
+        double lower = _inputBounds.first.get( i );
+        double upper = _inputBounds.second.get( i );
+
+        if ( std::isinf( lower ) && std::isinf( upper ) )
+        {
+            sample[i] = 0.0f;
+            epsilons[i] = std::numeric_limits<double>::infinity();
+        }
+        else if ( std::isinf( lower ) )
+        {
+            sample[i] = upper - GlobalConfiguration::PGD_INPUT_RANGE;
+            epsilons[i] = GlobalConfiguration::PGD_INPUT_RANGE;
+        }
+        else if ( std::isinf( upper ) )
+        {
+            sample[i] = lower + GlobalConfiguration::PGD_INPUT_RANGE;
+            epsilons[i] = GlobalConfiguration::PGD_INPUT_RANGE;
+        }
+        else
+        {
+            // Both bounds are finite
+            sample[i] = lower + ( upper - lower ) / 2.0f;
+            epsilons[i] = ( upper - lower ) / 2.0f;
+        }
+    }
+
+    return { torch::tensor( sample.getContainer() ).unsqueeze( 0 ).to( _device ),
+             torch::tensor( epsilons.getContainer() ).to( _device ) };
+}
+
+bool PGDAttack::isWithinBounds( const torch::Tensor &sample,
+                                const std::pair<Vector<double>, Vector<double>> &bounds )
+{
+    torch::Tensor flatInput = sample.view( { -1 } );
+    if ( flatInput.numel() != bounds.first.size() || flatInput.numel() != bounds.second.size() )
+    {
+        throw std::runtime_error( "Mismatch in sizes of input and bounds" );
+    }
+
+    for ( int64_t i = 0; i < flatInput.size( 0 ); i++ )
+    {
+        auto value = flatInput[i].item<double>();
+        double lower = bounds.first.get( i );
+        double upper = bounds.second.get( i );
+
+        if ( lower == FloatUtils::negativeInfinity() && upper == FloatUtils::infinity() )
+        {
+            // If both bounds are infinite, any value is acceptable
+            continue;
+        }
+        else if ( lower == FloatUtils::negativeInfinity() )
+        {
+            // Only check upper bound
+            if ( value > upper )
+                return false;
+        }
+        else if ( upper == FloatUtils::infinity() )
+        {
+            // Only check lower bound
+            if ( value < lower )
+                return false;
+        }
+        else
+        {
+            // Check both bounds
+            if ( value < lower || value > upper )
+                return false;
+        }
+    }
+
+    return true;
+}
+
+
+torch::Tensor PGDAttack::calculateLoss( const torch::Tensor &predictions )
+{
+    torch::Tensor lowerBoundTensor =
+        torch::tensor( _outputBounds.first.data(), torch::kFloat32 ).to( _device );
+    torch::Tensor upperBoundTensor =
+        torch::tensor( _outputBounds.second.data(), torch::kFloat32 ).to( _device );
+
+    // Compute the penalty: High loss if predictions are outside the bounds
+    torch::Tensor ubViolation =
+        torch::sum( torch::square( torch::relu( predictions - upperBoundTensor ) ) ).to( _device );
+    torch::Tensor lbViolation =
+        torch::sum( torch::square( torch::relu( lowerBoundTensor - predictions ) ) ).to( _device );
+    return torch::sum( ubViolation + lbViolation ).to( _device );
+}
+
+std::pair<torch::Tensor, torch::Tensor> PGDAttack::findAdvExample()
+{
+    double timeoutForAttack = ( Options::get()->getInt( Options::ATTACK_TIMEOUT ) == 0
+                                    ? FloatUtils::infinity()
+                                    : Options::get()->getInt( Options::ATTACK_TIMEOUT ) );
+    PGD_LOG( Stringf( "Adversarial attack timeout set to %f\n", timeoutForAttack ).ascii() );
+    timespec startTime = TimeUtils::sampleMicro();
+
+    torch::Tensor inputExample;
+    torch::Tensor currentExample;
+    torch::Tensor prevExample;
+    torch::Tensor currentPrediction;
+    torch::Tensor lowerBoundTensor =
+        torch::tensor( _inputBounds.first.getContainer(), torch::kFloat32 ).to( _device );
+    torch::Tensor upperBoundTensor =
+        torch::tensor( _inputBounds.second.getContainer(), torch::kFloat32 ).to( _device );
+    torch::Tensor delta = torch::zeros( _inputSize ).to( _device ).requires_grad_( true );
+
+    for ( unsigned i = 0; i < _restarts; ++i )
+    {
+        unsigned long timePassed = TimeUtils::timePassed( startTime, TimeUtils::sampleMicro() );
+        if ( static_cast<long double>( timePassed ) / MICROSECONDS_TO_SECONDS > timeoutForAttack )
+        {
+            throw MarabouError( MarabouError::TIMEOUT, "Attack failed due to timeout" );
+        }
+        inputExample = torch::rand( _inputExample.sizes() );
+        inputExample = inputExample * ( upperBoundTensor - lowerBoundTensor ) + lowerBoundTensor;
+
+        torch::optim::Adam optimizer( { delta }, torch::optim::AdamOptions( 0.1 ) );
+
+        for ( unsigned j = 0; j < _iters; ++j )
+        {
+            prevExample = currentExample;
+            currentExample = inputExample + delta;
+            if ( ( prevExample.defined() && currentExample.equal( prevExample ) ) ||
+                 !isWithinBounds( currentExample, _inputBounds ) )
+                break;
+
+            currentPrediction = _model->forward( currentExample );
+            if ( isWithinBounds( currentPrediction, _outputBounds ) )
+            {
+                return { currentExample, currentPrediction };
+            }
+            optimizer.zero_grad();
+            torch::Tensor loss = calculateLoss( currentPrediction );
+            loss.backward();
+            optimizer.step();
+            delta.data() = delta.data().clamp( -_epsilon, _epsilon );
+        }
+        delta = ( torch::rand( _inputSize ) * 2 - 1 )
+                    .mul( _epsilon )
+                    .to( _device )
+                    .requires_grad_( true );
+    }
+    return { currentExample, currentPrediction };
+}
+
+double PGDAttack::getAssignment( int index )
+{
+    return _assignments[index];
+}
+
+void PGDAttack::printValue( double value )
+{
+    if ( std::isinf( value ) )
+    {
+        if ( value < 0 )
+        {
+            PGD_LOG( "-inf" );
+        }
+        else
+        {
+            PGD_LOG( "inf" );
+        }
+    }
+    else if ( std::isnan( value ) )
+    {
+        PGD_LOG( "nan" );
+    }
+    else
+    {
+        PGD_LOG( Stringf( "%.3lf", value ).ascii() );
+    }
+}
+
+bool PGDAttack::runAttack()
+{
+    PGD_LOG( "-----Starting PGD attack-----" );
+    auto adversarial = findAdvExample();
+    torch::Tensor advInput = adversarial.first.to( torch::kDouble );
+    torch::Tensor advPred = adversarial.second.to( torch::kDouble );
+
+    bool isFooled =
+        isWithinBounds( advInput, _inputBounds ) && isWithinBounds( advPred, _outputBounds );
+
+    auto *example = advInput.data_ptr<double>();
+    auto *prediction = advPred.data_ptr<double>();
+    size_t outputSize = advPred.size( 1 );
+    ASSERT( advInput.size( 1 ) == _inputSize && outputSize == _model->getLayerSizes().last() );
+
+    if ( isFooled )
+    {
+        _adversarialInput = new double[advInput.size( 1 )];
+        _adversarialOutput = new double[advPred.size( 1 )];
+
+        std::copy( example, example + _inputSize, _adversarialInput );
+        std::copy( prediction, prediction + outputSize, _adversarialOutput );
+    }
+    PGD_LOG( "Input Lower Bounds : " );
+    for ( auto &bound : _inputBounds.first.getContainer() )
+        printValue( bound );
+    PGD_LOG( "Input Upper Bounds : " );
+    for ( auto &bound : _inputBounds.second.getContainer() )
+        printValue( bound );
+
+    PGD_LOG( "Adversarial Input:" );
+    for ( int i = 0; i < advInput.numel(); ++i )
+    {
+        PGD_LOG( Stringf( "x%u=%.3lf", i, example[i] ).ascii() );
+    }
+    PGD_LOG( "Output Lower Bounds : " );
+    for ( auto &bound : _outputBounds.first.getContainer() )
+        printValue( bound );
+    PGD_LOG( "Output Upper Bounds : " );
+    for ( auto &bound : _outputBounds.second.getContainer() )
+        printValue( bound );
+
+    PGD_LOG( "Adversarial Prediction: " );
+    for ( int i = 0; i < advPred.numel(); ++i )
+    {
+        PGD_LOG( Stringf( "y%u=%.3lf", i, prediction[i] ).ascii() );
+    }
+
+
+    if ( isFooled )
+    {
+        PGD_LOG( "Model fooled: Yes \n ------ PGD Attack Succeed ------\n" );
+    }
+    else
+        PGD_LOG( "Model fooled: No \n ------ PGD Attack Failed ------\n" );
+
+
+    if ( _adversarialInput )
+        networkLevelReasoner->concretizeInputAssignment( _assignments, _adversarialInput );
+
+    return isFooled;
+}
+#endif
\ No newline at end of file
diff --git a/src/engine/PGD.h b/src/engine/PGD.h
new file mode 100644
index 0000000000..8a27b0ab9f
--- /dev/null
+++ b/src/engine/PGD.h
@@ -0,0 +1,86 @@
+#ifdef BUILD_TORCH
+#ifndef __PGD_h__
+#define __PGD_h__
+#undef Warning
+#include <torch/torch.h>
+#include "CustomDNN.h"
+#include "Options.h"
+
+#include <TimeUtils.h>
+#define PGD_LOG( x, ... ) LOG( GlobalConfiguration::CUSTOM_DNN_LOGGING, "PGD: %s\n", x )
+
+
+
+/*
+  PGDAttack class implements the Projected Gradient Descent method for generating
+  adversarial examples for the network.
+  The model aim to find valid input to the network that result in outputs within output bounds
+  (SAT).
+*/
+class PGDAttack
+{
+public:
+    enum {
+        MICROSECONDS_TO_SECONDS = 1000000,
+    };
+    PGDAttack( NLR::NetworkLevelReasoner *networkLevelReasoner );
+    ~PGDAttack();
+
+    /*
+    Search for an adversarial example. Returns true if successful.
+  */
+    bool runAttack();
+    double getAssignment( int index );
+
+
+private:
+    NLR::NetworkLevelReasoner *networkLevelReasoner;
+    torch::Device _device;
+    /*
+     The maximum permissible perturbation for each variable in the input vector, Defining
+     the scope of allowable changes to the input during the attack.
+     */
+    torch::Tensor _epsilon;
+    torch::Tensor _inputExample;
+    std::unique_ptr<CustomDNN> _model;
+    unsigned _iters;
+    unsigned _restarts;
+    unsigned _inputSize;
+    std::pair<Vector<double>, Vector<double>> _inputBounds;
+    std::pair<Vector<double>, Vector<double>> _outputBounds;
+    Map<unsigned, double> _assignments;
+    double *_adversarialInput;
+    double *_adversarialOutput;
+
+    /*
+     Iteratively generates and refines adversarial examples, aiming to discover inputs that lead to
+     predictions outside the defined bounds, using gradient-based optimization.
+     */
+    std::pair<torch::Tensor, torch::Tensor> findAdvExample();
+    /*
+    Generates a valid sample input and epsilon tensor for initializing the attack,
+   */
+    std::pair<torch::Tensor, torch::Tensor> generateSampleAndEpsilon();
+
+    /*
+      Checks if a given sample is within the valid bounds
+    */
+    static bool isWithinBounds( const torch::Tensor &sample,
+                                const std::pair<Vector<double>, Vector<double>> &bounds );
+    /*
+     Get the bounds of each neuron in the network defining in the nlr.
+     */
+    void getBounds( std::pair<Vector<double>, Vector<double>> &bounds, signed type ) const;
+    /*
+     Calculates the loss based on how far the network's outputs deviate from its bounds.
+     Assigns a higher loss to predictions that fall outside bounds.
+
+  */
+    torch::Tensor calculateLoss( const torch::Tensor &predictions );
+    static torch::Device getDevice();
+    static void printValue( double value );
+};
+
+
+#endif
+#endif
\ No newline at end of file
diff --git a/src/engine/Preprocessor.cpp b/src/engine/Preprocessor.cpp
index e4f2de17e1..08a00c0487 100644
--- a/src/engine/Preprocessor.cpp
+++ b/src/engine/Preprocessor.cpp
@@ -13,6 +13,7 @@
 
  **/
 
+
 #include "Preprocessor.h"
 
 #include "Debug.h"
@@ -26,7 +27,6 @@
 #include "PiecewiseLinearFunctionType.h"
 #include "Statistics.h"
 #include "Tightening.h"
-
 #ifdef _WIN32
 #undef INFINITE
 #endif
@@ -174,6 +174,12 @@ std::unique_ptr<InputQuery> Preprocessor::preprocess( const InputQuery &query,
     ASSERT( _preprocessed->getLowerBounds().size() == _preprocessed->getNumberOfVariables() );
     ASSERT( _preprocessed->getUpperBounds().size() == _preprocessed->getNumberOfVariables() );
 
+
+    String networkFilePath = Options::get()->getString( Options::INPUT_FILE_PATH );
+
+
+
+
     return std::move( _preprocessed );
 }
 
diff --git a/src/engine/SumOfInfeasibilitiesManager.cpp b/src/engine/SumOfInfeasibilitiesManager.cpp
index 606a059bb3..0cdd54e17e 100644
--- a/src/engine/SumOfInfeasibilitiesManager.cpp
+++ b/src/engine/SumOfInfeasibilitiesManager.cpp
@@ -192,8 +192,19 @@ void SumOfInfeasibilitiesManager::proposePhasePatternUpdateRandomly()
     } );
 
     // First, pick a pl constraint whose cost component we will update.
-    unsigned index = (unsigned)T::rand() % _plConstraintsInCurrentPhasePattern.size();
-    PiecewiseLinearConstraint *plConstraintToUpdate = _plConstraintsInCurrentPhasePattern[index];
+    bool fixed = true;
+    PiecewiseLinearConstraint *plConstraintToUpdate;
+    while ( fixed )
+    {
+        if ( _plConstraintsInCurrentPhasePattern.empty() )
+            return;
+
+        unsigned index = (unsigned)T::rand() % _plConstraintsInCurrentPhasePattern.size();
+        plConstraintToUpdate = _plConstraintsInCurrentPhasePattern[index];
+        fixed = plConstraintToUpdate->phaseFixed();
+        if ( fixed )
+            removeCostComponentFromHeuristicCost( plConstraintToUpdate );
+    }
 
     // Next, pick an alternative phase.
     PhaseStatus currentPhase = _currentPhasePattern[plConstraintToUpdate];
diff --git a/src/input_parsers/OnnxParser.cpp b/src/input_parsers/OnnxParser.cpp
index 71848dad3b..19e5e28003 100644
--- a/src/input_parsers/OnnxParser.cpp
+++ b/src/input_parsers/OnnxParser.cpp
@@ -972,7 +972,7 @@ void OnnxParser::makeMarabouEquations( onnx::NodeProto &node, bool makeEquations
 void OnnxParser::constant( onnx::NodeProto &node )
 {
     String outputNodeName = node.output()[0];
-    const onnx::TensorProto &value = getTensorAttribute( node, "value" );
+    const onnx::TensorProto value = getTensorAttribute( node, "value" );
     const TensorShape shape = shapeOfConstant( value );
 
     _shapeMap[outputNodeName] = shape;
diff --git a/src/input_parsers/TensorUtils.cpp b/src/input_parsers/TensorUtils.cpp
index eab6aae7f9..d88719aff7 100644
--- a/src/input_parsers/TensorUtils.cpp
+++ b/src/input_parsers/TensorUtils.cpp
@@ -165,9 +165,9 @@ calculatePaddingNeeded( int inputSize, int filterSize, int stride, bool padFront
 Permutation reversePermutation( unsigned int size )
 {
     Permutation result;
-    for ( unsigned int i = size - 1; i-- > 0; )
+    for ( unsigned int i = size; i-- > 0; )
     {
         result.append( i );
     }
     return result;
-}
+}
\ No newline at end of file
diff --git a/src/input_parsers/TensorUtils.h b/src/input_parsers/TensorUtils.h
index 295f8aac6c..3d46074856 100644
--- a/src/input_parsers/TensorUtils.h
+++ b/src/input_parsers/TensorUtils.h
@@ -55,6 +55,8 @@ TensorIndices unpackIndex( TensorShape shape, PackedTensorIndices packedIndex );
 
 PackedTensorIndices packIndex( TensorShape shape, TensorIndices indices );
 
+unsigned int tensorSize( TensorShape shape );
+
 template <typename T> T tensorLookup( Vector<T> tensor, TensorShape shape, TensorIndices indices )
 {
     return tensor[packIndex( shape, indices )];
@@ -77,20 +79,20 @@ Vector<T> transposeTensor( Vector<T> tensor, TensorShape shape, Permutation perm
     // NOTE this implementation is *very* inefficient. Eventually we might want to
     // switch to a similar implementation as NumPy arrays with internal strides etc.
     ASSERT( shape.size() == permutation.size() );
+    ASSERT( tensorSize( shape ) == tensor.size() );
+
     TensorShape transposedShape = transposeVector( shape, permutation );
     Vector<T> result( tensor.size() );
-    for ( PackedTensorIndices rawOutputIndex = 0; rawOutputIndex < tensor.size(); rawOutputIndex++ )
+    for ( PackedTensorIndices rawInputIndex = 0; rawInputIndex < tensor.size(); rawInputIndex++ )
     {
-        TensorIndices outputIndex = unpackIndex( transposedShape, rawOutputIndex );
-        TensorIndices inputIndex = transposeVector( outputIndex, permutation );
-        T value = tensorLookup( tensor, shape, inputIndex );
-        result[rawOutputIndex] = value;
+        TensorIndices inputIndex = unpackIndex( shape, rawInputIndex );
+        TensorIndices outputIndex = transposeVector( inputIndex, permutation );
+        int rawOutputIndex = packIndex( transposedShape, outputIndex );
+        result[rawOutputIndex] = tensor[rawInputIndex];
     }
     return result;
 }
 
-unsigned int tensorSize( TensorShape shape );
-
 // See https://github.com/onnx/onnx/blob/main/docs/Broadcasting.md#multidirectional-broadcasting
 TensorShape getMultidirectionalBroadcastShape( TensorShape shape1, TensorShape shape2 );
 
diff --git a/src/nlr/NetworkLevelReasoner.cpp b/src/nlr/NetworkLevelReasoner.cpp
index 6d93535021..2bb8f09a1c 100644
--- a/src/nlr/NetworkLevelReasoner.cpp
+++ b/src/nlr/NetworkLevelReasoner.cpp
@@ -128,7 +128,8 @@ void NetworkLevelReasoner::evaluate( double *input, double *output )
     memcpy( output, outputLayer->getAssignment(), sizeof( double ) * outputLayer->getSize() );
 }
 
-void NetworkLevelReasoner::concretizeInputAssignment( Map<unsigned, double> &assignment )
+void NetworkLevelReasoner::concretizeInputAssignment( Map<unsigned, double> &assignment,
+                                                      const double *pgdAdversarialInput )
 {
     Layer *inputLayer = _layerIndexToLayer[0];
     ASSERT( inputLayer->getLayerType() == Layer::INPUT );
@@ -144,7 +145,12 @@ void NetworkLevelReasoner::concretizeInputAssignment( Map<unsigned, double> &ass
         if ( !inputLayer->neuronEliminated( index ) )
         {
             unsigned variable = inputLayer->neuronToVariable( index );
-            double value = _tableau->getValue( variable );
+            double value;
+            if (pgdAdversarialInput)
+                value = pgdAdversarialInput[index];
+            else
+                value = _tableau->getValue( variable );
+
             input[index] = value;
             assignment[variable] = value;
         }
diff --git a/src/nlr/NetworkLevelReasoner.h b/src/nlr/NetworkLevelReasoner.h
index 93fa39423a..926cee6b1b 100644
--- a/src/nlr/NetworkLevelReasoner.h
+++ b/src/nlr/NetworkLevelReasoner.h
@@ -79,7 +79,8 @@ class NetworkLevelReasoner : public LayerOwner
       Perform an evaluation of the network for the current input variable
       assignment and store the resulting variable assignment in the assignment.
     */
-    void concretizeInputAssignment( Map<unsigned, double> &assignment );
+    void concretizeInputAssignment( Map<unsigned, double> &assignment,
+                                    const double *pgdAdversarialInput = nullptr );
 
     /*
       Perform a simulation of the network for a specific input
diff --git a/tools/download_boost.sh b/tools/download_boost.sh
index f77d5fbd42..83bbc0e4d8 100755
--- a/tools/download_boost.sh
+++ b/tools/download_boost.sh
@@ -9,7 +9,7 @@ cd $mydir
 # multiple lines
 echo "Downloading boost"
 underscore_version=${version//./_}
-wget -q https://sourceforge.net/projects/boost/files/boost/$version/boost_$underscore_version.tar.gz/download -O boost-$version.tar.gz
+wget https://sourceforge.net/projects/boost/files/boost/$version/boost_$underscore_version.tar.gz/download -O boost-$version.tar.gz -q --show-progress --progress=bar:force:noscroll
 
 echo "Unzipping boost"
 tar xzvf boost-$version.tar.gz >> /dev/null
diff --git a/tools/download_libtorch.bat b/tools/download_libtorch.bat
new file mode 100644
index 0000000000..177d0ad323
--- /dev/null
+++ b/tools/download_libtorch.bat
@@ -0,0 +1,14 @@
+@echo off
+set LIBTORCH_VERSION=%1
+set LIBTORCH_DIR=%~dp0
+
+set TEMP_DIR=%LIBTORCH_DIR%\temp
+
+if not exist "%TEMP_DIR%" mkdir "%TEMP_DIR%"
+
+powershell -command "Invoke-WebRequest -Uri https://download.pytorch.org/libtorch/cpu/libtorch-cxx11-abi-shared-with-deps-2.3.1%2Bcpu.zip -OutFile %TEMP_DIR%\libtorch.zip"
+
+powershell -command "Expand-Archive -Path %TEMP_DIR%\libtorch.zip -DestinationPath %LIBTORCH_DIR%"
+
+del "%TEMP_DIR%\libtorch.zip"
+rmdir /s /q "%TEMP_DIR%"
diff --git a/tools/download_libtorch.sh b/tools/download_libtorch.sh
new file mode 100755
index 0000000000..90f1884b42
--- /dev/null
+++ b/tools/download_libtorch.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+curdir=$pwd
+mydir="${0%/*}"
+version=$1
+
+cd $mydir
+
+# Need to download the cxx11-abi version of libtorch in order to ensure compatability
+# with boost.
+#
+# See https://discuss.pytorch.org/t/issues-linking-with-libtorch-c-11-abi/29510 for details.
+echo "Downloading PyTorch"
+wget https://download.pytorch.org/libtorch/cpu/libtorch-cxx11-abi-shared-with-deps-$version%2Bcpu.zip -O libtorch-$version.zip -q --show-progress --progress=bar:force:noscroll
+
+echo "Unzipping PyTorch"
+unzip libtorch-$version.zip >> /dev/null
+mv libtorch libtorch-$version
+
+cd $curdir
diff --git a/tools/download_onnx.sh b/tools/download_onnx.sh
index 3ca484754e..8c0cd22e4e 100755
--- a/tools/download_onnx.sh
+++ b/tools/download_onnx.sh
@@ -17,7 +17,7 @@ cd $mydir
 mkdir -p $onnxdir
 cd $onnxdir
 echo "Downloading ONNX proto file"
-wget -q https://raw.githubusercontent.com/onnx/onnx/v$version/onnx/onnx.proto3 -O onnx.proto3
+wget https://raw.githubusercontent.com/onnx/onnx/v$version/onnx/onnx.proto3 -O onnx.proto3  -q --show-progress --progress=bar:force:noscroll
 
 echo "Compiling the ONNX proto file"
 ../$protobufdir/installed/bin/protoc --cpp_out=. onnx.proto3
diff --git a/tools/download_protobuf.sh b/tools/download_protobuf.sh
index 2b0e4e31a6..29e9bc8972 100755
--- a/tools/download_protobuf.sh
+++ b/tools/download_protobuf.sh
@@ -17,8 +17,7 @@ fi
 
 cd $mydir
 echo "Downloading protobuf-$version"
-wget -q https://github.com/protocolbuffers/protobuf/releases/download/v$version/protobuf-cpp-$version.tar.gz -O protobuf-cpp-$version.tar.gz
-
+wget https://github.com/protocolbuffers/protobuf/releases/download/v$version/protobuf-cpp-$version.tar.gz -O protobuf-cpp-$version.tar.gz  -q --show-progress --progress=bar:force:noscroll
 echo "Unzipping protobuf-$version"
 tar -xzf protobuf-cpp-$version.tar.gz # >> /dev/null
 
diff --git a/tools/download_pybind11.sh b/tools/download_pybind11.sh
index 7dec0beec1..73698e9161 100755
--- a/tools/download_pybind11.sh
+++ b/tools/download_pybind11.sh
@@ -8,8 +8,7 @@ cd $mydir
 # TODO: add progress bar, -q is quite, if removing it the progress bar is in
 # multiple lines
 echo "downloading pybind"
-wget -q https://github.com/pybind/pybind11/archive/v$version.tar.gz -O pybind11-$version.tar.gz
-
+wget https://github.com/pybind/pybind11/archive/v$version.tar.gz -O pybind11-$version.tar.gz  -q --show-progress --progress=bar:force:noscroll
 echo "unzipping pybind"
 tar xzvf pybind11-$version.tar.gz >> /dev/null