summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r--src/theory/strings/theory_strings.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f2af6452b..efb737a29 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1830,9 +1830,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & n
}
nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() );
nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() );
- //if( eqc!=normal_form_src[nf_index] ){
- // nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) );
- //}
+ if( eqc!=normal_form_src[nf_index] ){
+ nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) );
+ }
Trace("strings-solve-debug2") << "take normal form ... done" << std::endl;
d_normal_forms_base[eqc] = normal_form_src[nf_index];
//*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback