diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4e20ac248..a4c0c00b8 100644 --- 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() && |