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

address #1167

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-27 07:44:08 -07:00
parent 1a07c6c188
commit 2cc6baede5
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2238,6 +2238,9 @@ namespace smt2 {
m_assert_expr = m_scanner.cached_str(0, m_cache_end); m_assert_expr = m_scanner.cached_str(0, m_cache_end);
m_scanner.stop_caching(); m_scanner.stop_caching();
} }
if (expr_stack().empty()) {
throw cmd_exception("invalid assert command, expression required as argument");
}
expr * f = expr_stack().back(); expr * f = expr_stack().back();
if (!m().is_bool(f)) if (!m().is_bool(f))
throw cmd_exception("invalid assert command, term is not Boolean"); throw cmd_exception("invalid assert command, term is not Boolean");