From 2dd9ea071d8471b4f6a48b5d731e4a73534a20f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Sep 2019 10:40:52 -0700 Subject: [PATCH] fix #2577 Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index dc3eefa06..470573714 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1951,7 +1951,7 @@ namespace smt2 { // the resultant expression is on the top of the stack TRACE("let_frame", tout << "let result expr: " << mk_pp(expr_stack().back(), m()) << "\n";); expr_ref r(m()); - if (expr_stack().empty()) + if (expr_stack().size() < fr->m_expr_spos + 1) throw parser_exception("invalid let expression"); r = expr_stack().back(); expr_stack().pop_back();