diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 05160f8d1ba2a4f47254eee14c7dc740c35cd96a..62408579664a57852f1dfedb38bdefe45a448a8c 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -43,9 +43,7 @@ public:
     virtual void computeDSOG(LDDGraph &g) {};
 protected:
     void initializeLDD();
-
     void loadNetFromFile();
-
     const NewNet *m_net;
     int m_nbPlaces = 0;
     static LDDGraph *m_graph;
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
index 4bfe6fb68065f57b8f78e205868a7900b51aef3f..cfdbff634bbfd9461674e20f5ce74cb144a5e87e 100644
--- a/src/SylvanWrapper.cpp
+++ b/src/SylvanWrapper.cpp
@@ -815,16 +815,17 @@ bool SylvanWrapper::isFirable(MDD cmark, MDD minus) {
     MDD _cmark = cmark, _minus = minus;
     mddnode_t n_cmark = GETNODE(_cmark);
     mddnode_t n_minus = GETNODE(_minus);
+    std::cout<<(int)mddnode_getvalue(n_cmark)<<" \n";
     while (!result) {
         uint32_t value;
         value = mddnode_getvalue(n_cmark);
         uint32_t value_minus = mddnode_getvalue(n_minus);
 
         if (value >= value_minus) {
-            mddnode_t node_mark=mddnode_getdown(n_cmark);
-            if (node_mark==lddmc_true) return true;
-            mddnode_t node_minus=mddnode_getdown(n_minus);
-            result=isFirable(node_mark, mddnode_getdown(node_minus));
+            MDD _mark=mddnode_getdown(n_cmark);
+            if (_mark==lddmc_true) return true;
+            MDD _minus=mddnode_getdown(n_minus);
+            result=isFirable(_mark, _minus);
         }
         cmark = mddnode_getright(n_cmark);
         if (cmark == lddmc_false || result) return result;
diff --git a/src/main.cpp b/src/main.cpp
index 39da26a7b1e73fdd80981ea6292ef289e3b56791..dca15015588e8ce2511d48f237ad29f6d8db6a0c 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -1,4 +1,4 @@
-#include <time.h>
+#include <ctime>
 #include <chrono>
 #include <iostream>
 #include <string>
@@ -62,9 +62,9 @@ set<string> buildPropositions(const string &fileName) {
 		std::cerr << "Only LTL formulas are supported.\n";
 		return transitionSet;
 	}
-	spot::atomic_prop_set *p_list = spot::atomic_prop_collect(fo, 0);
-	for (spot::atomic_prop_set::const_iterator i = p_list->begin(); i != p_list->end(); i++) {
-		transitionSet.insert((*i).ap_name());
+	spot::atomic_prop_set *p_list = spot::atomic_prop_collect(fo, nullptr);
+	for (const auto i : *p_list) {
+		transitionSet.insert(i.ap_name());
 	}
 	print_spin_ltl(std::cout, fo) << '\n';
 	cout << "Building formula negation\n";
@@ -84,7 +84,7 @@ void displayTime(auto startTime,auto finalTime) {
 }
 /***********************************************/
 int main(int argc, char **argv) {
-	int choix;
+
 	if (argc < 3)
 		return 0;
 	char formula[100] = "";
@@ -159,14 +159,14 @@ int main(int argc, char **argv) {
                 }
                 auto startTime = std::chrono::steady_clock::now();
                 spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
-                bool res = (echptr->check() == 0);
+                bool res = (echptr->check() == nullptr);
                 auto finalTime = std::chrono::steady_clock::now();
                 displayTime(startTime, finalTime);
                 displayCheckResult(res);
 
             } else {
                 auto startTime = std::chrono::steady_clock::now();
-                bool res = (k->intersecting_run(af) == 0);
+                bool res = (k->intersecting_run(af) == nullptr);
                 auto finalTime = std::chrono::steady_clock::now();
                 displayTime(startTime, finalTime);
                 displayCheckResult(res);
@@ -304,13 +304,13 @@ int main(int argc, char **argv) {
                             cout<<"Spot emptiness check algorithm : "<<algorithm<<endl;
                         auto startTime = std::chrono::high_resolution_clock::now();
                         spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
-                        bool res = (echptr->check() == 0);
+                        bool res = (echptr->check() == nullptr);
                         auto finalTime = std::chrono::high_resolution_clock::now();
                         displayTime(startTime, finalTime);
                         displayCheckResult(res);
                     } else {
                         auto startTime = std::chrono::steady_clock::now();
-                        bool res = (k->intersecting_run(af) == 0);
+                        bool res = (k->intersecting_run(af) == nullptr);
                         auto finalTime = std::chrono::steady_clock::now();
                         displayTime(startTime, finalTime);
                         displayCheckResult(res);