From 9b9864d639ccf474dedd66c5691c93ca17b670e9 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 17 Aug 2015 22:31:47 -0500 Subject: [PATCH] fix for bug663 --- src/theory/strings/theory_strings.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 : -- 2.30.2