1 files changed, 10 insertions, 0 deletions
diff --git a/src/options/options.i b/src/options/options.i
new file mode 100644
index 000000000..25eecaf2d
--- /dev/null
+++ b/src/options/options.i
@@ -0,0 +1,10 @@
+%{
+#include "options/options.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, SimplificationMode);
+%ignore CVC4::operator<<(std::ostream&, ArithPivotRule);
+
+%apply char** STRING_ARRAY { char* argv[] }
+%include "options/options.h"
+%clear char* argv[];