From 700a21a55d277d7bb4e475849e98aab58d91dba5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 11 Sep 2018 21:15:28 -0500 Subject: [PATCH] Fix for when strings process loop is disabled. (#2456) --- src/theory/strings/theory_strings.cpp | 20 ++++++++++---------- 1 file 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 -- 2.30.2