mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

DRAT debugging updates

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-22 15:38:57 -08:00
parent 6d0b89a989
commit 797f50e699
6 changed files with 19 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -541,8 +541,6 @@ namespace smt2 {
unsigned epos = sexpr_stack().size();
SASSERT(epos >= spos);
unsigned num = epos - spos;
if (num == 0)
throw parser_exception("invalid empty s-expression");
sexpr * r = sm().mk_composite(num, sexpr_stack().c_ptr() + spos, line, pos);
sexpr_stack().shrink(spos);
sexpr_stack().push_back(r);