Remove invalid assertion (#1993). (#2057)

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index bd4040dd77951175f146e2aab4c6609c5ffea3a7..7b12b3d53bdab1499c13c8eaa31a32794548d321 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -459,11 +459,6 @@ bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
 }
 
 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 (isComplete());
   TNode repr = d_equalityEngine.getRepresentative(var);