From 1dcbde4ecb5ee77e958108fdd408506d63a228d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 May 2020 19:55:39 -0700 Subject: [PATCH] fix #4401 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 64da45a3d..18fc25555 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -538,6 +538,8 @@ namespace smt { CTRACE("internalize_quantifier_zero", q->get_weight() == 0, tout << mk_pp(q, m) << "\n";); SASSERT(gate_ctx); // limitation of the current implementation SASSERT(!b_internalized(q)); + if (!is_forall(q)) + throw default_exception("internalization of exists is not supported"); SASSERT(is_forall(q)); SASSERT(check_patterns(q)); bool_var v = mk_bool_var(q);