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/theory/quantifiers/theory_quantifiers.cpp | |
| parent | a0c5a51f6fae81ffeb1752ee4d75db7a51c23680 (diff) | |
Remove support for prototype (non-sygus) synthesis (#2338)
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 842671a5e..2ab45aa96 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -47,7 +47,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output out.handleUserAttribute("quant-name", this); out.handleUserAttribute("sygus-synth-grammar", this); out.handleUserAttribute( "sygus-synth-fun-var-list", this ); - out.handleUserAttribute( "synthesis", this ); out.handleUserAttribute( "quant-inst-max-level", this ); out.handleUserAttribute( "rr-priority", this ); out.handleUserAttribute( "quant-elim", this ); |