diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 33674770d..740e35ba4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1868,12 +1868,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] << f2 << " " << type << std::endl; expr = MK_CONST( ::CVC4::EmptySet(type) ); } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) { - expr = EXPR_MANAGER->mkUniqueVar(type, kind::UNIVERSE_SET); + expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET); } else if(f.getKind() == CVC4::kind::SEP_NIL) { //We don't want the nil reference to be a constant: for instance, it //could be of type Int but is not a const rational. However, the //expression has 0 children. So we convert to a SEP_NIL variable. - expr = EXPR_MANAGER->mkUniqueVar(type, kind::SEP_NIL); + expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL); } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -2304,11 +2304,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | UNIVSET_TOK { //booleanType is placeholder here since we don't have type info without type annotation - expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } + expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } | NILREF_TOK { //booleanType is placeholder here since we don't have type info without type annotation - expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } + expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } // NOTE: Theory constants go here ; |