Minor fix for strings.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f2af6452b57a318fa60a0f1818fc817b96adbccc..efb737a293d10ac23e58c279118d9b7445211868 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1830,9 +1830,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & n
         }
         nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() );
         nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() );
-        //if( eqc!=normal_form_src[nf_index] ){
-        //  nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) );
-        //}
+        if( eqc!=normal_form_src[nf_index] ){
+          nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) );
+        }
         Trace("strings-solve-debug2") << "take normal form ... done" << std::endl;
         d_normal_forms_base[eqc] = normal_form_src[nf_index];
         //*/

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 3daf646abffc2dc2cc50333c75500fd1c69142b0..477d336e6eb727479cd410666b4127228ca56989 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -77,7 +77,8 @@ TESTS = \
   crash-1019.smt2 \
   norn-31.smt2 \
   strings-native-simple.cvc \
-  cmu-2db2-extf-reg.smt2
+  cmu-2db2-extf-reg.smt2 \
+  norn-nel-bug-052116.smt2
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/norn-nel-bug-052116.smt2 b/test/regress/regress0/strings/norn-nel-bug-052116.smt2
new file mode 100644 (file)
index 0000000..f0c2534
--- /dev/null
+++ b/test/regress/regress0/strings/norn-nel-bug-052116.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun var_0 () String)
+(declare-fun var_1 () String)
+(declare-fun var_2 () String)
+(declare-fun var_3 () String)
+(declare-fun var_4 () String)
+(declare-fun var_5 () String)
+(declare-fun var_6 () String)
+(declare-fun var_7 () String)
+(declare-fun var_8 () String)
+(declare-fun var_9 () String)
+(declare-fun var_10 () String)
+(declare-fun var_11 () String)
+(declare-fun var_12 () String)
+
+(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in.re var_4 (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (str.to.re "a")))) (str.to.re "b"))))
+(assert (str.in.re (str.++ "a" var_4 "b" ) (re.* (re.range "a" "u"))))
+(assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
+(check-sat)