From 0df4931c4b5cfc42358d7063806309a219fee03a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jan 2016 15:43:47 -0800 Subject: [PATCH] dealing with issue #402 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- src/smt/smt_internalizer.cpp | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) 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); }