diff --git a/README.md b/README.md
index 23391036f..078e3d18c 100644
--- a/README.md
+++ b/README.md
@@ -148,6 +148,8 @@ cd build
 cmake .. -G"Visual Studio 15 2017 Win64" -DBUILD_PYTHON=ON
 cmake --build . --config Release
 ```
+Make sure the detected python ("Found PythonInterp: ....") is a windows python and not cygwin or something like that (if it is cygwin, use -DPYTHON_EXECUTABLE flag to override the default python, or manuialy download the linux pybind and locate it in the tools directory)
+
 This process will produce the binary file and the shared library for the Python 
 API. The shared library will be in the maraboupy folder for Linux and MacOS. 
 On Windows, the shared library is written to a Release subfolder in maraboupy, 
@@ -207,7 +209,7 @@ We have three types of tests:
 * regression tests - test end to end functionality thorugh the API, each test is defined by:  
   * network_file - description of the "neural network" supporting nnet and mps formats (using the extension to decdie on the format)  
   * property_file - optional, constraint on the input and output variables  
-  * expected_result - SAT/UNSAT  
+  * expected_result - sat/unsat  
 
 The tests are divided into 5 levels to allow variability in running time, to add a new regression tests: 
   * add the description of the network and property to the _resources_ sub-folder 
diff --git a/maraboupy/Marabou.py b/maraboupy/Marabou.py
index 09a07d6ea..9f5afa555 100644
--- a/maraboupy/Marabou.py
+++ b/maraboupy/Marabou.py
@@ -100,9 +100,9 @@ def solve_query(ipq, filename="", verbose=True, timeout=0, verbosity=2):
         if stats.hasTimedOut():
             print ("TIMEOUT")
         elif len(vals)==0:
-            print("UNSAT")
+            print("unsat")
         else:
-            print("SAT")
+            print("sat")
             for i in range(ipq.getNumInputVariables()):
                 print("input {} = {}".format(i, vals[ipq.inputVariableByIndex(i)]))
             for i in range(ipq.getNumOutputVariables()):
diff --git a/maraboupy/MarabouNetwork.py b/maraboupy/MarabouNetwork.py
index 451efe825..b0cd78583 100644
--- a/maraboupy/MarabouNetwork.py
+++ b/maraboupy/MarabouNetwork.py
@@ -201,9 +201,9 @@ def solve(self, filename="", verbose=True, options=None):
             if stats.hasTimedOut():
                 print("TO")
             elif len(vals)==0:
-                print("UNSAT")
+                print("unsat")
             else:
-                print("SAT")
+                print("sat")
                 for j in range(len(self.inputVars)):
                     for i in range(self.inputVars[j].size):
                         print("input {} = {}".format(i, vals[self.inputVars[j].item(i)]))
diff --git a/maraboupy/MarabouNetworkONNX.py b/maraboupy/MarabouNetworkONNX.py
index 1c2eecf1e..4b6e2b983 100644
--- a/maraboupy/MarabouNetworkONNX.py
+++ b/maraboupy/MarabouNetworkONNX.py
@@ -342,7 +342,7 @@ def transpose(self, node):
         if inputName in self.varMap:
             self.varMap[nodeName] = np.transpose(self.varMap[node.input[0]], perm)
         elif inputName in self.constantMap:
-            self.constantMap[nodeName] = np.transpose(self.constant[inputName], perm)
+            self.constantMap[nodeName] = np.transpose(self.constantMap[inputName], perm)
     
     def maxpoolEquations(self, node, makeEquations):
         """
@@ -812,4 +812,4 @@ def evaluateWithoutMarabou(self, inputValues):
                 printf("Not sure how to cast input to graph input of type %s" % onnxType)
                 raise NotImplementedError
             input_dict[inputName] = inputValues[i].reshape(self.inputVars[i].shape).astype(inputType)
-        return sess.run([self.outputName],input_dict)[0]
\ No newline at end of file
+        return sess.run([self.outputName],input_dict)[0]
diff --git a/maraboupy/examples/Example Notebook.ipynb b/maraboupy/examples/Example Notebook.ipynb
index f4a9e645c..13de4f9b2 100644
--- a/maraboupy/examples/Example Notebook.ipynb	
+++ b/maraboupy/examples/Example Notebook.ipynb	
@@ -94,7 +94,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "SAT\n",
+      "sat\n",
       "input 0 = -0.32842287715105956\n",
       "input 1 = 0.18470882292589386\n",
       "input 2 = -0.015568802288230335\n",
@@ -177,7 +177,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "SAT\n",
+      "sat\n",
       "input 0 = -0.32842287715105956\n",
       "input 1 = 0.18470882292589386\n",
       "input 2 = -0.015568802288230335\n",
@@ -245,7 +245,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "SAT\n",
+      "sat\n",
       "input 0 = -0.328422874212265\n",
       "input 1 = 0.40932923555374146\n",
       "input 2 = -0.017379289492964745\n",
diff --git a/maraboupy/examples/MarabouCoreExample.py b/maraboupy/examples/MarabouCoreExample.py
index 715236840..4af92fb26 100644
--- a/maraboupy/examples/MarabouCoreExample.py
+++ b/maraboupy/examples/MarabouCoreExample.py
@@ -88,7 +88,7 @@
 options = createOptions()
 vars1, stats1 = MarabouCore.solve(inputQuery, options, "")
 if len(vars1) > 0:
-    print("SAT")
+    print("sat")
     print(vars1)
 else:
-    print("UNSAT")
+    print("unsat")
diff --git a/regress/regress0/CMakeLists.txt b/regress/regress0/CMakeLists.txt
index 5c7659a44..427f74d14 100644
--- a/regress/regress0/CMakeLists.txt
+++ b/regress/regress0/CMakeLists.txt
@@ -1,11 +1,11 @@
-marabou_add_regress_mps_test(0 "lp_feasible_1.mps" "SAT" "" "mps")
-marabou_add_regress_mps_test(0 "lp_infeasible_1.mps" "UNSAT" "" "mps")
+marabou_add_regress_mps_test(0 "lp_feasible_1.mps" "sat" "" "mps")
+marabou_add_regress_mps_test(0 "lp_infeasible_1.mps" "unsat" "" "mps")
 
-marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_1_7.nnet" "3" SAT)
-marabou_add_acasxu_dnc_test(0 "ACASXU_experimental_v2a_1_9.nnet" "4" SAT)
-marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_4_1.nnet" "4" UNSAT)
+marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_1_7.nnet" "3" sat)
+marabou_add_acasxu_dnc_test(0 "ACASXU_experimental_v2a_1_9.nnet" "4" sat)
+marabou_add_acasxu_test(0 "ACASXU_experimental_v2a_4_1.nnet" "4" unsat)
 
-marabou_add_coav_test(0 "reluBenchmark0.067841053009s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(0 "reluBenchmark0.0518190860748s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(0 "reluBenchmark0.536728143692s_SAT.nnet" SAT)
-marabou_add_coav_test(0 "reluBenchmark0.899523973465s_SAT.nnet" SAT)
+marabou_add_coav_test(0 "reluBenchmark0.067841053009s_UNSAT.nnet" unsat)
+marabou_add_coav_test(0 "reluBenchmark0.0518190860748s_UNSAT.nnet" unsat)
+marabou_add_coav_test(0 "reluBenchmark0.536728143692s_SAT.nnet" sat)
+marabou_add_coav_test(0 "reluBenchmark0.899523973465s_SAT.nnet" sat)
diff --git a/regress/regress1/CMakeLists.txt b/regress/regress1/CMakeLists.txt
index 9c57eaf64..f83b1310c 100644
--- a/regress/regress1/CMakeLists.txt
+++ b/regress/regress1/CMakeLists.txt
@@ -1,111 +1,111 @@
 
-marabou_add_coav_test(1 "reluBenchmark1.30941200256s_UNSAT.nnet" UNSAT) 
-marabou_add_coav_test(1 "reluBenchmark0.94518494606s_SAT.nnet" SAT) 
-marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_8.nnet" "3" SAT)
-marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_2_9.nnet" "3" UNSAT)
-marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_6.nnet" "3" UNSAT)
-marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_6.nnet" "4" UNSAT)
-marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_7.nnet" "4" SAT)
-marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_8.nnet" "4" SAT)
-marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_9.nnet" "4" SAT)
+marabou_add_coav_test(1 "reluBenchmark1.30941200256s_UNSAT.nnet" unsat) 
+marabou_add_coav_test(1 "reluBenchmark0.94518494606s_SAT.nnet" sat) 
+marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_8.nnet" "3" sat)
+marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_2_9.nnet" "3" unsat)
+marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_6.nnet" "3" unsat)
+marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_6.nnet" "4" unsat)
+marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_7.nnet" "4" sat)
+marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_8.nnet" "4" sat)
+marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_1_9.nnet" "4" sat)
 
 
-marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_5_7.nnet" "3" UNSAT)
-marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_4_7.nnet" "4" UNSAT)
+marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_5_7.nnet" "3" unsat)
+marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_4_7.nnet" "4" unsat)
 
 
 
 
-marabou_add_coav_test(1 "reluBenchmark0.453322172165s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.30711388588s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.00512099266052s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.725997209549s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.919886112213s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0352051258087s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.97177696228s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.36359000206s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0990879535675s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.20350694656s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.221790075302s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.048150062561s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.781363010406s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.0492730140686s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0494029521942s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.499482154846s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.674989938736s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark1.15705108643s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.0606548786163s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.21319699287s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.0064799785614s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0780329704285s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.454473018646s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.00568509101868s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.930528879166s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.0380239486694s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.764842987061s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.385080099106s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark1.07406687737s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0645151138306s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.04137301445s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.505765914917s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.07428097725s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.734488964081s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.326423883438s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.398984909058s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.379405975342s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.479170084s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0386769771576s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.4906899929s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark2.79231500626s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.345348119736s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.780378818512s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.32709693909s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.287177085876s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0374069213867s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0594508647919s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0918869972229s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.983299016953s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0842049121857s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.213617086411s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.666516065598s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.149944067s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.165054798126s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.00636315345764s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0596628189087s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0065929889679s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.30961179733s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0715999603271s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.29426407814s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.294414997101s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.124088048935s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0637600421906s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.00662088394165s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.276684999466s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.271136045456s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.101797103882s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.836799860001s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.907590150833s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.54942297935s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.692045211792s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.04315304756s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.213303089142s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.09928894043s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark1.21413683891s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.183997154236s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.514003992081s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.047042131424s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0507640838623s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.83825802803s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.262641906738s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.434634923935s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.950109958649s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.62436914444s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.73387503624s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.0452961921692s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.828888177872s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.996887922287s_SAT.nnet" SAT)
-marabou_add_coav_test(1 "reluBenchmark0.0575940608978s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.213079929352s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark1.81178617477s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.956095933914s_UNSAT.nnet" UNSAT)
-marabou_add_coav_test(1 "reluBenchmark0.00601387023926s_UNSAT.nnet" UNSAT)
+marabou_add_coav_test(1 "reluBenchmark0.453322172165s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.30711388588s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.00512099266052s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.725997209549s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.919886112213s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0352051258087s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.97177696228s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.36359000206s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0990879535675s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.20350694656s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.221790075302s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.048150062561s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.781363010406s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.0492730140686s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0494029521942s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.499482154846s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.674989938736s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark1.15705108643s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.0606548786163s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.21319699287s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.0064799785614s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0780329704285s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.454473018646s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.00568509101868s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.930528879166s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.0380239486694s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.764842987061s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.385080099106s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark1.07406687737s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0645151138306s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.04137301445s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.505765914917s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.07428097725s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.734488964081s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.326423883438s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.398984909058s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.379405975342s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.479170084s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0386769771576s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.4906899929s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark2.79231500626s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.345348119736s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.780378818512s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.32709693909s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.287177085876s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0374069213867s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0594508647919s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0918869972229s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.983299016953s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0842049121857s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.213617086411s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.666516065598s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.149944067s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.165054798126s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.00636315345764s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0596628189087s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0065929889679s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.30961179733s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0715999603271s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.29426407814s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.294414997101s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.124088048935s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0637600421906s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.00662088394165s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.276684999466s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.271136045456s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.101797103882s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.836799860001s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.907590150833s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.54942297935s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.692045211792s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.04315304756s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.213303089142s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.09928894043s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark1.21413683891s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.183997154236s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.514003992081s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.047042131424s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0507640838623s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.83825802803s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.262641906738s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.434634923935s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.950109958649s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.62436914444s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.73387503624s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.0452961921692s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.828888177872s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.996887922287s_SAT.nnet" sat)
+marabou_add_coav_test(1 "reluBenchmark0.0575940608978s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.213079929352s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark1.81178617477s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.956095933914s_UNSAT.nnet" unsat)
+marabou_add_coav_test(1 "reluBenchmark0.00601387023926s_UNSAT.nnet" unsat)
diff --git a/regress/regress2/CMakeLists.txt b/regress/regress2/CMakeLists.txt
index 306ae5a29..9402ad74b 100644
--- a/regress/regress2/CMakeLists.txt
+++ b/regress/regress2/CMakeLists.txt
@@ -1,11 +1,11 @@
 
-marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_7.nnet" "4" UNSAT) 
-marabou_add_coav_test(2 "reluBenchmark2.66962385178s_UNSAT.nnet" UNSAT) #25 sec
-marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_9.nnet" "3" UNSAT) #
+marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_7.nnet" "4" unsat) 
+marabou_add_coav_test(2 "reluBenchmark2.66962385178s_UNSAT.nnet" unsat) #25 sec
+marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_9.nnet" "3" unsat) #
 
- marabou_add_coav_test(2 "reluBenchmark2.64361000061s_SAT.nnet" SAT) # 25sec
-# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_5_1.nnet" "2" SAT) # 480sec
-# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_2_4.nnet" "2" SAT) # 300sec
-# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_7.nnet" "4" UNSAT) # 150sec
-# marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_5.nnet" "2" SAT) # timeout
-# marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_9.nnet" "3" UNSAT) # 200sec
+ marabou_add_coav_test(2 "reluBenchmark2.64361000061s_SAT.nnet" sat) # 25sec
+# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_5_1.nnet" "2" sat) # 480sec
+# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_2_4.nnet" "2" sat) # 300sec
+# marabou_add_acasxu_test(1 "ACASXU_experimental_v2a_3_7.nnet" "4" unsat) # 150sec
+# marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_5.nnet" "2" sat) # timeout
+# marabou_add_acasxu_dnc_test(1 "ACASXU_experimental_v2a_3_9.nnet" "3" unsat) # 200sec
diff --git a/regress/run_regression.py b/regress/run_regression.py
index 08223c62c..5346dd541 100755
--- a/regress/run_regression.py
+++ b/regress/run_regression.py
@@ -5,7 +5,7 @@
 import threading
 
 DEFAULT_TIMEOUT = 600
-EXPECTED_RESULT_OPTIONS = ('SAT', 'UNSAT')
+EXPECTED_RESULT_OPTIONS = ('sat', 'unsat')
 
 
 def run_process(args, cwd, timeout, s_input=None):
@@ -50,19 +50,19 @@ def analyze_process_result(out, err, exit_status, expected_result):
         print("err: {}".format(err))
         return False
 
-    # If the output is UNSAT there is no \n after the UNSAT statement
-    if expected_result == 'UNSAT':
+    # If the output is unsat there is no \n after the unsat statement
+    if expected_result == 'unsat':
         out_lines = out.splitlines()
         if out_lines[-1] == expected_result:
             return True
         else:
-            print("Expected UNSAT, but last line is in output is: ", out_lines[-1])
+            print("Expected unsat, but last line is in output is: ", out_lines[-1])
             return False
     else:
-        if '\nSAT' in out:
+        if '\nsat' in out:
             return True
         else:
-            print('expected SAT, but \'\\nSAT\' is not in the output. tail of the output:\n', out[-1500:])
+            print('expected sat, but \'\\nSAT\' is not in the output. tail of the output:\n', out[-1500:])
             return False
 
 
@@ -72,7 +72,7 @@ def run_marabou(marabou_binary, network_path, property_path, expected_result, ti
     :param marabou_binary: path to marabou executable
     :param network_path: path to nnet file to pass too marabou
     :param property_path: path to property file to pass to marabou to verify
-    :param expected_result: SAT / UNSAT
+    :param expected_result: sat / unsat
     :param arguments list of arguments to pass to Marabou (for example DnC mode)
     :return: True / False if test pass or not
     '''
@@ -83,7 +83,7 @@ def run_marabou(marabou_binary, network_path, property_path, expected_result, ti
         sys.exit('"{}" does not exist or is not a file'.format(network_path))
     if not os.path.isfile(property_path):
         sys.exit('"{}" does not exist or is not a file'.format(property_path))
-    if expected_result not in {'SAT', 'UNSAT'}:
+    if expected_result not in {'sat', 'unsat'}:
         sys.exit('"{}" is not a marabou supported result'.format(expected_result))
 
     args = [marabou_binary, network_path, property_path]
@@ -100,7 +100,7 @@ def run_mpsparser(mps_binary, network_path, expected_result, arguments=None):
     :param marabou_binary: path to marabou executable
     :param network_path: path to nnet file to pass too marabou
     :param property_path: path to property file to pass to marabou to verify
-    :param expected_result: SAT / UNSAT
+    :param expected_result: sat / unsat
     :param arguments list of arguments to pass to Marabou (for example DnC mode)
     :return: True / False if test pass or not
     '''
@@ -109,7 +109,7 @@ def run_mpsparser(mps_binary, network_path, expected_result, arguments=None):
             '"{}" does not exist or is not executable'.format(mps_binary))
     if not os.path.isfile(network_path):
         sys.exit('"{}" does not exist or is not a file'.format(network_path))
-    if expected_result not in {'SAT', 'UNSAT'}:
+    if expected_result not in {'sat', 'unsat'}:
         sys.exit('"{}" is not a marabou supported result'.format(expected_result))
 
     args = [mps_binary, network_path]
diff --git a/src/common/FloatUtils.cpp b/src/common/FloatUtils.cpp
index d19b536ac..5fc82baa8 100644
--- a/src/common/FloatUtils.cpp
+++ b/src/common/FloatUtils.cpp
@@ -15,7 +15,6 @@
 
 #include "FloatUtils.h"
 #include <iomanip>
-#include <math.h>
 #include <sstream>
 
 // https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/
@@ -39,81 +38,6 @@ bool FloatUtils::areEqual( double x, double y, double epsilon )
     return false;
 }
 
-double FloatUtils::abs( double x )
-{
-    return fabs( x );
-}
-
-bool FloatUtils::areDisequal( double x, double y, double epsilon )
-{
-    return !areEqual( x, y, epsilon );
-}
-
-bool FloatUtils::isZero( double x, double epsilon )
-{
-    return ( -epsilon <= x ) && ( x <= epsilon );
-}
-
-double FloatUtils::roundToZero( double x, double epsilon )
-{
-    return isZero( x, epsilon ) ? 0.0 : x;
-}
-
-bool FloatUtils::isPositive( double x, double epsilon )
-{
-    return ( !isZero( x, epsilon ) ) && ( x > 0.0 );
-}
-
-bool FloatUtils::isNegative( double x, double epsilon )
-{
-    return ( !isZero( x, epsilon ) ) && ( x < 0.0 );
-}
-
-bool FloatUtils::isFinite( double x )
-{
-    return ( x != infinity() ) && ( x != negativeInfinity() );
-}
-
-bool FloatUtils::gt( double x, double y, double epsilon )
-{
-    return isPositive( x - y, epsilon );
-}
-
-bool FloatUtils::gte( double x, double y, double epsilon )
-{
-    return !isNegative( x - y, epsilon );
-}
-
-bool FloatUtils::lt( double x, double y, double epsilon )
-{
-    return gt( y, x, epsilon );
-}
-
-bool FloatUtils::lte( double x, double y, double epsilon )
-{
-    return gte( y, x, epsilon );
-}
-
-double FloatUtils::min( double x, double y, double epsilon )
-{
-    return lt( x, y, epsilon ) ? x : y;
-}
-
-double FloatUtils::max( double x, double y, double epsilon )
-{
-    return gt( x, y, epsilon ) ? x : y;
-}
-
-double FloatUtils::infinity()
-{
-    return DBL_MAX;
-}
-
-double FloatUtils::negativeInfinity()
-{
-    return -DBL_MAX;
-}
-
 String FloatUtils::doubleToString( double x, unsigned precision )
 {
     std::ostringstream strout;
@@ -128,11 +52,6 @@ String FloatUtils::doubleToString( double x, unsigned precision )
     return str;
 }
 
-bool FloatUtils::wellFormed( double x )
-{
-    return !isNan( x ) && !isInf( x );
-}
-
 bool FloatUtils::isNan( double x )
 {
     return isnan( x );
diff --git a/src/common/FloatUtils.h b/src/common/FloatUtils.h
index aa62572d0..ed1d9075a 100644
--- a/src/common/FloatUtils.h
+++ b/src/common/FloatUtils.h
@@ -16,10 +16,12 @@
 #ifndef __FloatUtils_h__
 #define __FloatUtils_h__
 
+#include "Debug.h"
 #include "GlobalConfiguration.h"
 #include "MString.h"
 
 #include <cfloat>
+#include <math.h>
 
 #ifdef _WIN32
 #undef max
@@ -30,28 +32,97 @@ class FloatUtils
 {
 public:
     static bool areEqual( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static double abs( double x );
-    static bool areDisequal( double x,
-                             double y,
-                             double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static bool isZero( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static double roundToZero( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static bool isPositive( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static bool isNegative( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static bool gt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static bool gte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static bool lt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static bool lte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static double min( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static double max( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS );
-    static double infinity();
-    static double negativeInfinity();
-    static bool isFinite( double x );
     static String doubleToString( double x,
                                   unsigned precision = GlobalConfiguration::DEFAULT_DOUBLE_TO_STRING_PRECISION );
-    static bool wellFormed( double x );
+
     static bool isNan( double x );
+
     static bool isInf( double x );
+
+    static bool isZero( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return ( -epsilon <= x ) && ( x <= epsilon );
+    }
+
+    static bool isPositive( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        ASSERT( epsilon > 0 ); 
+        return x > epsilon;
+    }
+
+    static bool isNegative( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        ASSERT( epsilon > 0 ); 
+        return x < -epsilon;
+    }
+
+    static double abs( double x )
+    {
+        return fabs( x );
+    }
+
+    static bool areDisequal( double x,
+                             double y,
+                             double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return !areEqual( x, y, epsilon );
+    }
+
+    static double roundToZero( double x, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return isZero( x, epsilon ) ? 0.0 : x;
+    }
+
+    static bool gt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return isPositive( x - y, epsilon );
+    }
+
+    static bool gte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return !isNegative( x - y, epsilon );
+    }
+
+    static bool lt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return gt( y, x, epsilon );
+    }
+
+    static bool lte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return gte( y, x, epsilon );
+    }
+
+    static double min( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return lt( x, y, epsilon ) ? x : y;
+    }
+
+    static double max( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )
+    {
+        return gt( x, y, epsilon ) ? x : y;
+    }
+
+    static double infinity()
+    {
+        return DBL_MAX;
+    }
+
+    static double negativeInfinity()
+    {
+        return -DBL_MAX;
+    }
+
+    static bool isFinite( double x )
+    {
+        return ( x != infinity() ) && ( x != negativeInfinity() );
+    }
+
+    static bool wellFormed( double x )
+    {
+        return !isNan( x ) && !isInf( x );
+    }
+
 };
 
 #endif // __FloatUtils_h__
diff --git a/src/engine/DnCManager.cpp b/src/engine/DnCManager.cpp
index a6ad65c8a..b8dcfd814 100644
--- a/src/engine/DnCManager.cpp
+++ b/src/engine/DnCManager.cpp
@@ -215,9 +215,9 @@ String DnCManager::getResultString()
     switch ( _exitCode )
     {
     case DnCManager::SAT:
-        return "SAT";
+        return "sat";
     case DnCManager::UNSAT:
-        return "UNSAT";
+        return "unsat";
     case DnCManager::ERROR:
         return "ERROR";
     case DnCManager::NOT_DONE:
@@ -252,7 +252,7 @@ void DnCManager::printResult()
     {
     case DnCManager::SAT:
     {
-        std::cout << "SAT\n" << std::endl;
+        std::cout << "sat\n" << std::endl;
 
         ASSERT( _engineWithSATAssignment != nullptr );
 
@@ -288,7 +288,7 @@ void DnCManager::printResult()
         break;
     }
     case DnCManager::UNSAT:
-        std::cout << "UNSAT" << std::endl;
+        std::cout << "unsat" << std::endl;
         break;
     case DnCManager::ERROR:
         std::cout << "ERROR" << std::endl;
diff --git a/src/engine/DnCWorker.cpp b/src/engine/DnCWorker.cpp
index 58f456c7b..17bea6ec0 100644
--- a/src/engine/DnCWorker.cpp
+++ b/src/engine/DnCWorker.cpp
@@ -170,9 +170,9 @@ String DnCWorker::exitCodeToString( IEngine::ExitCode result )
     switch ( result )
     {
     case IEngine::UNSAT:
-        return "UNSAT";
+        return "unsat";
     case IEngine::SAT:
-        return "SAT";
+        return "sat";
     case IEngine::ERROR:
         return "ERROR";
     case IEngine::TIMEOUT:
diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
index fc48b43e8..606643c91 100644
--- a/src/engine/Engine.cpp
+++ b/src/engine/Engine.cpp
@@ -217,7 +217,7 @@ bool Engine::solve( unsigned timeoutInSeconds )
                     {
                         if ( _verbosity > 0 )
                         {
-                            printf( "Before declaring SAT, recomputing...\n" );
+                            printf( "Before declaring sat, recomputing...\n" );
                         }
                         // Make sure that the assignment is precise before declaring success
                         _tableau->computeAssignment();
@@ -225,7 +225,7 @@ bool Engine::solve( unsigned timeoutInSeconds )
                     }
                     if ( _verbosity > 0 )
                     {
-                        printf( "\nEngine::solve: SAT assignment found\n" );
+                        printf( "\nEngine::solve: sat assignment found\n" );
                         _statistics.print();
                     }
                     _exitCode = Engine::SAT;
@@ -287,7 +287,7 @@ bool Engine::solve( unsigned timeoutInSeconds )
             {
                 if ( _verbosity > 0 )
                 {
-                    printf( "\nEngine::solve: UNSAT query\n" );
+                    printf( "\nEngine::solve: unsat query\n" );
                     _statistics.print();
                 }
                 _exitCode = Engine::UNSAT;
diff --git a/src/engine/Marabou.cpp b/src/engine/Marabou.cpp
index 2ddd52ab3..3419656a2 100644
--- a/src/engine/Marabou.cpp
+++ b/src/engine/Marabou.cpp
@@ -135,13 +135,13 @@ void Marabou::displayResults( unsigned long long microSecondsElapsed ) const
 
     if ( result == Engine::UNSAT )
     {
-        resultString = "UNSAT";
-        printf( "UNSAT\n" );
+        resultString = "unsat";
+        printf( "unsat\n" );
     }
     else if ( result == Engine::SAT )
     {
-        resultString = "SAT";
-        printf( "SAT\n" );
+        resultString = "sat";
+        printf( "sat\n" );
 
         printf( "Input assignment:\n" );
         for ( unsigned i = 0; i < _inputQuery.getNumInputVariables(); ++i )
diff --git a/src/input_parsers/mps_example/main.cpp b/src/input_parsers/mps_example/main.cpp
index 4dff63b15..bf856773f 100644
--- a/src/input_parsers/mps_example/main.cpp
+++ b/src/input_parsers/mps_example/main.cpp
@@ -41,11 +41,11 @@ int main( int argc, char *argv[] )
 
     if ( !preprocess || !engine.solve() )
     {
-        printf( "UNSAT\n" );
+        printf( "unsat\n" );
         return 0;
     }
 
-    printf( "SAT\n" );
+    printf( "sat\n" );
 
     // Uncomment the below to print the solution