diff options
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 62bf7e974..ec3e874df 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1990,7 +1990,7 @@ qualIdentifier[CVC4::ParseOp& p] | LPAREN_TOK AS_TOK ( CONST_TOK sortSymbol[type, CHECK_DECLARED] { - p.d_kind = api::STORE_ALL; + p.d_kind = api::CONST_ARRAY; PARSER_STATE->parseOpApplyTypeAscription(p, type); } | identifier[p] diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 608e47a6b..3f25e3776 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1535,7 +1535,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type << std::endl; // (as const (Array T1 T2)) - if (p.d_kind == api::STORE_ALL) + if (p.d_kind == api::CONST_ARRAY) { if (!type.isArray()) { @@ -1701,7 +1701,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) // Second phase: apply the arguments to the parse op const Options& opts = d_solver->getExprManager()->getOptions(); // handle special cases - if (p.d_kind == api::STORE_ALL && !p.d_type.isNull()) + if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull()) { if (args.size() != 1) { |