diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index 0a9ef1ed30324d9b7d2717442aa57719686eb1f7..2491e553decb42ff0b6f28e7405941079873e687 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -54,7 +54,7 @@ bool Formula<ModalValueType>::check_satisfiability(bdd b){
 	//bdd_printdot(b);
 	bdd_allsat(b, sat_handler); // pushes satisfying assignment onto stack
 	vector<SatisfyingAssignment> sat_ass = sat_ass_stack; 
-	sat_ass_stack.clear();	
+	sat_ass_stack.clear();
 	for(unsigned int i=0; i < sat_ass.size() && !sat; i++){ // we break if proved sat
 		sat = apply_rules(sat_ass[i]);
 	}
diff --git a/GMLMIP-0.1/main.cpp b/GMLMIP-0.1/main.cpp
index 1e886207118221367226f14c1523766962f890b4..c4a5098ca02f274407898f43bd284751c0e771af 100644
--- a/GMLMIP-0.1/main.cpp
+++ b/GMLMIP-0.1/main.cpp
@@ -33,18 +33,18 @@ int main (int argc, char *argv[]){
 	bdd_error_hook(error_handler);
 	parse(f, argc, argv, verbose);
 	if(f){
-	// bdd_varblockall();
-	// bdd_reorder(BDD_REORDER_WIN3ITE);
-	// bdd_printdot((driver.formula)->bdd_rep);
-	//bdd_printset(f->get_bdd());
-	//cout << endl;
-	//(driver.formula)->print_back_vars();
-	if(f->satisfiability(verbose))
-		cout << "Satisfiable" << endl;
-	else
-		cout << "Unsatisfiable" << endl;
-	f->clear_maps();
-	delete f;
+		// bdd_varblockall();
+		// bdd_reorder(BDD_REORDER_WIN3ITE);
+		// bdd_printdot((driver.formula)->bdd_rep);
+		//bdd_printset(f->get_bdd());
+		//cout << endl;
+		//(driver.formula)->print_back_vars();
+		if(f->satisfiability(verbose))
+			cout << "Satisfiable" << endl;
+		else
+			cout << "Unsatisfiable" << endl;
+		f->clear_maps();
+		delete f;
 	}
 	bdd_done();
 	total_time = clock() - total_time;
@@ -67,4 +67,3 @@ void parse(IFormula* &formula, int argc, char *argv[], int& option){
 			driver.extract_formula(formula);
 }
 
-