1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 24a9f1bdf..668593842 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_epr.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
@@ -728,12 +729,15 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
     d_cbqi_set_quant_inactive = true;
     d_incomplete_check = true;
-    d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
+    d_quantEngine->getInstantiate()->recordInstantiation(
+        d_curr_quant, subs, false, false);
     return true;
   }else{
     //check if we need virtual term substitution (if used delta or infinity)
     bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false );
-    if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
+    if (d_quantEngine->getInstantiate()->addInstantiation(
+            d_curr_quant, subs, false, false, used_vts))
+    {
       ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
       //d_added_inst.insert( d_curr_quant );
       return true;