diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 7657fb347..89615e11e 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1898,13 +1898,17 @@ def is_quantifier(a):
 
 def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
     if __debug__:
-        _z3_assert(is_bool(body), "Z3 expression expected")
+        _z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected")
         _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)")
         _z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
-        _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
-    ctx = body.ctx
+        _z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")    
     if is_app(vs):
+        ctx = vs.ctx
         vs = [vs]
+    else:
+        ctx = vs[0].ctx
+    if not is_expr(body):
+       body = BoolVal(body, ctx)
     num_vars = len(vs)
     if num_vars == 0:
         return body
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index ddca84922..861a31cfb 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -46,7 +46,6 @@ Revision History:
 #endif
 
 
-#if 1
 #include <immintrin.h> 
 
 #if defined(__GNUC__)
@@ -69,14 +68,6 @@ inline uint64_t _trailing_zeros64(uint64_t x) {
 }
 #endif
 
-#else
-
-inline unsigned _trailing_zeros32(unsigned x) {
-    unsigned r = 0;
-    for (; 0 == (x & 1) && r < 32; ++r, x >>= 1);
-    return r;
-}
-#endif
 
 #define _bit_min(x, y) (y + ((x - y) & ((int)(x - y) >> 31)))
 #define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31)))