1 files changed, 2 insertions, 9 deletions
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 906673903..e4f9529a8 100644..100755
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -57,15 +57,6 @@ public:
 
 
 
-/** Attribute true for nodes that should not be used when considered for inst-gen basis */
-struct BasisNoMatchAttributeId {};
-/** use the special for boolean flag */
-typedef expr::Attribute< BasisNoMatchAttributeId,
-                         bool,
-                         expr::attr::NullCleanupStrategy,
-                         true // context dependent
-                       > BasisNoMatchAttribute;
-
 class TermArgBasisTrie {
 private:
   bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
@@ -85,7 +76,9 @@ public:
   */
 class QModelBuilderIG : public QModelBuilder
 {
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
 protected:
+  BoolMap d_basisNoMatch;
   //map from operators to model preference data
   std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
   //built model uf