summaryrefslogtreecommitdiff
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/cvc4_check.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/base/cvc4_check.h b/src/base/cvc4_check.h
index 703931108..b18e62303 100644
--- a/src/base/cvc4_check.h
+++ b/src/base/cvc4_check.h
@@ -55,11 +55,14 @@
#ifdef __has_builtin
#if __has_builtin(__builtin_expect)
#define CVC4_PREDICT_FALSE(x) (__builtin_expect(x, false))
+#define CVC4_PREDICT_TRUE(x) (__builtin_expect(x, true))
#else
#define CVC4_PREDICT_FALSE(x) x
+#define CVC4_PREDICT_TRUE(x) x
#endif
#else
#define CVC4_PREDICT_FALSE(x) x
+#define CVC4_PREDICT_TRUE(x) x
#endif
namespace CVC4 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback