From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 17 Apr 2015 19:41:24 +0000 (-0500)
Subject: Patch for Kshitij's fix on requriePhase
X-Git-Tag: cvc5-1.0.0~6352
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d359ce4470c44c3e7532edb6b60bcb61b51f862;p=cvc5.git

Patch for Kshitij's fix on requriePhase
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 34ca52419..e8985e074 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2283,7 +2283,7 @@ void TheoryStrings::checkDeqNF() {
         for( unsigned k=(j+1); k<cols[i].size(); k++ ){
           Assert( !d_conflict );
           if( !areDisequal( cols[i][j], cols[i][k] ) ){
-            sendSplit( cols[i][j], cols[i][k], "D-NORM", false );
+            sendSplit( cols[i][j], cols[i][k], "D-NORM", true );
             return;
           }else{
             Trace("strings-solve") << "- Compare ";
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 420361af3..d521680d5 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -33,6 +33,7 @@ TESTS =	\
   str007.smt2 \
   fmf002.smt2 \
   type001.smt2 \
+  type003.smt2 \
   model001.smt2 \
   substr001.smt2 \
   regexp001.smt2 \
@@ -45,6 +46,7 @@ TESTS =	\
   loop004.smt2 \
   loop005.smt2 \
   loop006.smt2 \
+  loop007.smt2 \
   loop008.smt2 \
   loop009.smt2 \
   reloop.smt2 
@@ -55,8 +57,6 @@ FAILING_TESTS =
 EXTRA_DIST = $(TESTS) \
   artemis-0512-nonterm.smt2 \
   fmf001.smt2 \
-  type003.smt2 \
-  loop007.smt2 \
   type002.smt2
 
 #   slow after changes on Nov 20 : artemis-0512-nonterm.smt2