diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8b7c0bda2..8dac9915e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -586,7 +586,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] ++i) { terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms); + Expr bvl; + if( !terms.empty() ){ + bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms); + } terms.clear(); terms.push_back(bvl); } @@ -633,8 +636,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL] PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); std::vector<Type> evalType; evalType.push_back(dtt); - for(size_t j = 0; j < terms[0].getNumChildren(); ++j) { - evalType.push_back(terms[0][j].getType()); + if( !terms[0].isNull() ){ + for(size_t j = 0; j < terms[0].getNumChildren(); ++j) { + evalType.push_back(terms[0][j].getType()); + } } evalType.push_back(sorts[i]); Expr eval = PARSER_STATE->mkVar(name, EXPR_MANAGER->mkFunctionType(evalType)); |