diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 650ad91bb..f24a4cbba 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1007,6 +1007,11 @@ namespace qe { break; } case AST_QUANTIFIER: { + if (is_lambda(e)) { + visited.insert(e, e); + todo.pop_back(); + break; + } SASSERT(!is_lambda(e)); app_ref_vector vars(m); quantifier* q = to_quantifier(e);