#pragma once

void __VERIFIER_ASSERT_MAX_LEAKAGE(int max);
void __VERIFIER_ASSUME_LEAKAGE(int assumedLeakage);
void benign();
#define BENIGN benign()