diff --git a/src/util/debug.h b/src/util/debug.h
index 9ad55a7c2..795976eac 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -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_)