6 files changed, 3 insertions, 18 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index ea97513b8..e1fc9e793 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -141,9 +141,6 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 bool CegInstantiation::needsModel( Theory::Effort e ) {
   return true;
 }
-bool CegInstantiation::needsFullModel( Theory::Effort e ) {
-  return true;
-}
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 786db12a9..f5077ad04 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -119,7 +119,6 @@ public:
 public:
   bool needsCheck( Theory::Effort e );
   bool needsModel( Theory::Effort e );
-  bool needsFullModel( Theory::Effort e );
   /* Call during quantifier engine's check */
   void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c0a734c35..c3a723fce 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -325,15 +325,9 @@ QModelBuilder( c, qe ){
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
-bool FullModelChecker::optBuildAtFullModel() {
-  //need to build after full model has taken effect if we are constructing interval models
-  //  this is because we need to have a constant in all integer equivalence classes
-  return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL;
-}
-
 void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
-  if( fullModel==optBuildAtFullModel() ){
+  if( !fullModel ){
     Trace("fmc") << "---Full Model Check reset() " << std::endl;
     fm->initialize();
     d_quant_models.clear();
@@ -514,8 +508,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       }
       */
     }
-  }
-  if( fullModel ){
+  }else{
     //make function values
     for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
       m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 9a7b05090..29913d98d 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -135,9 +135,6 @@ public:
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );
   ~FullModelChecker() throw() {}
 
-  bool optBuildAtFullModel();
-
-
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
 
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 22dac2225..a46aca3c8 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -46,6 +46,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
       }
       
       Node bd = TermDb::getFunDefBody( assertions[i] );
+      Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl;
       Assert( !bd.isNull() );
       bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd );
 
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index a3d239d18..d9ed3f092 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -42,8 +42,6 @@ public:
   virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
   //whether to construct model
   virtual bool optUseModel();
-  //whether to construct model at fullModel = true
-  virtual bool optBuildAtFullModel() { return false; }
   /** number of lemmas generated while building model */
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;