diff --git a/src/ast.rs b/src/ast.rs index 1a3c82a..b212278 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -502,6 +502,8 @@ impl Formula pub fn exists(parameters: std::rc::Rc, argument: Box) -> Self { + assert!(!parameters.is_empty()); + Self::Exists(Exists::new(parameters, argument)) } @@ -517,6 +519,8 @@ impl Formula pub fn for_all(parameters: std::rc::Rc, argument: Box) -> Self { + assert!(!parameters.is_empty()); + Self::ForAll(ForAll::new(parameters, argument)) } diff --git a/src/format.rs b/src/format.rs index 2ebfba3..925f976 100644 --- a/src/format.rs +++ b/src/format.rs @@ -205,6 +205,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> { crate::Formula::Exists(exists) => { + assert!(!exists.parameters.is_empty()); + write!(format, "exists")?; let mut separator = " "; @@ -220,6 +222,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula> }, crate::Formula::ForAll(for_all) => { + assert!(!for_all.parameters.is_empty()); + write!(format, "forall")?; let mut separator = " ";