support for quantifiers macros, bug fix for bug 454 involving E-matching Array select terms (thanks for the bug report Francois)

1 files changed, 1 insertions, 8 deletions

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 41ebb63d2..c8f843c90 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -92,14 +92,7 @@ public:
   /** get */
   Node get( TNode var ) { return d_map[var]; }
   /** set */
-  void set(TNode var, TNode n){
-    //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ;
-    Assert( !var.isNull() );
-    Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
-            //var.getType() == n.getType()
-            n.getType().isSubtypeOf( var.getType() ) );
-    d_map[var] = n;
-  }
+  void set(TNode var, TNode n);
   size_t size(){ return d_map.size(); }
   /* iterator */
   std::map< Node, Node >::iterator begin(){ return d_map.begin(); };