From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 16 Oct 2013 15:16:59 +0000 (-0500)
Subject: renames for strings fmf
X-Git-Tag: cvc5-1.0.0~7275^2~14
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=04868401c51b7f29c2b43ebc508dea59769dae93;p=cvc5.git

renames for strings fmf
---

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 2832c7833..58cbbc1b1 100644
--- a/src/theory/strings/options
+++ b/src/theory/strings/options
@@ -11,7 +11,7 @@ option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :de
 option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write
  the depth of unrolloing regular expression used by the theory of strings, default 10
 
-option stringFMF fmf-strings --fmf-strings bool :default false
+option stringFMF strings-fmf --str-fmf bool :default false
  the finite model finding used by the theory of strings
 
 endmodule
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1aae55a83..c4ecd02cf 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1908,7 +1908,7 @@ bool TheoryStrings::checkMemberships() {
 }
 
 Node TheoryStrings::getNextDecisionRequest() {
-	if(d_fmf) {
+	if(d_fmf && !d_conflict) {
 		Trace("strings-decide") << "Get next decision request." << std::endl;
 		Trace("strings-fmf-debug") << "Input variables: ";
 		for(std::vector< Node >::iterator itr = d_in_vars.begin();
@@ -1916,6 +1916,8 @@ Node TheoryStrings::getNextDecisionRequest() {
 				Trace("strings-fmf-debug") << " " << (*itr) ;
 			}
 		Trace("strings-fmf-debug") << std::endl;
+
+
 	}
 
 	return Node::null();