renames for strings fmf

diff --git a/src/theory/strings/options b/src/theory/strings/options
index 2832c7833df32cb3da7666a930662b2a700482be..58cbbc1b13e7c44ae5f1795ec9f6cc518404e833 100644 (file)
--- 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 1aae55a8361028546b30489409dabec5232af1cb..c4ecd02cf087dc784c238e9ebc642efde8046d28 100644 (file)
--- 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();