diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0cce030b0..a5033278d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1054,21 +1054,21 @@ sygusGrammar[CVC4::Type & ret, // grammar. This results in the error below. // We can also be in a case where the only rule specified was // (Constant T), in which case we have not yet added a constructor. We - // ensure an arbitrary constant is added in this case. - if (datatypes[i].getNumConstructors() == 0) + // ensure an arbitrary constant is added in this case. We additionally + // add a constant if the grammar allows it regardless of whether the + // datatype has other constructors, since this ensures the datatype is + // well-founded (see 3423). + if (aci) { - if (aci) - { - Expr c = btt.mkGroundTerm(); - PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres); - } - else - { - std::stringstream se; - se << "Grouped rule listing for " << datatypes[i].getName() - << " produced an empty rule list."; - PARSER_STATE->parseError(se.str()); - } + Expr c = btt.mkGroundTerm(); + PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres); + } + else if (datatypes[i].getNumConstructors() == 0) + { + std::stringstream se; + se << "Grouped rule listing for " << datatypes[i].getName() + << " produced an empty rule list."; + PARSER_STATE->parseError(se.str()); } } // pop scope from the pre-declaration |