diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-08-17 22:31:47 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-08-17 22:31:47 -0500 |
| commit | 9b9864d639ccf474dedd66c5691c93ca17b670e9 (patch) | |
| tree | 903a6978bea117b655486ef2665e48d6d0618203 | |
| parent | 7c798a5a2085754b26a0720d162b2ee45a705c4e (diff) | |
fix for bug663
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files 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 : |