From 3ab0db55341e7e752411bb003fb203fcd9ec9120 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 24 Nov 2017 19:08:41 -0600
Subject: (Refactor) Instantiate utility (#1387)

---
 src/theory/quantifiers/term_database.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/theory/quantifiers/term_database.cpp')

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5db58067f..19cdc68e5 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -186,7 +186,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
                    << std::endl;
     if (options::instMaxLevel() != -1)
     {
-      QuantifiersEngine::setInstantiationLevelAttr(k, 0);
+      QuantAttributes::setInstantiationLevelAttr(k, 0);
     }
     d_type_fv[tn] = k;
     return k;
-- 
cgit v1.2.3