diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index 1e95ed08c63c51061732198d32ef0a8affa0688e..843211081e4f17505c58867fafebd95cfc349a70 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -23,6 +23,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
    * The formula counterpart of [[PredicateLabel]].
    */
   sealed case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
+    require(label.arity == args.size)
     override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
 
     override def constantPredicates: Set[ConstantPredicateLabel] = label match {
@@ -42,6 +43,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
    * The formula counterpart of [[ConnectorLabel]].
    */
   sealed case class ConnectorFormula(label: ConnectorLabel, args: Seq[Formula]) extends Formula {
+    require(label.arity == -1 || label.arity == args.length)
     override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
 
     override def constantFunctions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions)
diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
index 33f62829dfcd6905417bc6592845310c925ff59f..771f392a11418522539fe1d7215446d119b719f5 100644
--- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
+++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala
@@ -38,7 +38,7 @@ class PrinterTest extends AnyFunSuite {
 
     assert(prettyFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀x. ∃y. ∃!z. a")
 
-    assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(?x, ?y, ?z)")
+    assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 3), Seq(x, y, z))) == "f(?x, ?y, ?z)")
   }
 
 }