Fix for when strings process loop is disabled. (#2456)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 35835398c6be1a672963c86c75f8470f8ab16592..902ce460ee962c21fd4c0d61fa378c756d0389bc 100644 (file)
--- 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