diff options
author | lianah <lianahady@gmail.com> | 2013-04-01 14:04:58 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-01 14:04:58 -0400 |
commit | 3cf2615b17761da8d310c7d80b55bdac0aa4c54f (patch) | |
tree | 4675d3a8dd5d4765c784f1bb10ee4c6d8b5a44ca /src/theory | |
parent | d803fada76b1c45c3da6960865fdc8d061c7b680 (diff) |
fixed bug 502; now the core bv solver only gives the model for variables and shared terms.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 11 |
1 files changed, 10 insertions, 1 deletions
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"; |