diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-20 18:40:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-20 18:40:40 -0500 |
commit | bf863b1f3cee791585e2c04e5f40afcadcdf113c (patch) | |
tree | 28d4912780a9396733542bbbdf97bd5eb62c40fc /src/parser/smt2 | |
parent | a0c5a51f6fae81ffeb1752ee4d75db7a51c23680 (diff) |
Remove support for prototype (non-sygus) synthesis (#2338)
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6491856a5..5e068948f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2435,8 +2435,9 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] PARSER_STATE->warning(ss.str()); } // do nothing - } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" || - attr==":sygus" || attr==":synthesis") { + } + else if (attr==":axiom" || attr==":conjecture" || attr==":fun-def") + { if(hasValue) { std::stringstream ss; ss << "warning: Attribute " << attr |