From bd284aa3cbe8960937e8ed8f140b12b3f5a446d3 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 9 Aug 2016 13:11:07 -0500
Subject: [PATCH] Fixes for sep star rewrite.

---
 src/theory/sep/theory_sep_rewriter.cpp  | 22 ++++++++--------------
 test/regress/regress0/sep/Makefile.am   |  3 ++-
 test/regress/regress0/sep/dup-nemp.smt2 |  7 +++++++
 3 files changed, 17 insertions(+), 15 deletions(-)
 create mode 100644 test/regress/regress0/sep/dup-nemp.smt2

diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index d58c2c13d..3e74bd61e 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -24,6 +24,7 @@ namespace sep {
 
 void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ){
   Assert( n.getKind()==kind::SEP_STAR );
+  Node tr = NodeManager::currentNM()->mkConst( true );
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
     if( n[i].getKind()==kind::SEP_EMP ){
       s_children.push_back( n[i] );
@@ -36,26 +37,19 @@ void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children
       getAndChildren( n[i], temp_s_children, ns_children );
       Node to_add;
       if( temp_s_children.size()==0 ){
-        to_add = NodeManager::currentNM()->mkConst( true );
-      }else{
-        //remove empty star
-        std::vector< Node > temp_s_children2;
-        for( unsigned i=0; i<temp_s_children.size(); i++ ){
-          if( temp_s_children[i].getKind()!=kind::SEP_EMP ){
-            temp_s_children2.push_back( temp_s_children[i] );
-          }
-        }
-        if( temp_s_children2.size()==1 ){
-          to_add = temp_s_children2[0];
-        }else if( temp_s_children2.size()>1 ){
-          to_add = NodeManager::currentNM()->mkNode( kind::AND, temp_s_children2 );
+        if( std::find( s_children.begin(), s_children.end(), tr )==s_children.end() ){
+          to_add = tr;
         }
+      }else if( temp_s_children.size()==1 ){
+        to_add = temp_s_children[0];
+      }else{
+        to_add = NodeManager::currentNM()->mkNode( kind::AND, temp_s_children );
       }
       if( !to_add.isNull() ){
         //flatten star
         if( to_add.getKind()==kind::SEP_STAR ){
           getStarChildren( to_add, s_children, ns_children );
-        }else if( std::find( s_children.begin(), s_children.end(), to_add )==s_children.end() ){
+        }else if( to_add.getKind()!=kind::SEP_EMP || s_children.empty() ){  //remove sep emp
           s_children.push_back( to_add );
         }
       }
diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index d72e02d97..6078bfa19 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -55,7 +55,8 @@ TESTS =	\
   quant_wand.smt2 \
   fmf-nemp-2.smt2 \
   trees-1.smt2 \
-  wand-false.smt2
+  wand-false.smt2 \
+  dup-nemp.smt2
 
 
 FAILING_TESTS =
diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2
new file mode 100644
index 000000000..009561128
--- /dev/null
+++ b/test/regress/regress0/sep/dup-nemp.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(declare-const l Loc)
+(assert (sep (not (emp l)) (not (emp l))))
+(assert (pto l l))
+(check-sat)
-- 
2.30.2