diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-11 21:15:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-11 21:15:28 -0500 |
commit | 700a21a55d277d7bb4e475849e98aab58d91dba5 (patch) | |
tree | c9802fbb5fdd5012a6c7098afd4c988473497d27 | |
parent | 078c8bcafbdeeb920642ff9326cf46fc72a2efe8 (diff) |
Fix for when strings process loop is disabled. (#2456)
-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 |