diff options
author | lianah <lianahady@gmail.com> | 2013-03-26 15:36:47 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-26 15:36:47 -0400 |
commit | a15bf2140e45d76f98f0887be6461618c884589d (patch) | |
tree | 98bf9421e6b8cac0c14b5f61ee9eb2c7b23d65a1 /src/theory/bv/slicer.cpp | |
parent | e69531ce6cefe15dcc7afe9b79d2b36c778148fa (diff) |
fixed inequality bugs due to improper explanation
Diffstat (limited to 'src/theory/bv/slicer.cpp')
-rw-r--r-- | src/theory/bv/slicer.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 5382695cf..23ae5beec 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -209,9 +209,8 @@ ExtractTerm UnionFind::mkExtractTerm(TermId id, Index high, Index low) { ExtractTerm top = getExtractTerm(id); Assert (d_topLevelIds.find(top.id) != d_topLevelIds.end()); - Index top_high = top.high; Index top_low = top.low; - Assert (top_high - top_low + 1 > high); + Assert (top.high - top_low + 1 > high); high += top_low; low += top_low; id = top.id; @@ -602,8 +601,7 @@ void UnionFind::backtrack() { } void UnionFind::undoMerge(TermId id) { - TermId repr = getRepr(id); - Assert (repr != UndefinedId); + Assert (getRepr(id) != UndefinedId); setRepr(id, UndefinedId, UndefinedId); } @@ -781,7 +779,10 @@ bool Slicer::isCoreTerm(TNode node) { Kind kind = node.getKind(); if (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT && - kind != kind::EQUAL && kind != kind::NOT && + kind != kind::EQUAL && + kind != kind::STORE && + kind != kind::SELECT && + kind != kind::NOT && node.getMetaKind() != kind::metakind::VARIABLE && kind != kind::CONST_BITVECTOR) { d_coreTermCache[node] = false; |