diff options
Diffstat (limited to 'src/theory/sep/theory_sep.cpp')
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index c9b6a9d89..573449287 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1646,9 +1646,9 @@ void TheorySep::computeLabelModel( Node lbl ) { Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl; if( v_val.getKind()!=kind::EMPTYSET ){ while( v_val.getKind()==kind::UNION ){ - Assert(v_val[1].getKind() == kind::SINGLETON); - d_label_model[lbl].d_heap_locs_model.push_back( v_val[1] ); - v_val = v_val[0]; + Assert(v_val[0].getKind() == kind::SINGLETON); + d_label_model[lbl].d_heap_locs_model.push_back(v_val[0]); + v_val = v_val[1]; } if( v_val.getKind()==kind::SINGLETON ){ d_label_model[lbl].d_heap_locs_model.push_back( v_val ); @@ -1916,15 +1916,13 @@ Node TheorySep::HeapInfo::getValue( TypeNode tn ) { Assert(d_heap_locs.size() == d_heap_locs_model.size()); if( d_heap_locs.empty() ){ return NodeManager::currentNM()->mkConst(EmptySet(tn)); - }else if( d_heap_locs.size()==1 ){ - return d_heap_locs[0]; - }else{ - Node curr = NodeManager::currentNM()->mkNode( kind::UNION, d_heap_locs[0], d_heap_locs[1] ); - for( unsigned j=2; j<d_heap_locs.size(); j++ ){ - curr = NodeManager::currentNM()->mkNode( kind::UNION, curr, d_heap_locs[j] ); - } - return curr; } + Node curr = d_heap_locs[0]; + for (unsigned j = 1; j < d_heap_locs.size(); j++) + { + curr = NodeManager::currentNM()->mkNode(kind::UNION, d_heap_locs[j], curr); + } + return curr; } }/* CVC4::theory::sep namespace */ |