mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

remove limiting error mode #6600

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-20 12:16:43 -08:00
parent 755b517001
commit 4aa05b2b57
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/parsers/smt2/smt2parser.cpp
View file

@ -2640,8 +2640,6 @@ namespace smt2 {
check_lparen_next("invalid get-value command, '(' expected"); check_lparen_next("invalid get-value command, '(' expected");
while (!curr_is_rparen()) { while (!curr_is_rparen()) {
parse_expr(); parse_expr();
if (!is_ground(expr_stack().back()))
throw cmd_exception("invalid get-value term, term must be ground and must not contain quantifiers");
m_cached_strings.push_back(m_scanner.cached_str(cache_it, m_cache_end)); m_cached_strings.push_back(m_scanner.cached_str(cache_it, m_cache_end));
cache_it = m_cache_end; cache_it = m_cache_end;
} }
@ -2680,7 +2678,7 @@ namespace smt2 {
m_ctx.regular_stream() << "\n "; m_ctx.regular_stream() << "\n ";
m_ctx.regular_stream() << "(" << m_cached_strings[i] << " "; m_ctx.regular_stream() << "(" << m_cached_strings[i] << " ";
m_ctx.display(m_ctx.regular_stream(), v); m_ctx.display(m_ctx.regular_stream(), v);
m_ctx.regular_stream() << ")"; m_ctx.regular_stream() << ")";
} }
m_ctx.regular_stream() << ")" << std::endl; m_ctx.regular_stream() << ")" << std::endl;
expr_stack().shrink(spos); expr_stack().shrink(spos);