string fmf perfomance fix

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4e20ac248363cc668a4fd95594a15b9bc95a39f7..a4c0c00b8b0aa05b92665bd7fa47d8f34bd7d661 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -356,12 +356,12 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
          if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){
                  Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-                 //Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero);
-                 Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR,
-                       n_len.eqNode( d_zero ),
-                       NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+                 Node n_len_eq_z = n_len.eqNode( d_zero );
+                 Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
+                                                                       NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
                  Trace("strings-lemma") << "Strings::Lemma LENGTH geq 0 : " << n_len_geq_zero << std::endl;
                  d_out->lemma(n_len_geq_zero);
+                 d_out->requirePhase( n_len_eq_z, true );
          }
          // FMF
          if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() &&