From d60204229552bc9009f86c6fbc809dbd42dd6ef4 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 18 Apr 2016 16:06:45 -0700
Subject: [PATCH] More fixes for python interface

---
 src/expr/expr.i         | 7 +++++++
 src/expr/expr_manager.i | 5 +++--
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/expr/expr.i b/src/expr/expr.i
index b50686f52..ae8b85560 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -130,7 +130,14 @@ namespace CVC4 {
 
 %include "expr/expr.h"
 
+#ifdef SWIGPYTHON
+/* The python bindings on Mac OS X have trouble with this one - leave it
+ * out for now. */
+*/
+//%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
+#else
 %template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
+#endif
 %template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>;
 %template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>;
 %template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>;
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 0158df3bd..11c1e284d 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -40,7 +40,6 @@
 
 %include "expr/expr_manager.h"
 
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::ArrayStoreAll>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
@@ -83,15 +82,17 @@
 %template(mkBoolConst) CVC4::ExprManager::mkConst<bool>;
 
 // These cases have trouble too.  Remove them for now.
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
 //%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
 //%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
 //%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
 
 #else
-%template(mkConst) CVC4::ExprManager::mkConst<bool>;		  %template(mkConst) CVC4::ExprManager::mkConst<bool>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
+%template(mkConst) CVC4::ExprManager::mkConst<bool>;
 #endif
 
 %include "expr/expr_manager.h"
-- 
2.30.2