summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/theory_quantifiers.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 64160dc71..00a358e5f 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -43,6 +43,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
out.handleUserAttribute( "conjecture", this );
out.handleUserAttribute( "fun-def", this );
out.handleUserAttribute( "sygus", this );
+ out.handleUserAttribute( "sygus-synth-fun", 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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback