From a15bf2140e45d76f98f0887be6461618c884589d Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 26 Mar 2013 15:36:47 -0400 Subject: fixed inequality bugs due to improper explanation --- src/theory/bv/slicer.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'src/theory/bv/slicer.cpp') 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; -- cgit v1.2.3