From 98b41576dcaaa3a6f935613fb7cc9065f4b3b813 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 7 Jun 2018 11:37:04 -0700 Subject: [PATCH] Remove invalid assertion (#1993). (#2057) --- src/theory/bv/bv_subtheory_core.cpp | 5 ----- 1 file changed, 5 deletions(-) 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); -- 2.30.2