summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus_grammar_red.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus_grammar_red.h')
-rw-r--r--src/theory/quantifiers/sygus_grammar_red.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus_grammar_red.h b/src/theory/quantifiers/sygus_grammar_red.h
index b65a12da2..d0484aa57 100644
--- a/src/theory/quantifiers/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus_grammar_red.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
#include <map>
#include "theory/quantifiers_engine.h"
@@ -116,4 +116,4 @@ class SygusRedundantCons
} /* CVC4::theory namespace */
} /* CVC4 namespace */
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback