diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1bc104096..ba59b4e4f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3412,6 +3412,21 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, isRev ? utils::mkNConcat(sk, nfiv[index]) : utils::mkNConcat(nfiv[index], sk)); + Node eqs = d_true; + if (!isRev) + { + sk.eqNode(d_sk_cache.mkSkolemCached( + nfiv[index], + nfjv[index], + SkolemCache::SK_FIRST_CTN_POST, + "v_spt1")) + .orNode(sk.eqNode(d_sk_cache.mkSkolemCached( + nfjv[index], + nfiv[index], + SkolemCache::SK_FIRST_CTN_POST, + "v_spt2"))); + } + if( lentTestSuccess!=-1 ){ info.d_antn.push_back( lentTestExp ); info.d_conc = lentTestSuccess==0 ? eq1 : eq2; @@ -3425,7 +3440,10 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, info.d_antn.push_back(ldeq); } //set info - info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + info.d_conc = nm->mkNode( + AND, + eqs, + NodeManager::currentNM()->mkNode(kind::OR, eq1, eq2)); info.d_id = INFER_SSPLIT_VAR; info_valid = true; } |