normal form fix

1 files changed, 9 insertions, 2 deletions

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8b88af3c0..35868fb69 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2703,7 +2703,7 @@ void TheoryStrings::getNormalForms(Node eqc,
                                    std::map<Node, unsigned>& term_to_nf_index)
 {
   //constant for equivalence class
-  Node eqc_non_c = eqc;
+  Node eqc_non_c;
   Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
   eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
   while( !eqc_i.isFinished() ){
@@ -2820,13 +2820,20 @@ void TheoryStrings::getNormalForms(Node eqc,
           Node nn = currv.size() == 0 ? d_emptyString : currv[0];
           Assert(d_state.areEqual(nn, eqc));
         }
-      }else{
+      }
+      else if (eqc_non_c.isNull() || n < eqc_non_c)
+      {
         eqc_non_c = n;
       }
     }
     ++eqc_i;
   }
 
+  if (eqc_non_c.isNull())
+  {
+    eqc_non_c = eqc;
+  }
+
   if( normal_forms.empty() ) {
     Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
     // This case happens when there are no non-trivial normal forms for this