fixed bug 502; now the core bv solver only gives the model for variables and shared...

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index f8c26c35ae87e97f5ec787a4eac4cef0b7958119..00777af5c21f5a3e18d206a480064775197dd6ad 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -202,6 +202,7 @@ bool CoreSolver::check(Theory::Effort e) {
 void CoreSolver::buildModel() {
   if (options::bitvectorCoreSolver()) {
     // FIXME
+    Unreachable(); 
     return; 
   }
   Debug("bv-core") << "CoreSolver::buildModel() \n"; 
@@ -227,7 +228,15 @@ void CoreSolver::buildModel() {
   eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
   while (!eqcs_i.isFinished()) {
     TNode repr = *eqcs_i;
-    ++eqcs_i; 
+    ++eqcs_i;
+    
+    if (repr.getKind() != kind::VARIABLE &&
+        repr.getKind() != kind::SKOLEM &&
+        repr.getKind() != kind::CONST_BITVECTOR &&
+        !d_bv->isSharedTerm(repr)) {
+      continue; 
+    }
+  
     TypeNode type = repr.getType(); 
     if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) {
       Debug("bv-core-model") << "   processing " << repr <<"\n";