From: lianah <lianahady@gmail.com>
Date: Mon, 1 Apr 2013 18:04:58 +0000 (-0400)
Subject: fixed bug 502; now the core bv solver only gives the model for variables and shared... 
X-Git-Tag: cvc5-1.0.0~7356
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3cf2615b17761da8d310c7d80b55bdac0aa4c54f;p=cvc5.git

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

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index f8c26c35a..00777af5c 100644
--- 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";