From ed61fb35596949aaa59ba5481c823f2ba99b6b5c Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 7 Mar 2014 12:35:15 -0600
Subject: bring back D-Norm

---
 src/theory/strings/theory_strings.cpp | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/theory')

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f819d46fb..fd9605e59 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1979,10 +1979,10 @@ void TheoryStrings::checkDeqNF() {
 			for( unsigned j=0; j<cols[i].size(); j++ ){
 				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 );
-					//	return;
-					//}else{
+					if( !areDisequal( cols[i][j], cols[i][k] ) ){
+						sendSplit( cols[i][j], cols[i][k], "D-NORM", false );
+						return;
+					}else{
 						Trace("strings-solve") << "- Compare ";
 						printConcat( d_normal_forms[cols[i][j]], "strings-solve" );
 						Trace("strings-solve") << " against ";
@@ -1991,7 +1991,7 @@ void TheoryStrings::checkDeqNF() {
 						if( processDeq( cols[i][j], cols[i][k] ) ){
 							return;
 						}
-					//}
+					}
 				}
 			}
 		}
-- 
cgit v1.2.3