From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 16 Mar 2015 16:04:43 +0000 (-0500)
Subject: Add requirePhase len(x) = 0.
X-Git-Tag: cvc5-1.0.0~6373
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=973cbd67611a2943714fd9544d098ec1472a40b8;p=cvc5.git

Add requirePhase len(x) = 0.
---

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 ) {