mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

VERIFY in test

Browse source
This commit is contained in:
Jakob Rath 2022-07-21 13:07:28 +02:00
parent 4a3fe8ab82
commit f762b66fe2
2 changed files with 89 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/util/debug.h
View file

@ -85,7 +85,14 @@ bool is_debug_enabled(const char * tag);
#define VERIFY(_x_) if (!(_x_)) { \
notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #_x_ "\n"); \
exit(ERR_UNREACHABLE); \
}
}
#define VERIFY_EQ(LHS, RHS) \
if (!((LHS) == (RHS))) { \
notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #LHS " == " #RHS "\n"); \
std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n"; \
exit(ERR_UNREACHABLE); \
}
#define ENSURE(_x_) VERIFY(_x_)