diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
index 61eadc2..6893980 100644
--- a/src/translate/verify_properties.rs
+++ b/src/translate/verify_properties.rs
@@ -134,7 +134,7 @@ where
 				let scoped_formula = crate::ScopedFormula
 				{
 					free_variable_declarations: definitions.head_atom_parameters,
-					formula: Box::new(completed_definition),
+					formula: completed_definition,
 				};
 
 				crate::universal_closure(scoped_formula)
@@ -165,7 +165,7 @@ where
 				let scoped_formula = crate::ScopedFormula
 				{
 					free_variable_declarations: head_atom_parameters,
-					formula: Box::new(not),
+					formula: not,
 				};
 
 				crate::universal_closure(scoped_formula)
@@ -420,7 +420,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
 			let definition = crate::ScopedFormula
 			{
 				free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
-				formula: Box::new(definition),
+				formula: definition,
 			};
 
 			log::debug!("translated rule with single atom in head: {}",
@@ -454,7 +454,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
 			let scoped_formula = crate::ScopedFormula
 			{
 				free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
-				formula: Box::new(formula),
+				formula,
 			};
 
 			let integrity_constraint = crate::universal_closure(scoped_formula);
diff --git a/src/utils.rs b/src/utils.rs
index f8cb111..b17d0ab 100644
--- a/src/utils.rs
+++ b/src/utils.rs
@@ -39,16 +39,16 @@ impl std::fmt::Display for Domain
 pub(crate) struct ScopedFormula
 {
 	pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,
-	pub formula: Box<foliage::Formula>,
+	pub formula: foliage::Formula,
 }
 
 pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
 {
 	match scoped_formula.free_variable_declarations.is_empty()
 	{
-		true => *scoped_formula.formula,
+		true => scoped_formula.formula,
 		false => foliage::Formula::exists(scoped_formula.free_variable_declarations,
-			scoped_formula.formula),
+			Box::new(scoped_formula.formula)),
 	}
 }
 
@@ -56,9 +56,9 @@ pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> foliage
 {
 	match scoped_formula.free_variable_declarations.is_empty()
 	{
-		true => *scoped_formula.formula,
+		true => scoped_formula.formula,
 		false => foliage::Formula::for_all(scoped_formula.free_variable_declarations,
-			scoped_formula.formula),
+			Box::new(scoped_formula.formula)),
 	}
 }