diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1947f1730..67f032193 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4468,19 +4468,29 @@ void TheoryStrings::checkNormalFormsDeq() for( unsigned j=0; j<cols[i].size(); j++ ){ for( unsigned k=(j+1); k<cols[i].size(); k++ ){ //for strings that are disequal, but have the same length - if( areDisequal( cols[i][j], cols[i][k] ) ){ - Assert( !d_conflict ); - if (Trace.isOn("strings-solve")) + if (cols[i][j].isConst() && cols[i][k].isConst()) + { + // if both are constants, they should be distinct, and its trivial + Assert(cols[i][j] != cols[i][k]); + } + else + { + if (areDisequal(cols[i][j], cols[i][k])) { - Trace("strings-solve") << "- Compare " << cols[i][j] << " "; - printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve"); - Trace("strings-solve") << " against " << cols[i][k] << " "; - printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve"); - Trace("strings-solve") << "..." << std::endl; - } - processDeq( cols[i][j], cols[i][k] ); - if( hasProcessed() ){ - return; + Assert(!d_conflict); + if (Trace.isOn("strings-solve")) + { + Trace("strings-solve") << "- Compare " << cols[i][j] << " "; + printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve"); + Trace("strings-solve") << " against " << cols[i][k] << " "; + printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve"); + Trace("strings-solve") << "..." << std::endl; + } + processDeq(cols[i][j], cols[i][k]); + if (hasProcessed()) + { + return; + } } } } |