Add requirePhase len(x) = 0.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 862f5c7bc70c0dc0771097c4a9b30a30d3414783..6d2dc3138e458469b9d3a7bedef91c0cb5eac05e 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1947,11 +1947,13 @@ void TheoryStrings::sendLengthLemma( Node n ){
   //registerTerm( d_emptyString );
   Node n_len_eq_z_2 = n.eqNode( d_emptyString );
   n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
+  n_len_eq_z_2 = Rewriter::rewrite( n_len_eq_z_2 );
   Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, NodeManager::currentNM()->mkNode( kind::AND, n_len_eq_z, n_len_eq_z_2 ),
               NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
   Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
   d_out->lemma(n_len_geq_zero);
   d_out->requirePhase( n_len_eq_z, true );
+  d_out->requirePhase( n_len_eq_z_2, true );
 }
 
 Node TheoryStrings::mkConcat( Node n1, Node n2 ) {