diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 686d838b2..2670dfa9a 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -1816,7 +1816,7 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[],
         vs = [vs]
     num_vars = len(vs)
     if num_vars == 0:
-        raise Z3Exception("Quantification requires a non-empty list of variables.")
+        return body
     _vs = (Ast * num_vars)()
     for i in range(num_vars):
         ## TODO: Check if is constant
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 13999222f..18e8879e9 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -322,6 +322,9 @@ namespace smt {
         TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m_manager) << "\n";);
         TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m_manager) << "\n";);
         if (m_manager.is_bool(n)) {
+            if (is_var(n)) {
+                throw default_exception("Formulas should not contain unbound variables");
+            }
             SASSERT(is_quantifier(n) || is_app(n));
             internalize_formula(n, gate_ctx);
         }