fn write_guard_conjunction<T: Types>( encoder: &SmtEncoder<T>, guards: &[&Pred<T>], out: &mut impl Write, ) -> Result