From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 13 Jun 2019 18:08:15 +0000 (-0500)
Subject:  Shorten explanation for strings inference I_Norm_S (#3051)
X-Git-Tag: cvc5-1.0.0~4111
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f61ad6919fc80cbc19fde9c295beb5082a6e0d79;p=cvc5.git

 Shorten explanation for strings inference I_Norm_S (#3051)
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 67f032193..ba0c16d02 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1464,6 +1464,7 @@ void TheoryStrings::checkInit() {
                 Trace("strings-process-debug") << "  congruent term by singular : " << n << " " << c[0] << std::endl;
                 //singular case
                 if( !areEqual( c[0], n ) ){
+                  Node ns;
                   std::vector< Node > exp;
                   //explain empty components
                   bool foundNEmpty = false;
@@ -1474,15 +1475,13 @@ void TheoryStrings::checkInit() {
                       }
                     }else{
                       Assert( !foundNEmpty );
-                      if( n[i]!=c[0] ){
-                        exp.push_back( n[i].eqNode( c[0] ) );
-                      }
+                      ns = n[i];
                       foundNEmpty = true;
                     }
                   }
                   AlwaysAssert( foundNEmpty );
                   //infer the equality
-                  sendInference( exp, n.eqNode( c[0] ), "I_Norm_S" );
+                  sendInference(exp, n.eqNode(ns), "I_Norm_S");
                 }
                 d_congruent.insert( n );
                 congruent[k]++;