1 files changed, 12 insertions, 6 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 29bbc6a2c..c418d0fb1 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -12,17 +12,19 @@
  ** \brief Implementation of abstract MBQI builder
  **/
 
-
-#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ambqi_builder.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
 
 void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) {
   d_def.clear();
@@ -807,7 +809,7 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
     }
     if( fapps.empty() ){
       //choose arbitrary value
-      Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+      Node mbt = fm->getModelBasisOpTerm(f);
       Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
       fapps.push_back( mbt );
     }
@@ -958,3 +960,7 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod
     return true;
   }
 }
+
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */