diff --git a/solver/include/solver.h b/solver/include/solver.h
index 59ebc15..b87acc3 100644
--- a/solver/include/solver.h
+++ b/solver/include/solver.h
@@ -88,7 +88,7 @@ namespace CDCL
 
 		UnitPropagationStatus unit_propagate(std::vector<VariableValueDecision> &current_variables_stack);
 		void apply_new_variables(std::vector<VariableValueDecision> &current_variables_stack,
-		                         const std::unordered_map<int, CNF::Value> &value_by_id);;
+		                         const std::unordered_map<int, CNF::Value> &value_by_id);
 
 		void updateClausesValue();
 
diff --git a/solver/include/utils.h b/solver/include/utils.h
index 8f1a7b1..142d64d 100644
--- a/solver/include/utils.h
+++ b/solver/include/utils.h
@@ -10,7 +10,10 @@ namespace utils
 		T value;
 		bool has_value;
 
-		Maybe(T value = -1, bool hasValue = false) : value(value), has_value(hasValue)
+		explicit Maybe(T value) : value(value), has_value(true)
+		{}
+
+		Maybe() : has_value(false)
 		{}
 	};
 }
diff --git a/solver/src/CNF.cpp b/solver/src/CNF.cpp
index 0a4ca02..8922942 100644
--- a/solver/src/CNF.cpp
+++ b/solver/src/CNF.cpp
@@ -3,7 +3,7 @@
 utils::Maybe<CNF::Variable> CNF::Clause::get_maybe_updatable_variable_id() const
 {
 	if (isTrue) {
-		return utils::Maybe<CNF::Variable>(Variable(), false);
+		return {};
 	}
 	CNF::Variable var_with_val(-1, Value::Undefined);
 	for (const auto &literal : literals)
@@ -13,18 +13,14 @@ utils::Maybe<CNF::Variable> CNF::Clause::get_maybe_updatable_variable_id() const
 			if (var_with_val.value == Value::Undefined)
 			{
 				var_with_val.id = literal.var->id;
-				if (literal.has_negate) {
-					var_with_val.value = Value::False;
-				} else {
-					var_with_val.value = Value::True;
-				}
+                var_with_val.value = literal.has_negate ? Value::False : Value::True;
 				continue;
 			}
-			return utils::Maybe<Variable>(Variable(), false);
+			return {};
 		}
 	}
 
-	return utils::Maybe<CNF::Variable>(var_with_val, var_with_val.value != Value::Undefined);
+    return var_with_val.value != Value::Undefined ? utils::Maybe(var_with_val) : utils::Maybe<CNF::Variable>();
 }
 
 void CNF::Clause::update_clause_value()
@@ -33,21 +29,23 @@ void CNF::Clause::update_clause_value()
 	for (const auto &literal : literals) {
 		if (literal.get_value() == Value::True) {
 			isTrue = true;
+            break;
 		}
 	}
 }
 
 CNF::Value CNF::Literal::get_value() const
 {
-	if (var->value == Value::Undefined)
+    auto value = var->value;
+	if (value == Value::Undefined)
 	{
 		return Value::Undefined;
 	}
 	if (has_negate)
 	{
-		return var->value == Value::True ? Value::False : Value::True;
+		return value == Value::True ? Value::False : Value::True;
 	}
-	return var->value;
+	return value;
 }
 
 std::ostream &operator<<(std::ostream &out, const CNF::Variable &var)
@@ -55,7 +53,6 @@ std::ostream &operator<<(std::ostream &out, const CNF::Variable &var)
 	out << var.id << " = ";
 	switch (var.value)
 	{
-
 		case CNF::Value::False:
 			out << 0;
 			break;
diff --git a/solver/src/solver.cpp b/solver/src/solver.cpp
index 43fae79..f48cb84 100644
--- a/solver/src/solver.cpp
+++ b/solver/src/solver.cpp
@@ -34,13 +34,13 @@ namespace CDCL
 		std::vector<VariableValueDecision> current_variables_stack;
 		while (current_variables_stack.size() != variables.size())
 		{
-			auto PropagatingStatus = unit_propagate(current_variables_stack);
-			while (PropagatingStatus == Good) {
-				PropagatingStatus = unit_propagate(current_variables_stack);
-			}
-			if (PropagatingStatus == Bad) {
+			UnitPropagationStatus propagating_status;
+			do {
+                propagating_status = unit_propagate(current_variables_stack);
+			} while (propagating_status == Good);
+			if (propagating_status == Bad) {
 				if (!change_last_decision(current_variables_stack)) {
-					return {{}, false};
+					return {};
 				}
 				continue;
 			}
@@ -50,7 +50,6 @@ namespace CDCL
 			current_variables_stack.emplace_back(next_variable_id, false, false);
 			variables[next_variable_id]->value = CNF::Value::False;
 			updateClausesValue();
-
 		}
 
 
@@ -60,7 +59,7 @@ namespace CDCL
 			result.emplace_back(var_with_decision.var_id, var_with_decision.cur_value);
 		}
 
-		return {result, true};
+		return utils::Maybe(result);
 	}
 
 	Solver::UnitPropagationStatus Solver::unit_propagate(std::vector<VariableValueDecision> &current_variables_stack)
@@ -118,18 +117,19 @@ namespace CDCL
 	{
 		// This is like we are looking for the least ancestor which has more "righter" path
 		while (!current_variables_stack.empty()) {
-			if (current_variables_stack.back().isAutomaticallyDetermined) {
-				variables[current_variables_stack.back().var_id]->value = CNF::Value::Undefined;
+            auto &stack_back = current_variables_stack.back();
+            if (stack_back.isAutomaticallyDetermined) {
+				variables[stack_back.var_id]->value = CNF::Value::Undefined;
 				current_variables_stack.pop_back();
 				continue;
 			}
-			if (current_variables_stack.back().cur_value) {
-				variables[current_variables_stack.back().var_id]->value = CNF::Value::Undefined;
+			if (stack_back.cur_value) {
+				variables[stack_back.var_id]->value = CNF::Value::Undefined;
 				current_variables_stack.pop_back();
 				continue;
 			}
-			variables[current_variables_stack.back().var_id]->value = CNF::Value::True;
-			current_variables_stack.back().cur_value = true;
+			variables[stack_back.var_id]->value = CNF::Value::True;
+            stack_back.cur_value = true;
 			updateClausesValue();
 			return true;
 		}