mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

Add SASSERT_EQ and VERIFY_EQ

Browse source
This commit is contained in:
Jakob Rath 2022-08-01 12:04:57 +02:00 • committed by Nikolaj Bjorner
parent 79ee543d25
commit d2fe174320
1 changed files with 15 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/util/debug.h
View file

@ -63,6 +63,13 @@ bool is_debug_enabled(const char * tag);
#define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
#define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
#define SASSERT_EQ(LHS, RHS) \
DEBUG_CODE(if (assertions_enabled() && !((LHS) == (RHS))) { \
notify_assertion_violation(__FILE__, __LINE__, #LHS " == " #RHS); \
std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n"; \
INVOKE_DEBUGGER(); \
})
#ifdef Z3DEBUG
# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();)
#else
@ -78,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_)