summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-08-20 18:40:40 -0500
committerGitHub <noreply@github.com>2018-08-20 18:40:40 -0500
commitbf863b1f3cee791585e2c04e5f40afcadcdf113c (patch)
tree28d4912780a9396733542bbbdf97bd5eb62c40fc /src/parser/smt2/Smt2.g
parenta0c5a51f6fae81ffeb1752ee4d75db7a51c23680 (diff)
Remove support for prototype (non-sygus) synthesis (#2338)
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g5
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback