diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 862f5c7bc..6d2dc3138 100644 --- 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 ) { |