diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-06-07 11:37:04 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-07 11:37:04 -0700 |
commit | 98b41576dcaaa3a6f935613fb7cc9065f4b3b813 (patch) | |
tree | c10837c8a2b32f759b4fcb8a2e2b3381bc8fcb9e | |
parent | 2022ec61d569e6408a0eccbde4954ccb7cac61a7 (diff) |
Remove invalid assertion (#1993). (#2057)
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 5 |
1 files changed, 0 insertions, 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); |