diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index dc57be11e..0cce030b0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -585,6 +585,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] ( SYNTH_FUN_V1_TOK { isInv = false; } | SYNTH_INV_V1_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); } ) + { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK ( sortSymbol[range,CHECK_DECLARED] )? @@ -606,6 +607,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] ( SYNTH_FUN_TOK { isInv = false; } | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); } ) + { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK ( sortSymbol[range,CHECK_DECLARED] )? |