diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 35835398c..902ce460e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3051,6 +3051,11 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form ss << "Looping word equation encountered." << std::endl; throw LogicException(ss.str()); } + if (!options::stringProcessLoop()) + { + d_out->setIncomplete(); + return false; + } NodeManager* nm = NodeManager::currentNM(); Node conc; Trace("strings-loop") << "Detected possible loop for " @@ -3228,16 +3233,11 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form d_regexp_ant[str_in_re] = ant; } // we will be done - if (options::stringProcessLoop()) - { - info.d_conc = conc; - info.d_id = INFER_FLOOP; - info.d_nf_pair[0] = normal_form_src[i]; - info.d_nf_pair[1] = normal_form_src[j]; - return true; - } - d_out->setIncomplete(); - return false; + info.d_conc = conc; + info.d_id = INFER_FLOOP; + info.d_nf_pair[0] = normal_form_src[i]; + info.d_nf_pair[1] = normal_form_src[j]; + return true; } //return true for lemma, false if we succeed |