From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 23 Oct 2013 16:45:34 +0000 (-0500)
Subject: bug fix for loop rule
X-Git-Tag: cvc5-1.0.0~7275^2~2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d5c0a5347e8389e2c40fc5fe0373ff36d151991;p=cvc5.git

bug fix for loop rule
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 11024e351..7c3e7ebbc 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -991,8 +991,15 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
 												//try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
 												sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty" );
 												return true;
-											}else{
+											} else if( !areDisequal( t_yz, d_emptyString ) ) {
+												//TODO...........
+												//try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop
+												sendSplit( t_yz, d_emptyString, "Loop Empty" );
+												return true;
+											} else {
 												//need to break
+												antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() );
+												antec.push_back( t_yz.eqNode( d_emptyString ).negate() );
 												Node ant = mkExplain( antec, antec_new_lits );
 												Node str_in_re;
 												if( s_zy == t_yz &&