diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 081990a45..f29e03380 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1692,7 +1692,13 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] std::vector<api::Sort> argTypes; } : LPAREN_TOK quantOp[kind] - { PARSER_STATE->pushScope(true); } + { + if (!PARSER_STATE->isTheoryEnabled(theory::THEORY_QUANTIFIERS)) + { + PARSER_STATE->parseError("Quantifier used in non-quantified logic."); + } + PARSER_STATE->pushScope(true); + } boundVarList[bvl] term[f, f2] RPAREN_TOK { |