mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #5224

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-29 20:12:02 -07:00
parent e4b660321f
commit 381e502d30
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2569,7 +2569,7 @@ namespace smt2 {
throw cmd_exception("invalid assert command, expression required as argument"); 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 (!f || !m().is_bool(f)) {
TRACE("smt2parser", tout << expr_ref(f, m()) << "\n";); TRACE("smt2parser", tout << expr_ref(f, m()) << "\n";);
throw cmd_exception("invalid assert command, term is not Boolean"); throw cmd_exception("invalid assert command, term is not Boolean");
} }