diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7ebc5f35f..33377e7f5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2736,14 +2736,23 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, if (d_state.areEqual(length_term_i, length_term_j)) { Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl; - Node eq = nfiv[index].eqNode(nfjv[index]); //eq = Rewriter::rewrite( eq ); Node length_eq = length_term_i.eqNode( length_term_j ); //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); NormalForm::getExplanationForPrefixEq( nfi, nfj, index, index, temp_exp); temp_exp.push_back(length_eq); - d_im.sendInference(temp_exp, eq, "N_Unify"); + + if (d_state.areDisequal(nfiv[index], nfjv[index])) + { + temp_exp.push_back(nfiv[index].eqNode(nfjv[index]).negate()); + d_im.sendInference(temp_exp, d_false, "N_Unify"); + } + else + { + Node eq = nfiv[index].eqNode(nfjv[index]); + d_im.sendInference(temp_exp, eq, "N_Unify"); + } return; } else if ((nfiv[index].getKind() != CONST_STRING |