Minor cleanup.

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index ce03a18778edb4ab3b00bbd0803044d935d51e79..a0b195a9c6c522ffc1c67ec84248afec17a6b584 100755 (executable)
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -1,4 +1,3 @@
-
 /*********************                                                        */
 /*! \file full_model_check.cpp
  ** \verbatim
@@ -553,7 +552,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
 
 void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
   if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){
-    Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl;\r
+    Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl;
     Node mbn;
     if (!fm->d_rep_set.hasType(tn)) {
       mbn = fm->getSomeDomainElement(tn);
@@ -684,16 +683,16 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
             }
             d_triedLemmas++;
             if( d_qe->addInstantiation( f, m ) ){
-              Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;\r
+              Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
               d_addedLemmas++;
             }else{
-              Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;\r
+              Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
               //this can happen if evaluation is unknown
               //might try it next effort level
               d_star_insts[f].push_back(i);
             }
           }else{
-            Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;\r
+            Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;
             //might try it next effort level
             d_star_insts[f].push_back(i);
           }
@@ -1149,7 +1148,7 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, De
 }
 
 int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
-  Trace("fmc-debug3") << "isCompat " << c << std::endl;\r
+  Trace("fmc-debug3") << "isCompat " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
@@ -1167,7 +1166,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c
 }
 
 bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
-  Trace("fmc-debug3") << "doMeet " << c << std::endl;\r
+  Trace("fmc-debug3") << "doMeet " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( cond[i]!=c[i-1] ) {

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 93174677fa0055d913cf7ca784cdcf49cdea1777..6bb375c3410c363633c28153af98e0cb9d448c18 100755 (executable)
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -10,6 +10,8 @@
  ** \brief Full model check class
  **/
 
+#include "cvc4_private.h"
+
 #ifndef FULL_MODEL_CHECK
 #define FULL_MODEL_CHECK