From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 7 Jun 2018 18:37:04 +0000 (-0700)
Subject: Remove invalid assertion (#1993). (#2057)
X-Git-Tag: cvc5-1.0.0~4975
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98b41576dcaaa3a6f935613fb7cc9065f4b3b813;p=cvc5.git

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

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index bd4040dd7..7b12b3d53 100644
--- 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);