diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a5033278d..9110b9660 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -392,17 +392,6 @@ command [std::unique_ptr<CVC4::Command>* cmd] csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } - // if sygus, check whether it has a free variable - // this is because, due to the sygus format, one can write assertions - // that have free function variables in them - if (PARSER_STATE->sygus()) - { - if (expr.hasFreeVariable()) - { - PARSER_STATE->parseError("Assertion has free variable. Perhaps you " - "meant constraint instead of assert?"); - } - } } | /* check-sat */ CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } |