Fixes for sep star rewrite.

diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index d58c2c13d310bae1b379a80cfa63a992379da7fc..3e74bd61e46475c46b751c1cb5cbb62345b00bb7 100644 (file)
--- 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 d72e02d975874274c00aaeb24bdb0cb60ae9528b..6078bfa19b160b6c8b787cfc25fd05b5a90f64b1 100644 (file)
--- 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 (file)
index 0000000..0095611
--- /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)