diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5179ddab3..405061a2d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3285,6 +3285,10 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal } bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j, unsigned rproc ){ + if (!options::stringProcessLoop()) + { + return false; + } int has_loop[2] = { -1, -1 }; if( options::stringLB() != 2 ) { for( unsigned r=0; r<2; r++ ) { @@ -3318,11 +3322,6 @@ 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 " |