diff options
Diffstat (limited to 'src/parser/tptp/Tptp.g')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 5f078cab7..c96fbf07d 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -194,7 +194,11 @@ parseCommand returns [cvc5::Command* cmd = NULL] cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); } ) RPAREN_TOK DOT_TOK - | THF_TOK LPAREN_TOK nameN[name] COMMA_TOK + | THF_TOK + { + PARSER_STATE->setHol(); + } + LPAREN_TOK nameN[name] COMMA_TOK // Supported THF formulas: either a logic formula or a typing atom (i.e. we // ignore subtyping and logic sequents). Also, only TH0 ( TYPE_TOK COMMA_TOK thfAtomTyping[cmd] |