diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2017-04-28 15:00:01 -0700 |
---|---|---|
committer | Clark Barrett <barrett@cs.stanford.edu> | 2017-04-28 15:00:01 -0700 |
commit | 5ab14e1abdff2cd4e75b3b698dc3d65fb07be3c1 (patch) | |
tree | 852a0b6c94166903bb8cb7e532fe80cd6f98e475 /src | |
parent | 3ad71136637d0a07b2f24bd83cb9284d312f385d (diff) |
Partial fix for bug 717.experiment
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f67112eec..2c7418a77 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -684,12 +684,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node) else { d_equalityEngine.addTerm(node); } - // Maybe it's a predicate - // TODO: remove this or keep it if we allow Boolean elements in arrays. - if (node.getType().isBoolean()) { - // Get triggered for both equal and dis-equal - d_equalityEngine.addTriggerPredicate(node); - } Assert(d_equalityEngine.getRepresentative(store) == store); d_infoMap.addIndex(store, node[1]); @@ -817,6 +811,12 @@ void TheoryArrays::preRegisterTermInternal(TNode node) void TheoryArrays::preRegisterTerm(TNode node) { preRegisterTermInternal(node); + // If we have a select from an array of Bools, mark it as a term that can be propagated. + // Note: do this here instead of in preRegisterTermInternal to prevent internal select + // terms from being propagated out (as this results in an assertion failure). + if (node.getKind() == kind::SELECT && node.getType().isBoolean()) { + d_equalityEngine.addTriggerPredicate(node); + } } |