From 5448aa3367acdbbba760ca05c62fa48f3ed49a74 Mon Sep 17 00:00:00 2001
From: Ori Lahav <vbCrLf@GMail.com>
Date: Wed, 22 Jul 2020 13:18:41 +0300
Subject: [PATCH] Fix file redirection

---
 maraboupy/MarabouCore.cpp | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/maraboupy/MarabouCore.cpp b/maraboupy/MarabouCore.cpp
index 87066fd79b..9e6e6edc24 100644
--- a/maraboupy/MarabouCore.cpp
+++ b/maraboupy/MarabouCore.cpp
@@ -150,7 +150,10 @@ std::pair<std::map<int, double>, Statistics> solve(InputQuery &inputQuery, Marab
         Engine engine;
         engine.setVerbosity(verbosity);
 
-        if(!engine.processInputQuery(inputQuery)) return std::make_pair(ret, *(engine.getStatistics()));
+        if(!engine.processInputQuery(inputQuery)) {
+            retStats = *(engine.getStatistics());
+            goto cleanup;
+        }
         if ( dnc )
         {
             unsigned initialDivides = options._initialDivides;
@@ -177,14 +180,17 @@ std::pair<std::map<int, double>, Statistics> solve(InputQuery &inputQuery, Marab
             {
                 retStats = Statistics();
                 retStats.timeout();
-                return std::make_pair( ret, retStats );
             }
             default:
-                return std::make_pair( ret, Statistics() ); // TODO: meaningful DnCStatistics
+                retStats = Statistics(); // TODO: meaningful DnCStatistics
+                goto cleanup;
             }
         } else
         {
-            if(!engine.solve(timeoutInSeconds)) return std::make_pair(ret, *(engine.getStatistics()));
+            if(!engine.solve(timeoutInSeconds)) {
+                retStats = *(engine.getStatistics());
+                goto cleanup;
+            }
 
             if (engine.getExitCode() == Engine::SAT)
                 engine.extractSolution(inputQuery);
@@ -195,10 +201,11 @@ std::pair<std::map<int, double>, Statistics> solve(InputQuery &inputQuery, Marab
     }
     catch(const MarabouError &e){
         printf( "Caught a MarabouError. Code: %u. Message: %s\n", e.getCode(), e.getUserMessage() );
-        return std::make_pair(ret, retStats);
+        goto cleanup;
     }
-    if(output != -1)
-        restoreOutputStream(output);
+
+cleanup:
+    if(output != -1) restoreOutputStream(output);
     return std::make_pair(ret, retStats);
 }