diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 630b2ae65..d4a3cf9c5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -527,7 +527,7 @@ void TheoryStrings::check(Effort e) { } doPendingFacts(); - if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) { + if( !d_conflict && ( ( e == EFFORT_FULL && !d_valuation.needCheck() ) || ( e==EFFORT_STANDARD && options::stringEager() ) ) ) { Trace("strings-check") << "Theory of strings full effort check " << std::endl; if(Trace.isOn("strings-eqc")) { @@ -573,7 +573,7 @@ void TheoryStrings::check(Effort e) { if( !hasProcessed() ){ checkFlatForms(); Trace("strings-process") << "Done check flat forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; - if( !hasProcessed() ){ + if( !hasProcessed() && e==EFFORT_FULL ){ checkNormalForms(); Trace("strings-process") << "Done check normal forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; if( !hasProcessed() ){ |