inequality solver now only splits on disequalities when complete

2 files changed, 13 insertions, 8 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 15720885d..811e9a200 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -403,8 +403,12 @@ void CoreSolver::collectModelInfo(TheoryModel* m) {
 
 Node CoreSolver::getModelValue(TNode var) {
   Assert (isComplete());
-  Assert (d_modelValues.find(var) != d_modelValues.end()); 
-  return d_modelValues[d_equalityEngine.getRepresentative(var)]; 
+  TNode repr = d_equalityEngine.getRepresentative(var);
+  if (repr.getKind() == kind::CONST_BITVECTOR) {
+    return repr; 
+  }
+  Assert (d_modelValues.find(repr) != d_modelValues.end()); 
+  return d_modelValues[repr]; 
 }
 
 CoreSolver::Statistics::Statistics()
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 27047f6af..d6539f3ed 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -74,12 +74,13 @@ bool InequalitySolver::check(Theory::Effort e) {
   // make sure all the disequalities we didn't split on are still satisifed
   // and split on the ones that are not
   d_inequalityGraph.checkDisequalities();
-
-  // send out any lemmas
-  std::vector<Node> lemmas;
-  d_inequalityGraph.getNewLemmas(lemmas); 
-  for(unsigned i = 0; i < lemmas.size(); ++i) {
-    d_bv->lemma(lemmas[i]); 
+  if (isComplete()) {
+    // if we are complete we want to send out any inequality lemmas 
+    std::vector<Node> lemmas;
+    d_inequalityGraph.getNewLemmas(lemmas); 
+    for(unsigned i = 0; i < lemmas.size(); ++i) {
+      d_bv->lemma(lemmas[i]); 
+    }
   }
   return true; 
 }