summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/arrays/array_info.cpp12
1 files changed, 4 insertions, 8 deletions
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index acc73163c..55f013f8c 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -161,11 +161,9 @@ void ArrayInfo::addStore(const Node a, const TNode st){
CNodeInfoMap::iterator it = info_map.find(a);
if(it == info_map.end()) {
- temp_store = new(true) CTNodeList(ct);
- temp_store->push_back(st);
-
temp_info = new Info(ct, bck);
- temp_info->stores = temp_store;
+ temp_store = temp_info->stores;
+ temp_store->push_back(st);
info_map[a]=temp_info;
} else {
temp_store = (*it).second->stores;
@@ -186,11 +184,9 @@ void ArrayInfo::addInStore(const TNode a, const TNode b){
CNodeInfoMap::iterator it = info_map.find(a);
if(it == info_map.end()) {
- temp_inst = new(true) CTNodeList(ct);
- temp_inst->push_back(b);
-
temp_info = new Info(ct, bck);
- temp_info->in_stores = temp_inst;
+ temp_inst = temp_info->in_stores;
+ temp_inst->push_back(b);
info_map[a] = temp_info;
} else {
temp_inst = (*it).second->in_stores;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback