#include <Extension2_util.h>
#include <stdint.h>

int32_t Extension2_util_one() {
  return 1;
}