#pragma once
#include <libsolutil/Assertions.h>
#include <libsolutil/Exceptions.h>
#include <boost/preprocessor/cat.hpp>
#include <boost/preprocessor/facilities/empty.hpp>
#include <boost/preprocessor/facilities/overload.hpp>
namespace solidity::smtutil
{
struct SMTLogicError: virtual util::Exception {};
#if !BOOST_PP_VARIADICS_MSVC
#define smtAssert(...) BOOST_PP_OVERLOAD(smtAssert_,__VA_ARGS__)(__VA_ARGS__)
#else
#define smtAssert(...) BOOST_PP_CAT(BOOST_PP_OVERLOAD(smtAssert_,__VA_ARGS__)(__VA_ARGS__),BOOST_PP_EMPTY())
#endif
#define smtAssert_1(CONDITION) \
smtAssert_2((CONDITION), "")
#define smtAssert_2(CONDITION, DESCRIPTION) \
assertThrowWithDefaultDescription( \
(CONDITION), \
::solidity::smtutil::SMTLogicError, \
(DESCRIPTION), \
"SMT assertion failed" \
)
}