diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h
index 1cc5022848..8ec3f26c8c 100644
--- a/src/util/rb_tree.h
+++ b/src/util/rb_tree.h
@@ -71,10 +71,7 @@ class rb_tree : private CMP {
     }
 
     bool check_cmp_result(T const & v1, T const & v2) const {
-        DEBUG_CODE(
-            int n1 = CMP::operator()(v1, v2);
-            int n2 = CMP::operator()(v2, v1);
-            );
+        DEBUG_CODE(int n1 = CMP::operator()(v1, v2); int n2 = CMP::operator()(v2, v1););
         lean_assert((n1 < 0  && n2 > 0) || (n1 == 0 && n2 == 0) || (n1 > 0  && n2 < 0));
         return true;
     }