diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f29e03380..62bf7e974 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret, PARSER_STATE->getUnresolvedSorts().clear(); - ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]); + ret = api::Sort(SOLVER, datatypeTypes[0]); }; // SyGuS grammar term. @@ -1798,7 +1798,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] if (Datatype::datatypeOf(ef).isParametric()) { type = api::Sort( - PARSER_STATE->getSolver(), + SOLVER, Datatype::datatypeOf(ef)[Datatype::indexOf(ef)] .getSpecializedConstructorType(expr.getSort().getType())); } @@ -2521,7 +2521,8 @@ constructorDef[CVC4::api::DatatypeDecl& type] } : symbol[id,CHECK_NONE,SYM_VARIABLE] { - ctor = new api::DatatypeConstructorDecl(id); + ctor = new api::DatatypeConstructorDecl( + SOLVER->mkDatatypeConstructorDecl(id)); } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* { // make the constructor |