From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 21 May 2016 21:58:19 +0000 (-0500)
Subject: Minor fix for strings.
X-Git-Tag: cvc5-1.0.0~6049^2~39
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c254649c8dadd9f0d94f09bf46b21f93b2c67c07;p=cvc5.git

Minor fix for strings.
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f2af6452b..efb737a29 100644
--- 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 3daf646ab..477d336e6 100644
--- 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
index 000000000..f0c2534a1
--- /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)