From 3cf2615b17761da8d310c7d80b55bdac0aa4c54f Mon Sep 17 00:00:00 2001 From: lianah Date: Mon, 1 Apr 2013 14:04:58 -0400 Subject: [PATCH] fixed bug 502; now the core bv solver only gives the model for variables and shared terms. --- src/theory/bv/bv_subtheory_core.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index f8c26c35a..00777af5c 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -202,6 +202,7 @@ bool CoreSolver::check(Theory::Effort e) { void CoreSolver::buildModel() { if (options::bitvectorCoreSolver()) { // FIXME + Unreachable(); return; } Debug("bv-core") << "CoreSolver::buildModel() \n"; @@ -227,7 +228,15 @@ void CoreSolver::buildModel() { eqcs_i = eq::EqClassesIterator(&d_equalityEngine); while (!eqcs_i.isFinished()) { TNode repr = *eqcs_i; - ++eqcs_i; + ++eqcs_i; + + if (repr.getKind() != kind::VARIABLE && + repr.getKind() != kind::SKOLEM && + repr.getKind() != kind::CONST_BITVECTOR && + !d_bv->isSharedTerm(repr)) { + continue; + } + TypeNode type = repr.getType(); if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) { Debug("bv-core-model") << " processing " << repr <<"\n"; -- 2.30.2