Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure to BV collectModelInfo in preparation for bug fix.

14 files changed, 368 insertions, 346 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 7960b0320..47aac4370 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -12,7 +12,7 @@
  ** \brief [[ Add one-line brief description here ]]
  **
  ** [[ Add lengthier description here ]]
- ** 
+ **
  **/
 
 #include "bitblaster.h"
@@ -29,7 +29,7 @@
 using namespace std;
 
 using namespace CVC4::theory::bv::utils;
-using namespace CVC4::context; 
+using namespace CVC4::context;
 using namespace CVC4::prop;
 
 namespace CVC4 {
@@ -37,20 +37,20 @@ namespace theory {
 namespace bv{
 
 std::string toString(Bits&  bits) {
-  ostringstream os; 
+  ostringstream os;
   for (int i = bits.size() - 1; i >= 0; --i) {
     TNode bit = bits[i];
     if (bit.getKind() == kind::CONST_BOOLEAN) {
       os << (bit.getConst<bool>() ? "1" : "0");
     } else {
-      os << bit<< " ";   
+      os << bit<< " ";
     }
   }
   os <<"\n";
-  
-  return os.str(); 
+
+  return os.str();
 }
-/////// Bitblaster 
+/////// Bitblaster
 
 Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
     d_bv(bv),
@@ -64,35 +64,35 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
     d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context());
 
     MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv);
-    d_satSolver->setNotify(notify); 
+    d_satSolver->setNotify(notify);
     // initializing the bit-blasting strategies
-    initAtomBBStrategies(); 
-    initTermBBStrategies(); 
+    initAtomBBStrategies();
+    initTermBBStrategies();
   }
 
 Bitblaster::~Bitblaster() {
   delete d_cnfStream;
-  delete d_satSolver; 
+  delete d_satSolver;
 }
 
 
-/** 
+/**
  * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
  * NOTE: duplicate clauses are not detected because of marker literal
  * @param node the atom to be bitblasted
- * 
+ *
  */
 void Bitblaster::bbAtom(TNode node) {
   node = node.getKind() == kind::NOT?  node[0] : node;
-  
+
   if (hasBBAtom(node)) {
-    return; 
+    return;
   }
 
   // make sure it is marked as an atom
-  addAtom(node); 
+  addAtom(node);
 
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
   Node normalized = Rewriter::rewrite(node);
@@ -126,14 +126,14 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numTerms;
 
   d_termBBStrategies[node.getKind()] (node, bits,this);
-  
+
   Assert (bits.size() == utils::getSize(node));
 
-  cacheTermDef(node, bits); 
+  cacheTermDef(node, bits);
 }
 
 Node Bitblaster::bbOptimize(TNode node) {
@@ -142,21 +142,21 @@ Node Bitblaster::bbOptimize(TNode node) {
    if (node.getKind() == kind::BITVECTOR_PLUS) {
     if (RewriteRule<BBPlusNeg>::applies(node)) {
       Node res = RewriteRule<BBPlusNeg>::run<false>(node);
-      return res; 
+      return res;
     }
     //  if (RewriteRule<BBFactorOut>::applies(node)) {
     //   Node res = RewriteRule<BBFactorOut>::run<false>(node);
-    //   return res; 
-    // } 
+    //   return res;
+    // }
 
   } else if (node.getKind() == kind::BITVECTOR_MULT) {
     if (RewriteRule<MultPow2>::applies(node)) {
       Node res = RewriteRule<MultPow2>::run<false>(node);
-      return res; 
+      return res;
     }
   }
-  
-  return node; 
+
+  return node;
 }
 
 /// Public methods
@@ -173,31 +173,31 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
   std::vector<SatLiteral> literal_explanation;
   d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation);
   for (unsigned i = 0; i < literal_explanation.size(); ++i) {
-    explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); 
+    explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
   }
 }
 
 
-/** 
+/**
  * Asserts the clauses corresponding to the atom to the Sat Solver
  * by turning on the marker literal (i.e. setting it to false)
  * @param node the atom to be asserted
- * 
+ *
  */
- 
+
 bool Bitblaster::propagate() {
   return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
 }
 
 bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   // strip the not
-  TNode atom; 
+  TNode atom;
   if (lit.getKind() == kind::NOT) {
-    atom = lit[0]; 
+    atom = lit[0];
   } else {
-    atom = lit; 
+    atom = lit;
   }
-  
+
   Assert (hasBBAtom(atom));
 
   SatLiteral markerLit = d_cnfStream->getLiteral(atom);
@@ -205,9 +205,9 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   if(lit.getKind() == kind::NOT) {
     markerLit = ~markerLit;
   }
-  
+
   Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
-  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";
 
   SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 
@@ -217,13 +217,13 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   return ret == prop::SAT_VALUE_TRUE;
 }
 
-/** 
- * Calls the solve method for the Sat Solver. 
+/**
+ * Calls the solve method for the Sat Solver.
  * passing it the marker literals to be asserted
- * 
+ *
  * @return true for sat, and false for unsat
  */
- 
+
 bool Bitblaster::solve(bool quick_solve) {
   if (Trace.isOn("bitvector")) {
     Trace("bitvector") << "Bitblaster::solve() asserted atoms ";
@@ -232,24 +232,24 @@ bool Bitblaster::solve(bool quick_solve) {
       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
     }
   }
-  Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
-  return SAT_VALUE_TRUE == d_satSolver->solve(); 
+  Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
+  return SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
 void Bitblaster::getConflict(std::vector<TNode>& conflict) {
   SatClause conflictClause;
   d_satSolver->getUnsatCore(conflictClause);
-  
+
   for (unsigned i = 0; i < conflictClause.size(); i++) {
-    SatLiteral lit = conflictClause[i]; 
+    SatLiteral lit = conflictClause[i];
     TNode atom = d_cnfStream->getNode(lit);
-    Node  not_atom; 
+    Node  not_atom;
     if (atom.getKind() == kind::NOT) {
       not_atom = atom[0];
     } else {
-      not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); 
+      not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom);
     }
-    conflict.push_back(not_atom); 
+    conflict.push_back(not_atom);
   }
 }
 
@@ -259,9 +259,9 @@ void Bitblaster::getConflict(std::vector<TNode>& conflict) {
 
 void Bitblaster::initAtomBBStrategies() {
   for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
-    d_atomBBStrategies[i] = UndefinedAtomBBStrategy; 
+    d_atomBBStrategies[i] = UndefinedAtomBBStrategy;
   }
-  
+
   /// setting default bb strategies for atoms
   d_atomBBStrategies [ kind::EQUAL ]           = DefaultEqBB;
   d_atomBBStrategies [ kind::BITVECTOR_ULT ]   = DefaultUltBB;
@@ -272,7 +272,7 @@ void Bitblaster::initAtomBBStrategies() {
   d_atomBBStrategies [ kind::BITVECTOR_SLE ]   = DefaultSleBB;
   d_atomBBStrategies [ kind::BITVECTOR_SGT ]   = DefaultSgtBB;
   d_atomBBStrategies [ kind::BITVECTOR_SGE ]   = DefaultSgeBB;
-  
+
 }
 
 void Bitblaster::initTermBBStrategies() {
@@ -281,7 +281,7 @@ void Bitblaster::initTermBBStrategies() {
   for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
     d_termBBStrategies[i] = DefaultVarBB;
   }
-  
+
   /// setting default bb strategies for terms:
   //  d_termBBStrategies [ kind::VARIABLE ]               = DefaultVarBB;
   d_termBBStrategies [ kind::CONST_BITVECTOR ]        = DefaultConstBB;
@@ -298,13 +298,13 @@ void Bitblaster::initTermBBStrategies() {
   d_termBBStrategies [ kind::BITVECTOR_PLUS ]         = DefaultPlusBB;
   d_termBBStrategies [ kind::BITVECTOR_SUB ]          = DefaultSubBB;
   d_termBBStrategies [ kind::BITVECTOR_NEG ]          = DefaultNegBB;
-  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = UndefinedTermBBStrategy;
   d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ]   = DefaultUdivBB;
   d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ]   = DefaultUremBB;
-  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = UndefinedTermBBStrategy;
   d_termBBStrategies [ kind::BITVECTOR_SHL ]          = DefaultShlBB;
   d_termBBStrategies [ kind::BITVECTOR_LSHR ]         = DefaultLshrBB;
   d_termBBStrategies [ kind::BITVECTOR_ASHR ]         = DefaultAshrBB;
@@ -316,22 +316,22 @@ void Bitblaster::initTermBBStrategies() {
   d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ]  = DefaultRotateLeftBB;
 
 }
- 
+
 bool Bitblaster::hasBBAtom(TNode atom) const {
   return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end();
 }
 
 void Bitblaster::cacheTermDef(TNode term, Bits def) {
   Assert (d_termCache.find(term) == d_termCache.end());
-  d_termCache[term] = def; 
+  d_termCache[term] = def;
 }
 
 bool Bitblaster::hasBBTerm(TNode node) const {
-  return d_termCache.find(node) != d_termCache.end(); 
+  return d_termCache.find(node) != d_termCache.end();
 }
 
 void Bitblaster::getBBTerm(TNode node, Bits& bits) const {
-  Assert (hasBBTerm(node)); 
+  Assert (hasBBTerm(node));
   // copy?
   bits = d_termCache.find(node)->second;
 }
@@ -340,7 +340,7 @@ Bitblaster::Statistics::Statistics() :
   d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0),
   d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0),
   d_numTerms("theory::bv::NumberOfBitblastedTerms", 0),
-  d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), 
+  d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0),
   d_bitblastTimer("theory::bv::BitblastTimer")
 {
   StatisticsRegistry::registerStat(&d_numTermClauses);
@@ -377,7 +377,7 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
 };
 
 void Bitblaster::MinisatNotify::safePoint() {
-  d_bv->d_out->safePoint(); 
+  d_bv->d_out->safePoint();
 }
 
 EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
@@ -420,70 +420,75 @@ EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
 
 
 bool Bitblaster::isSharedTerm(TNode node) {
-  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); 
+  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
 
 bool Bitblaster::hasValue(TNode a) {
-  Assert (d_termCache.find(a) != d_termCache.end()); 
+  Assert (d_termCache.find(a) != d_termCache.end());
   Bits bits = d_termCache[a];
   for (int i = bits.size() -1; i >= 0; --i) {
-    SatValue bit_value; 
-    if (d_cnfStream->hasLiteral(bits[i])) { 
+    SatValue bit_value;
+    if (d_cnfStream->hasLiteral(bits[i])) {
       SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
       if (bit_value == SAT_VALUE_UNKNOWN)
-        return false; 
+        return false;
     } else {
-      return false; 
+      return false;
     }
   }
-  return true; 
+  return true;
 }
-/** 
+/**
  * Returns the value a is currently assigned to in the SAT solver
- * or null if the value is completely unassigned. 
- * 
- * @param a 
- * 
- * @return 
+ * or null if the value is completely unassigned.
+ *
+ * @param a
+ *
+ * @return
  */
-Node Bitblaster::getVarValue(TNode a) {
+Node Bitblaster::getVarValue(TNode a, bool fullModel) {
   if (d_termCache.find(a) == d_termCache.end()) {
     Assert(isSharedTerm(a));
-    return Node(); 
+    return Node();
   }
   Bits bits = d_termCache[a];
-  Integer value(0); 
+  Integer value(0);
   for (int i = bits.size() -1; i >= 0; --i) {
     SatValue bit_value;
-    if (d_cnfStream->hasLiteral(bits[i])) { 
+    if (d_cnfStream->hasLiteral(bits[i])) {
       SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
-      Assert (bit_value != SAT_VALUE_UNKNOWN); 
+      Assert (bit_value != SAT_VALUE_UNKNOWN);
     } else {
-      // the bit is unconstrainted so we can give it an arbitrary value 
+      //TODO: return Node() if fullModel=false?
+      // the bit is unconstrainted so we can give it an arbitrary value
       bit_value = SAT_VALUE_FALSE;
     }
-    Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); 
-    value = value * 2 + bit_int;  
+    Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+    value = value * 2 + bit_int;
   }
-  return utils::mkConst(BitVector(bits.size(), value));  
+  return utils::mkConst(BitVector(bits.size(), value));
 }
 
-void Bitblaster::collectModelInfo(TheoryModel* m) {
+void Bitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
     if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
-      Node const_value = getVarValue(var);
+      Node const_value = getVarValue(var, fullModel);
       if(const_value == Node()) {
-        // if the value is unassigned just set it to zero
-        const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); 
+        if( fullModel ){
+          // if the value is unassigned just set it to zero
+          const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
+        }
+      }
+      if(const_value != Node()) {
+        Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
+                                  << var << " "
+                                  << const_value << "))\n";
+        m->assertEquality(var, const_value, true);
       }
-      Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
-                                << var << " "
-                                << const_value << "))\n";
-      m->assertEquality(var, const_value, true); 
     }
   }
 }
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index c122c407d..83efc05b0 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -55,14 +55,14 @@ namespace bv {
 
 typedef std::vector<Node> Bits;
 
-std::string toString (Bits& bits); 
+std::string toString (Bits& bits);
 
 class TheoryBV;
 
-/** 
- * The Bitblaster that manages the mapping between Nodes 
- * and their bitwise definition 
- * 
+/**
+ * The Bitblaster that manages the mapping between Nodes
+ * and their bitwise definition
+ *
  */
 class Bitblaster {
 
@@ -79,26 +79,26 @@ class Bitblaster {
     void notify(prop::SatClause& clause);
     void safePoint();
   };
-  
-  
+
+
   typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction >              TermDefMap;
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      AtomSet;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      VarSet; 
-  
-  typedef void   (*TermBBStrategy) (TNode, Bits&, Bitblaster*); 
-  typedef Node   (*AtomBBStrategy) (TNode, Bitblaster*); 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      VarSet;
+
+  typedef void   (*TermBBStrategy) (TNode, Bits&, Bitblaster*);
+  typedef Node   (*AtomBBStrategy) (TNode, Bitblaster*);
 
   TheoryBV *d_bv;
-  
+
   // sat solver used for bitblasting and associated CnfStream
   theory::OutputChannel*             d_bvOutput;
-  prop::BVSatSolverInterface*        d_satSolver; 
+  prop::BVSatSolverInterface*        d_satSolver;
   prop::CnfStream*                   d_cnfStream;
 
   // caches and mappings
   TermDefMap                   d_termCache;
   AtomSet                      d_bitblastedAtoms;
-  VarSet                       d_variables; 
+  VarSet                       d_variables;
   context::CDList<prop::SatLiteral>  d_assertedAtoms; /**< context dependent list storing the atoms
                                                        currently asserted by the DPLL SAT solver. */
 
@@ -111,79 +111,79 @@ class Bitblaster {
 
   /// function tables for the various bitblasting strategies indexed by node kind
   TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
-  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; 
+  AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
 
   // helper methods to initialize function tables
   void initAtomBBStrategies();
-  void initTermBBStrategies(); 
+  void initTermBBStrategies();
 
   // returns a node that might be easier to bitblast
-  Node bbOptimize(TNode node); 
-  
-  void addAtom(TNode atom); 
+  Node bbOptimize(TNode node);
+
+  void addAtom(TNode atom);
   // division is bitblasted in terms of constraints
   // so it needs to use private bitblaster interface
   void bbUdiv(TNode node, Bits& bits);
   void bbUrem(TNode node, Bits& bits);
-  bool hasValue(TNode a); 
+  bool hasValue(TNode a);
 public:
   void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
   void bbTerm(TNode node, Bits&  bits);
   void bbAtom(TNode node);
-  
-  Bitblaster(context::Context* c, bv::TheoryBV* bv); 
+
+  Bitblaster(context::Context* c, bv::TheoryBV* bv);
   ~Bitblaster();
   bool assertToSat(TNode node, bool propagate = true);
   bool propagate();
   bool solve(bool quick_solve = false);
-  void getConflict(std::vector<TNode>& conflict); 
+  void getConflict(std::vector<TNode>& conflict);
   void explain(TNode atom, std::vector<TNode>& explanation);
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  /** 
+  /**
    * Return a constant Node representing the value of a variable
-   * in the current model. 
-   * @param a 
-   * 
-   * @return 
+   * in the current model.
+   * @param a
+   *
+   * @return
    */
-  Node getVarValue(TNode a);
-  /** 
-   * Adds a constant value for each bit-blasted variable in the model. 
-   * 
-   * @param m the model 
+  Node getVarValue(TNode a, bool fullModel=true);
+  /**
+   * Adds a constant value for each bit-blasted variable in the model.
+   *
+   * @param m the model
    */
-  void collectModelInfo(TheoryModel* m); 
-  /** 
-   * Stores the variable (or non-bv term) and its corresponding bits. 
-   * 
-   * @param var 
-   * @param bits 
+  void collectModelInfo(TheoryModel* m, bool fullModel);
+  /**
+   * Stores the variable (or non-bv term) and its corresponding bits.
+   *
+   * @param var
+   * @param bits
    */
   void storeVariable(TNode var) {
-    d_variables.insert(var); 
+    d_variables.insert(var);
   }
 
   bool isSharedTerm(TNode node);
   uint64_t computeAtomWeight(TNode node);
 
 private:
- 
+
   class Statistics {
   public:
     IntStat d_numTermClauses, d_numAtomClauses;
-    IntStat d_numTerms, d_numAtoms; 
+    IntStat d_numTerms, d_numAtoms;
     TimerStat d_bitblastTimer;
     Statistics();
-    ~Statistics(); 
-  }; 
-  
+    ~Statistics();
+  };
+
   Statistics d_statistics;
 };
 
 
 
-} /* bv namespace */ 
+} /* bv namespace */
 
 } /* theory namespace */
 
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 1c6920236..0b0551283 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Algebraic solver. 
+ ** \brief Algebraic solver.
  **
  ** Algebraic solver.
  **/
@@ -46,7 +46,7 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
     out << "BV_CORE_SUBTHEORY";
     break;
   case SUB_INEQUALITY:
-    out << "BV_INEQUALITY_SUBTHEORY"; 
+    out << "BV_INEQUALITY_SUBTHEORY";
   default:
     Unreachable();
     break;
@@ -55,10 +55,10 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
 }
 
 
-// forward declaration 
-class TheoryBV; 
+// forward declaration
+class TheoryBV;
 
-typedef context::CDQueue<Node> AssertionQueue; 
+typedef context::CDQueue<Node> AssertionQueue;
 /**
  * Abstract base class for bit-vector subtheory solvers
  *
@@ -75,7 +75,7 @@ protected:
   AssertionQueue d_assertionQueue;
   context::CDO<uint32_t>  d_assertionIndex;
 public:
-  
+
   SubtheorySolver(context::Context* c, TheoryBV* bv) :
     d_context(c),
     d_bv(bv),
@@ -83,24 +83,24 @@ public:
     d_assertionIndex(c, 0)
   {}
   virtual ~SubtheorySolver() {}
-  virtual bool check(Theory::Effort e) = 0; 
+  virtual bool check(Theory::Effort e) = 0;
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
   virtual void preRegister(TNode node) {}
   virtual void propagate(Theory::Effort e) {}
-  virtual void collectModelInfo(TheoryModel* m) = 0;
-  virtual Node getModelValue(TNode var) = 0; 
+  virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0;
+  virtual Node getModelValue(TNode var) = 0;
   virtual bool isComplete() = 0;
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
-  virtual void addSharedTerm(TNode node) {} 
+  virtual void addSharedTerm(TNode node) {}
   bool done() { return d_assertionQueue.size() == d_assertionIndex; }
   TNode get() {
-    Assert (!done()); 
+    Assert (!done());
     TNode res = d_assertionQueue[d_assertionIndex];
     d_assertionIndex = d_assertionIndex + 1;
-    return res; 
+    return res;
   }
   virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
-}; 
+};
 
 }
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 244d87233..5a0c17134 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -84,20 +84,20 @@ void BitblastSolver::bitblastQueue() {
 }
 
 bool BitblastSolver::check(Theory::Effort e) {
-  Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; 
+  Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
   Assert(!options::bitvectorEagerBitblast());
 
-  ++(d_statistics.d_numCallstoCheck); 
+  ++(d_statistics.d_numCallstoCheck);
 
   //// Lazy bit-blasting
   // bit-blast enqueued nodes
   bitblastQueue();
 
-  // Processing assertions  
+  // Processing assertions
   while (!done()) {
     TNode fact = get();
     d_validModelCache = false;
-    Debug("bv-bitblast") << "  fact " << fact << ")\n"; 
+    Debug("bv-bitblast") << "  fact " << fact << ")\n";
     if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
       d_bitblaster->bbAtom(fact);
@@ -144,8 +144,8 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
   return d_bitblaster->getEqualityStatus(a, b);
 }
 
-void BitblastSolver::collectModelInfo(TheoryModel* m) {
-  return d_bitblaster->collectModelInfo(m); 
+void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+  return d_bitblaster->collectModelInfo(m, fullModel);
 }
 
 Node BitblastSolver::getModelValue(TNode node)
@@ -189,5 +189,5 @@ Node BitblastSolver::getModelValueRec(TNode node)
   Assert(val.isConst());
   d_modelCache[node] = val;
   Debug("bitvector-model") << node << " => " << val <<"\n";
-  return val; 
+  return val;
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 315254c8e..71e80238d 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -33,21 +33,21 @@ class BitblastSolver : public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     Statistics();
-    ~Statistics(); 
-  }; 
+    ~Statistics();
+  };
   /** Bitblaster */
   Bitblaster* d_bitblaster;
 
   /** Nodes that still need to be bit-blasted */
   context::CDQueue<TNode> d_bitblastQueue;
-  Statistics d_statistics; 
+  Statistics d_statistics;
 
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
   NodeMap d_modelCache;
   context::CDO<bool> d_validModelCache;
   Node getModelValueRec(TNode node);
 
-  bool  d_useSatPropagation; 
+  bool  d_useSatPropagation;
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
@@ -56,7 +56,7 @@ public:
   bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void collectModelInfo(TheoryModel* m); 
+  void collectModelInfo(TheoryModel* m, bool fullModel);
   Node getModelValue(TNode node);
   bool isComplete() { return true; }
   void bitblastQueue();
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index f7209d326..45946b8c8 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -72,7 +72,7 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
 }
 
 CoreSolver::~CoreSolver() {
-  delete d_slicer; 
+  delete d_slicer;
 }
 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
@@ -104,51 +104,51 @@ Node CoreSolver::getBaseDecomposition(TNode a) {
   std::vector<Node> a_decomp;
   d_slicer->getBaseDecomposition(a, a_decomp);
   Node new_a = utils::mkConcat(a_decomp);
-  Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n"; 
-  return new_a; 
+  Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a <<" => " << new_a << "\n";
+  return new_a;
 }
 
 bool CoreSolver::decomposeFact(TNode fact) {
-  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;  
+  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
   // assert decompositions since the equality engine does not know the semantics of
   // concat:
   //   a == a_1 concat ... concat a_k
   //   b == b_1 concat ... concat b_k
-  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;  
-  // FIXME: are this the right things to assert? 
+  Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact << endl;
+  // FIXME: are this the right things to assert?
   // assert decompositions since the equality engine does not know the semantics of
   // concat:
   //   a == a_1 concat ... concat a_k
   //   b == b_1 concat ... concat b_k
-  TNode eq = fact.getKind() == kind::NOT? fact[0] : fact; 
+  TNode eq = fact.getKind() == kind::NOT? fact[0] : fact;
 
   TNode a = eq[0];
   TNode b = eq[1];
   Node new_a = getBaseDecomposition(a);
-  Node new_b = getBaseDecomposition(b); 
-  
+  Node new_b = getBaseDecomposition(b);
+
   Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
-          utils::getSize(new_a) == utils::getSize(a)); 
-  
+          utils::getSize(new_a) == utils::getSize(a));
+
   NodeManager* nm = NodeManager::currentNM();
   Node a_eq_new_a = nm->mkNode(kind::EQUAL, a, new_a);
   Node b_eq_new_b = nm->mkNode(kind::EQUAL, b, new_b);
 
   bool ok = true;
   ok = assertFactToEqualityEngine(a_eq_new_a, utils::mkTrue());
-  if (!ok) return false; 
+  if (!ok) return false;
   ok = assertFactToEqualityEngine(b_eq_new_b, utils::mkTrue());
-  if (!ok) return false; 
+  if (!ok) return false;
   ok = assertFactToEqualityEngine(fact, fact);
   if (!ok) return false;
-  
+
   if (fact.getKind() == kind::EQUAL) {
     // assert the individual equalities as well
     //    a_i == b_i
     if (new_a.getKind() == kind::BITVECTOR_CONCAT &&
         new_b.getKind() == kind::BITVECTOR_CONCAT) {
-      
-      Assert (new_a.getNumChildren() == new_b.getNumChildren()); 
+
+      Assert (new_a.getNumChildren() == new_b.getNumChildren());
       for (unsigned i = 0; i < new_a.getNumChildren(); ++i) {
         Node eq_i = nm->mkNode(kind::EQUAL, new_a[i], new_b[i]);
         ok = assertFactToEqualityEngine(eq_i, fact);
@@ -156,23 +156,23 @@ bool CoreSolver::decomposeFact(TNode fact) {
       }
     }
   }
-  return true; 
+  return true;
 }
 
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
   Assert (!d_bv->inConflict());
-  ++(d_statistics.d_numCallstoCheck); 
-  bool ok = true; 
+  ++(d_statistics.d_numCallstoCheck);
+  bool ok = true;
   std::vector<Node> core_eqs;
   while (! done()) {
-    TNode fact = get(); 
-    
+    TNode fact = get();
+
     // update whether we are in the core fragment
     if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
-      d_isCoreTheory = false; 
+      d_isCoreTheory = false;
     }
-    
+
     // only reason about equalities
     if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
       if (options::bitvectorCoreSolver()) {
@@ -181,31 +181,31 @@ bool CoreSolver::check(Theory::Effort e) {
         ok = assertFactToEqualityEngine(fact, fact);
       }
     } else {
-      ok = assertFactToEqualityEngine(fact, fact); 
+      ok = assertFactToEqualityEngine(fact, fact);
     }
     if (!ok)
-      return false; 
+      return false;
   }
-  
+
   if (Theory::fullEffort(e) && isComplete()) {
     buildModel();
   }
-  
+
   return true;
 }
 
 void CoreSolver::buildModel() {
   if (options::bitvectorCoreSolver()) {
     // FIXME
-    Unreachable(); 
-    return; 
+    Unreachable();
+    return;
   }
-  Debug("bv-core") << "CoreSolver::buildModel() \n"; 
-  d_modelValues.clear(); 
+  Debug("bv-core") << "CoreSolver::buildModel() \n";
+  d_modelValues.clear();
   TNodeSet constants;
-  TNodeSet constants_in_eq_engine; 
+  TNodeSet constants_in_eq_engine;
   // collect constants in equality engine
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); 
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
   while (!eqcs_i.isFinished()) {
     TNode repr = *eqcs_i;
     if  (repr.getKind() == kind::CONST_BITVECTOR) {
@@ -213,39 +213,39 @@ void CoreSolver::buildModel() {
       eq::EqClassIterator it(repr, &d_equalityEngine);
       if (!(++it).isFinished() || true) {
         constants.insert(repr);
-        constants_in_eq_engine.insert(repr); 
+        constants_in_eq_engine.insert(repr);
       }
     }
-    ++eqcs_i; 
+    ++eqcs_i;
   }
   // build repr to value map
-  
+
   eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
   while (!eqcs_i.isFinished()) {
     TNode repr = *eqcs_i;
     ++eqcs_i;
-    
+
     if (repr.getKind() != kind::VARIABLE &&
         repr.getKind() != kind::SKOLEM &&
         repr.getKind() != kind::CONST_BITVECTOR &&
         !d_bv->isSharedTerm(repr)) {
-      continue; 
+      continue;
     }
-  
-    TypeNode type = repr.getType(); 
+
+    TypeNode type = repr.getType();
     if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
-      Debug("bv-core-model") << "   processing " << repr <<"\n"; 
+      Debug("bv-core-model") << "   processing " << repr <<"\n";
       // we need to assign a value for it
       TypeEnumerator te(type);
-      Node val; 
+      Node val;
       do {
-        val = *te; 
+        val = *te;
         ++te;
         // Debug("bv-core-model") << "  trying value " << val << "\n";
         // Debug("bv-core-model") << "  is in set? " << constants.count(val) << "\n";
-        // Debug("bv-core-model") << "  enumerator done? " << te.isFinished() << "\n"; 
+        // Debug("bv-core-model") << "  enumerator done? " << te.isFinished() << "\n";
       } while (constants.count(val) != 0 && !(te.isFinished()));
-      
+
       if (te.isFinished() && constants.count(val) != 0) {
         // if we cannot enumerate anymore values we just return the lemma stating that
         // at least two of the representatives are equal.
@@ -254,15 +254,15 @@ void CoreSolver::buildModel() {
 
         for (TNodeSet::const_iterator it = constants_in_eq_engine.begin();
              it != constants_in_eq_engine.end(); ++it) {
-          TNode constant = *it; 
+          TNode constant = *it;
           if (utils::getSize(constant) == utils::getSize(repr)) {
-            representatives.push_back(constant); 
+            representatives.push_back(constant);
           }
         }
         for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
           representatives.push_back(it->first);
         }
-        std::vector<Node> equalities; 
+        std::vector<Node> equalities;
         for (unsigned i = 0; i < representatives.size(); ++i) {
           for (unsigned j = i + 1; j < representatives.size(); ++j) {
             TNode a = representatives[i];
@@ -274,18 +274,18 @@ void CoreSolver::buildModel() {
         }
         Node lemma = utils::mkOr(equalities);
         d_bv->lemma(lemma);
-        Debug("bv-core") << "  lemma: " << lemma << "\n"; 
-        return; 
+        Debug("bv-core") << "  lemma: " << lemma << "\n";
+        return;
       }
       Debug("bv-core-model") << "   " << repr << " => " << val <<"\n" ;
       constants.insert(val);
-      d_modelValues[repr] = val; 
+      d_modelValues[repr] = val;
     }
   }
 }
 
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
-  // Notify the equality engine 
+  // Notify the equality engine
   if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
@@ -310,8 +310,8 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   // checking for a conflict
   if (d_bv->inConflict()) {
     return false;
-  }  
-  return true; 
+  }
+  return true;
 }
 
 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
@@ -356,10 +356,10 @@ void CoreSolver::conflict(TNode a, TNode b) {
   d_bv->setConflict(conflict);
 }
 
-void CoreSolver::collectModelInfo(TheoryModel* m) {
+void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
   if (options::bitvectorCoreSolver()) {
     Unreachable();
-    return; 
+    return;
   }
   if (Debug.isOn("bitvector-model")) {
     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
@@ -372,11 +372,11 @@ void CoreSolver::collectModelInfo(TheoryModel* m) {
   d_bv->computeRelevantTerms(termSet);
   m->assertEqualityEngine(&d_equalityEngine, &termSet);
   if (isComplete()) {
-    Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; 
+    Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
     for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
       Node a = it->first;
       Node b = it->second;
-      m->assertEquality(a, b, true); 
+      m->assertEquality(a, b, true);
     }
   }
 }
@@ -385,23 +385,23 @@ Node CoreSolver::getModelValue(TNode var) {
   // we don't need to evaluate bv expressions and only look at variable values
   // because this only gets called when the core theory is complete (i.e. no other bv
   // function symbols are currently asserted)
-  Assert (d_slicer->isCoreTerm(var)); 
-  
-  Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";  
+  Assert (d_slicer->isCoreTerm(var));
+
+  Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";
   Assert (isComplete());
   TNode repr = d_equalityEngine.getRepresentative(var);
-  Node result = Node(); 
+  Node result = Node();
   if (repr.getKind() == kind::CONST_BITVECTOR) {
-    result = repr; 
+    result = repr;
   } else if (d_modelValues.find(repr) == d_modelValues.end()) {
     // it may be a shared term that never gets asserted
     // result is just Null
     Assert(d_bv->isSharedTerm(var));
   } else {
-    result = d_modelValues[repr]; 
+    result = d_modelValues[repr];
   }
-  Debug("bitvector-model") << " => " << result <<"\n"; 
-  return result; 
+  Debug("bitvector-model") << " => " << result <<"\n";
+  return result;
 }
 
 CoreSolver::Statistics::Statistics()
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 423408a7c..b886bbdd5 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -25,21 +25,21 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-class Slicer; 
-class Base; 
+class Slicer;
+class Base;
 /**
  * Bitvector equality solver
  */
 class CoreSolver : public SubtheorySolver {
   typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
 
   struct Statistics {
     IntStat d_numCallstoCheck;
     Statistics();
-    ~Statistics(); 
-  }; 
-  
+    ~Statistics();
+  };
+
   // NotifyClass: handles call-back from congruence closure module
   class NotifyClass : public eq::EqualityEngineNotify {
     CoreSolver& d_solver;
@@ -59,13 +59,13 @@ class CoreSolver : public SubtheorySolver {
 
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
-  
+
   /** Equality engine */
   eq::EqualityEngine d_equalityEngine;
 
   /** Store a propagation to the bv solver */
   bool storePropagation(TNode literal);
-  
+
   /** Store a conflict from merging two constants */
   void conflict(TNode a, TNode b);
 
@@ -74,12 +74,12 @@ class CoreSolver : public SubtheorySolver {
   /** To make sure we keep the explanations */
   context::CDHashSet<Node, NodeHashFunction> d_reasons;
   ModelValue d_modelValues;
-  void buildModel(); 
-  bool assertFactToEqualityEngine(TNode fact, TNode reason);  
+  void buildModel();
+  bool assertFactToEqualityEngine(TNode fact, TNode reason);
   bool decomposeFact(TNode fact);
   Node getBaseDecomposition(TNode a);
-  Statistics d_statistics; 
-public: 
+  Statistics d_statistics;
+public:
   CoreSolver(context::Context* c, TheoryBV* bv);
   ~CoreSolver();
   bool  isComplete() { return d_isCoreTheory; }
@@ -87,8 +87,8 @@ public:
   void  preRegister(TNode node);
   bool  check(Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
-  void  collectModelInfo(TheoryModel* m);
-  Node  getModelValue(TNode var); 
+  void  collectModelInfo(TheoryModel* m, bool fullModel);
+  Node  getModelValue(TNode var);
   void  addSharedTerm(TNode t) {
     d_equalityEngine.addTriggerTerm(t, THEORY_BV);
   }
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 6c95bd308..a3970c9e3 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -29,17 +29,17 @@ using namespace CVC4::theory::bv::utils;
 bool InequalitySolver::check(Theory::Effort e) {
   Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
   ++(d_statistics.d_numCallstoCheck);
-  
-  bool ok = true; 
+
+  bool ok = true;
   while (!done() && ok) {
     TNode fact = get();
-    Debug("bv-subtheory-inequality") << "  "<< fact <<"\n"; 
+    Debug("bv-subtheory-inequality") << "  "<< fact <<"\n";
     if (fact.getKind() == kind::EQUAL) {
       TNode a = fact[0];
       TNode b = fact[1];
       ok = d_inequalityGraph.addInequality(a, b, false, fact);
       if (ok)
-        ok = d_inequalityGraph.addInequality(b, a, false, fact); 
+        ok = d_inequalityGraph.addInequality(b, a, false, fact);
     } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
       TNode a = fact[0][0];
       TNode b = fact[0][1];
@@ -47,40 +47,40 @@ bool InequalitySolver::check(Theory::Effort e) {
     }
     if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0][1];
-      TNode b = fact[0][0]; 
+      TNode b = fact[0][0];
       ok = d_inequalityGraph.addInequality(a, b, true, fact);
       // propagate
       // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
-      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); 
+      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
       //   d_bv->storePropagation(neq, SUB_INEQUALITY);
       //   d_explanations[neq] = fact;
       // }
     } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
       TNode a = fact[0][1];
-      TNode b = fact[0][0]; 
+      TNode b = fact[0][0];
       ok = d_inequalityGraph.addInequality(a, b, false, fact);
     } else if (fact.getKind() == kind::BITVECTOR_ULT) {
       TNode a = fact[0];
-      TNode b = fact[1]; 
+      TNode b = fact[1];
       ok = d_inequalityGraph.addInequality(a, b, true, fact);
       // propagate
       // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
-      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); 
+      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b));
       //   d_bv->storePropagation(neq, SUB_INEQUALITY);
       //   d_explanations[neq] = fact;
       // }
     } else if (fact.getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0];
-      TNode b = fact[1]; 
+      TNode b = fact[1];
       ok = d_inequalityGraph.addInequality(a, b, false, fact);
     }
   }
-  
+
   if (!ok) {
     std::vector<TNode> conflict;
-    d_inequalityGraph.getConflict(conflict); 
+    d_inequalityGraph.getConflict(conflict);
     d_bv->setConflict(utils::flattenAnd(conflict));
-    return false; 
+    return false;
   }
 
   if (isComplete() && Theory::fullEffort(e)) {
@@ -89,39 +89,39 @@ bool InequalitySolver::check(Theory::Effort e) {
     std::vector<Node> lemmas;
     d_inequalityGraph.checkDisequalities(lemmas);
     for(unsigned i = 0; i < lemmas.size(); ++i) {
-      d_bv->lemma(lemmas[i]); 
+      d_bv->lemma(lemmas[i]);
     }
   }
-  return true; 
+  return true;
 }
 
 EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) {
   if (!isComplete())
     return EQUALITY_UNKNOWN;
-  
+
   Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
   Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
 
   // if an inequality containing the terms has been asserted then we know
   // the equality is false
   if (d_assertionSet.contains(a_lt_b) || d_assertionSet.contains(b_lt_a)) {
-    return EQUALITY_FALSE; 
+    return EQUALITY_FALSE;
   }
-  
+
   if (!d_inequalityGraph.hasValueInModel(a) ||
       !d_inequalityGraph.hasValueInModel(b)) {
-    return EQUALITY_UNKNOWN; 
+    return EQUALITY_UNKNOWN;
   }
 
   // TODO: check if this disequality is entailed by inequalities via transitivity
-  
+
   BitVector a_val = d_inequalityGraph.getValueInModel(a);
   BitVector b_val = d_inequalityGraph.getValueInModel(b);
-  
+
   if (a_val == b_val) {
-    return EQUALITY_TRUE_IN_MODEL; 
+    return EQUALITY_TRUE_IN_MODEL;
   } else {
-    return EQUALITY_FALSE_IN_MODEL; 
+    return EQUALITY_FALSE_IN_MODEL;
   }
 }
 
@@ -129,19 +129,19 @@ void InequalitySolver::assertFact(TNode fact) {
   d_assertionQueue.push_back(fact);
   d_assertionSet.insert(fact);
   if (!isInequalityOnly(fact)) {
-    d_isComplete = false; 
+    d_isComplete = false;
   }
 }
 
 bool InequalitySolver::isInequalityOnly(TNode node) {
   if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) {
-    return d_ineqTermCache[node]; 
+    return d_ineqTermCache[node];
   }
-  
+
   if (node.getKind() == kind::NOT) {
-    node = node[0]; 
+    node = node[0];
   }
-  
+
   if (node.getKind() != kind::EQUAL &&
       node.getKind() != kind::BITVECTOR_ULT &&
       node.getKind() != kind::BITVECTOR_ULE &&
@@ -149,50 +149,50 @@ bool InequalitySolver::isInequalityOnly(TNode node) {
       node.getKind() != kind::SELECT &&
       node.getKind() != kind::STORE &&
       node.getMetaKind() != kind::metakind::VARIABLE) {
-    return false; 
+    return false;
   }
-  bool res = true; 
+  bool res = true;
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
     res = res && isInequalityOnly(node[i]);
   }
-  d_ineqTermCache[node] = res; 
-  return res; 
+  d_ineqTermCache[node] = res;
+  return res;
 }
 
 void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   Assert (d_explanations.find(literal) != d_explanations.end());
   TNode explanation = d_explanations[literal];
   assumptions.push_back(explanation);
-  Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n"; 
+  Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n";
 }
 
 void InequalitySolver::propagate(Theory::Effort e) {
-  Assert (false); 
+  Assert (false);
 }
 
-void InequalitySolver::collectModelInfo(TheoryModel* m) {
-  Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; 
+void InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+  Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
   std::vector<Node> model;
   d_inequalityGraph.getAllValuesInModel(model);
   for (unsigned i = 0; i < model.size(); ++i) {
-    Assert (model[i].getKind() == kind::EQUAL); 
-    m->assertEquality(model[i][0], model[i][1], true); 
+    Assert (model[i].getKind() == kind::EQUAL);
+    m->assertEquality(model[i][0], model[i][1], true);
   }
 }
 
 Node InequalitySolver::getModelValue(TNode var) {
-  Assert (isInequalityOnly(var)); 
-  Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";  
+  Assert (isInequalityOnly(var));
+  Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";
   Assert (isComplete());
-  Node result = Node(); 
+  Node result = Node();
   if (!d_inequalityGraph.hasValueInModel(var)) {
     Assert (d_bv->isSharedTerm(var));
   } else {
     BitVector val = d_inequalityGraph.getValueInModel(var);
     result = utils::mkConst(val);
   }
-  Debug("bitvector-model") << " => " << result <<"\n";  
-  return result; 
+  Debug("bitvector-model") << " => " << result <<"\n";
+  return result;
 }
 
 InequalitySolver::Statistics::Statistics()
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 390a329ff..6e0139e09 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Algebraic solver. 
+ ** \brief Algebraic solver.
  **
  ** Algebraic solver.
  **/
@@ -31,16 +31,16 @@ class InequalitySolver: public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     Statistics();
-    ~Statistics(); 
-  }; 
+    ~Statistics();
+  };
 
-  context::CDHashSet<Node, NodeHashFunction> d_assertionSet; 
+  context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
   InequalityGraph d_inequalityGraph;
-  context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; 
+  context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
   context::CDO<bool> d_isComplete;
-  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache; 
-  bool isInequalityOnly(TNode node); 
-  Statistics d_statistics; 
+  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache;
+  bool isInequalityOnly(TNode node);
+  Statistics d_statistics;
 public:
   InequalitySolver(context::Context* c, TheoryBV* bv)
     : SubtheorySolver(c, bv),
@@ -51,19 +51,19 @@ public:
       d_ineqTermCache(),
       d_statistics()
   {}
-  
+
   bool check(Theory::Effort e);
-  void propagate(Theory::Effort e); 
+  void propagate(Theory::Effort e);
   void explain(TNode literal, std::vector<TNode>& assumptions);
   bool isComplete() { return d_isComplete; }
-  void collectModelInfo(TheoryModel* m); 
-  Node getModelValue(TNode var); 
+  void collectModelInfo(TheoryModel* m, bool fullModel);
+  Node getModelValue(TNode var);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-  void assertFact(TNode fact); 
-}; 
+  void assertFact(TNode fact);
+};
 
 }
 }
 }
 
-#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ 
+#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 38d3a2f5e..d7a7f358a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -50,24 +50,24 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_propagatedBy(c)
   {
     if (options::bvEquality()) {
-      SubtheorySolver* core_solver = new CoreSolver(c, this); 
+      SubtheorySolver* core_solver = new CoreSolver(c, this);
       d_subtheories.push_back(core_solver);
       d_subtheoryMap[SUB_CORE] = core_solver;
     }
     if (options::bitvectorInequalitySolver()) {
-      SubtheorySolver* ineq_solver = new InequalitySolver(c, this); 
+      SubtheorySolver* ineq_solver = new InequalitySolver(c, this);
       d_subtheories.push_back(ineq_solver);
       d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
     }
-    
-    SubtheorySolver* bb_solver = new BitblastSolver(c, this); 
+
+    SubtheorySolver* bb_solver = new BitblastSolver(c, this);
     d_subtheories.push_back(bb_solver);
     d_subtheoryMap[SUB_BITBLAST] = bb_solver;
   }
 
 TheoryBV::~TheoryBV() {
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    delete d_subtheories[i]; 
+    delete d_subtheories[i];
   }
 }
 
@@ -113,7 +113,7 @@ void TheoryBV::preRegisterTerm(TNode node) {
     return;
   }
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    d_subtheories[i]->preRegister(node); 
+    d_subtheories[i]->preRegister(node);
   }
 }
 
@@ -134,22 +134,22 @@ void TheoryBV::checkForLemma(TNode fact) {
     if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) {
       TNode urem = fact[0];
       TNode result = fact[1];
-      TNode divisor = urem[1]; 
+      TNode divisor = urem[1];
       Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
       Node divisor_eq_0 = mkNode(kind::EQUAL,
                                  divisor,
-                                 mkConst(BitVector(getSize(divisor), 0u)));  
+                                 mkConst(BitVector(getSize(divisor), 0u)));
       Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
       lemma(split);
     }
     if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) {
       TNode urem = fact[1];
       TNode result = fact[0];
-      TNode divisor = urem[1]; 
+      TNode divisor = urem[1];
       Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor);
       Node divisor_eq_0 = mkNode(kind::EQUAL,
                                   divisor,
-                                  mkConst(BitVector(getSize(divisor), 0u)));  
+                                  mkConst(BitVector(getSize(divisor), 0u)));
       Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div);
       lemma(split);
     }
@@ -165,9 +165,9 @@ void TheoryBV::check(Effort e)
   }
 
   if (Theory::fullEffort(e)) {
-    ++(d_statistics.d_numCallsToCheckFullEffort); 
+    ++(d_statistics.d_numCallsToCheckFullEffort);
   } else {
-    ++(d_statistics.d_numCallsToCheckStandardEffort); 
+    ++(d_statistics.d_numCallsToCheckStandardEffort);
   }
   // if we are already in conflict just return the conflict
   if (inConflict()) {
@@ -177,28 +177,28 @@ void TheoryBV::check(Effort e)
 
   while (!done()) {
     TNode fact = get().assertion;
-   	checkForLemma(fact); 
+   	checkForLemma(fact);
     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-      d_subtheories[i]->assertFact(fact); 
+      d_subtheories[i]->assertFact(fact);
     }
   }
 
   bool ok = true;
   bool complete = false;
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
-    Assert (!inConflict()); 
+    Assert (!inConflict());
     ok = d_subtheories[i]->check(e);
-    complete = d_subtheories[i]->isComplete(); 
+    complete = d_subtheories[i]->isComplete();
 
     if (!ok) {
       // if we are in a conflict no need to check with other theories
       Assert (inConflict());
       sendConflict();
-      return; 
+      return;
     }
     if (complete) {
       // if the last subtheory was complete we stop
-      return; 
+      return;
     }
   }
 }
@@ -208,8 +208,8 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   //  Assert (fullModel); // can only query full model
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
-      d_subtheories[i]->collectModelInfo(m);
-      return; 
+      d_subtheories[i]->collectModelInfo(m, fullModel);
+      return;
     }
   }
 }
@@ -218,10 +218,10 @@ Node TheoryBV::getModelValue(TNode var) {
   Assert(!inConflict());
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
-      return d_subtheories[i]->getModelValue(var); 
+      return d_subtheories[i]->getModelValue(var);
     }
   }
-  Unreachable(); 
+  Unreachable();
 }
 
 void TheoryBV::propagate(Effort e) {
@@ -239,7 +239,7 @@ void TheoryBV::propagate(Effort e) {
   bool ok = true;
   for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-    // temporary fix for incremental bit-blasting 
+    // temporary fix for incremental bit-blasting
     if (d_valuation.isSatLiteral(literal)) {
       Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n";
       ok = d_out->propagate(literal);
@@ -289,14 +289,14 @@ Node TheoryBV::ppRewrite(TNode t)
   if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) {
     std::vector<Node> equalities;
     Slicer::splitEqualities(t, equalities);
-    return utils::mkAnd(equalities); 
+    return utils::mkAnd(equalities);
   }
-  
+
   return t;
 }
 
 void TheoryBV::presolve() {
-  Debug("bitvector") << "TheoryBV::presolve" << endl; 
+  Debug("bitvector") << "TheoryBV::presolve" << endl;
 }
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
@@ -321,7 +321,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
       // Safe to ignore this one, subtheory should produce a conflict
       return true;
     }
- 
+
     d_propagatedBy[literal] = subtheory;
   }
 
@@ -382,11 +382,11 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
   if (options::bitvectorEagerBitblast()) {
     return EQUALITY_UNKNOWN;
   }
-  
+
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
-      return status; 
+      return status;
     }
   }
   return EQUALITY_UNKNOWN; ;
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 42d5bbd3a..4c168acfc 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -193,6 +193,7 @@ bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) {
 

 bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {

   if (d_et.hasGeneralization(m, c)) {

+    Trace("fmc-debug") << "Already has generalization, skip." << std::endl;

     return false;

   }

   int newIndex = (int)d_cond.size();

@@ -382,18 +383,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
       Node op = it->first;

       TypeNode tno = op.getType();

       for( unsigned i=0; i<tno.getNumChildren(); i++) {

-        TypeNode tn = tno[i];

-        if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){

-          Node mbn;

-          if (!fm->d_rep_set.hasType(tn)) {

-            mbn = fm->getSomeDomainElement(tn);

-          }else{

-            mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);

-          }

-          Node mbnr = fm->getUsedRepresentative( mbn );

-          fm->d_model_basis_rep[tn] = mbnr;

-          Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;

-        }

+        initializeType( fm, tno[i] );

       }

     }

     //now, make models

@@ -561,6 +551,21 @@ 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 << std::endl;

+    Node mbn;

+    if (!fm->d_rep_set.hasType(tn)) {

+      mbn = fm->getSomeDomainElement(tn);

+    }else{

+      mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);

+    }

+    Node mbnr = fm->getUsedRepresentative( mbn );

+    fm->d_model_basis_rep[tn] = mbnr;

+    Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;

+  }

+}

+

 void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {

   Trace(tr) << "(";

   for( unsigned j=0; j<n.getNumChildren(); j++) {

@@ -613,6 +618,10 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
         Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );

         d_quant_cond[f] = op;

       }

+      //make sure all types are set

+      for( unsigned i=0; i<f[0].getNumChildren(); i++ ){

+        initializeType( fmfmc, f[0][i].getType() );

+      }

 

       //model check the quantifier

       doCheck(fmfmc, f, d_quant_models[f], f[1]);

@@ -810,6 +819,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;

     d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );

   }else if( n.getKind() == kind::BOUND_VARIABLE ){

+    Trace("fmc-debug") << "Add default entry..." << std::endl;

     d.addEntry(fm, mkCondDefault(fm, f), n);

   }

   else if( n.getKind() == kind::NOT ){

@@ -856,6 +866,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       }

       r = fm->getUsedRepresentative( r );

     }

+    Trace("fmc-debug") << "Add constant entry..." << std::endl;

     d.addEntry(fm, mkCondDefault(fm, f), r);

   }

   else{

@@ -906,6 +917,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       }

     }

     Trace("fmc-debug") << "Simplify the definition..." << std::endl;

+    d.debugPrint("fmc-debug", Node::null(), this);

     d.simplify(this, fm);

     Trace("fmc-debug") << "Done simplifying" << std::endl;

   }

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 8ebef640c..fb810c355 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -90,6 +90,7 @@ protected:
   std::map< Node, Node > d_array_term_cond;

   std::map<Node, std::map< Node, int > > d_quant_var_id;

   std::map<Node, std::vector< int > > d_star_insts;

+  void initializeType( FirstOrderModelFmc * fm, TypeNode tn );

   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);

   bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);

 protected:

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 3e0f13e4b..628f8b14a 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -92,7 +92,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           NodeBuilder<> nb(kind::OR);
           nb << f << ceLit;
           Node lem = nb;
-          Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
+          Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
           d_quantEngine->getOutputChannel().lemma( lem );
           addedLemma = true;
         }
@@ -213,7 +213,9 @@ void InstantiationEngine::check( Theory::Effort e ){
         d_quant_active[n] = active;
         if( active ){
           Debug("quantifiers") << "  Active : " << n;
-          quantActive = true;
+          if( !TermDb::hasInstConstAttr(n) ){
+            quantActive = true;
+          }
         }else{
           Debug("quantifiers") << "  NOT active : " << n;
           if( d_quantEngine->getValuation().isDecision( cel ) ){
@@ -232,7 +234,9 @@ void InstantiationEngine::check( Theory::Effort e ){
       //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
       }else{
         d_quant_active[n] = true;
-        quantActive = true;
+        if( !TermDb::hasInstConstAttr(n) ){
+          quantActive = true;
+        }
         Debug("quantifiers") << "  Active : " << n << ", no ce assigned." << std::endl;
       }
       Debug("quantifiers-relevance")  << "Quantifier : " << n << std::endl;
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index c68623baa..52c9e34f3 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -163,7 +163,7 @@ void TheoryQuantifiers::assertExistential( Node n ){
       NodeBuilder<> nb(kind::OR);
       nb << n[0] << body.notNode();
       Node lem = nb;
-      Debug("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
+      Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
       d_out->lemma( lem );
       d_skolemized[n] = true;
     }