From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 18 Aug 2015 03:31:47 +0000 (-0500)
Subject: fix for bug663
X-Git-Tag: cvc5-1.0.0~6257
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b9864d639ccf474dedd66c5691c93ca17b670e9;p=cvc5.git

fix for bug663
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index af6d92ee5..059db91f2 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1464,10 +1464,10 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
           temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
           temp_exp.push_back(length_eq);
           //must add explanation for length terms
-          if( !normal_forms[i][index_i].isConst() && length_term_i[0]!=normal_forms[i][index_i] ){
+          if( !normal_forms[i][index_i].isConst() && !length_term_i.isConst() && length_term_i[0]!=normal_forms[i][index_i] ){
             temp_exp.push_back( length_term_i[0].eqNode( normal_forms[i][index_i] ) );
           }
-          if( !normal_forms[j][index_j].isConst() && length_term_j[0]!=normal_forms[j][index_j] ){
+          if( !normal_forms[j][index_j].isConst() && !length_term_j.isConst() && length_term_j[0]!=normal_forms[j][index_j] ){
             temp_exp.push_back( length_term_j[0].eqNode( normal_forms[j][index_j] ) );
           }
           Node eq_exp = temp_exp.empty() ? d_true :