From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 12 Sep 2018 02:15:28 +0000 (-0500)
Subject: Fix for when strings process loop is disabled. (#2456)
X-Git-Tag: cvc5-1.0.0~4658
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=700a21a55d277d7bb4e475849e98aab58d91dba5;p=cvc5.git

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 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