diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-11 16:14:01 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-11 16:14:01 +0000 |
commit | 42794501e81c44dce5c2f7687af288af030ef63e (patch) | |
tree | 2f0c8b7f0ad93fe64ad877b46f1c449320de8513 /src/theory/arrays/theory_arrays.h | |
parent | 7fd544c108f9fc5a6b4842593597e8fa4a8d11d7 (diff) |
Fix for array bug with decision heuristic
Also fixed one bv rewrite failure (more to come)
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 54d20d478..80fe692c0 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -305,7 +305,8 @@ class TheoryArrays : public Theory { context::CDQueue<RowLemmaType> d_RowQueue; context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded; - context::CDHashMap<TNode, bool, TNodeHashFunction> d_sharedArrays; + context::CDHashSet<TNode, TNodeHashFunction> d_sharedArrays; + context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther; context::CDO<bool> d_sharedTerms; context::CDList<TNode> d_reads; std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache; |