From cd373527ffbad928273a6433771155fa494fcbc7 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 27 Jul 2023 16:54:59 +0200 Subject: [PATCH] static_assert --- src/util/sat_literal.h | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/util/sat_literal.h b/src/util/sat_literal.h index eb4c16705c7..58088e6281a 100644 --- a/src/util/sat_literal.h +++ b/src/util/sat_literal.h @@ -39,12 +39,7 @@ namespace sat { class literal { unsigned m_val; public: - constexpr literal(): m_val(null_bool_var << 1) { -#ifdef Z3DEBUG - assert(var() == null_bool_var); - assert(!sign()); -#endif - } + constexpr literal(): m_val(null_bool_var << 1) { } explicit literal(bool_var v, bool _sign = false): m_val((v << 1) + static_cast(_sign)) { @@ -90,6 +85,9 @@ namespace sat { }; inline constexpr literal null_literal; + static_assert(null_literal.var() == null_bool_var); + static_assert(!null_literal.sign()); + using literal_hash = obj_hash; inline literal to_literal(unsigned x) { literal l; l.m_val = x; return l; }