diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-10 14:12:16 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-21 02:29:21 -0800 |
| commit | 295ec1fb86977c70ea07eabcbb95a6a646c7cb74 (patch) | |
| tree | 021c897730f983a7f6f79c9160316682786653b2 /src/theory/strings/theory_strings.cpp | |
| parent | 19a4e3f33b166aeefdcf47e7bb17332a45460464 (diff) | |
revert change
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 20 |
1 files changed, 1 insertions, 19 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 415cefd0b..1e4f13f74 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3419,21 +3419,6 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, isRev ? utils::mkNConcat(sk2, nfiv[index]) : utils::mkNConcat(nfiv[index], sk2)); - 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; @@ -3447,10 +3432,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, info.d_antn.push_back(ldeq); } //set info - info.d_conc = nm->mkNode( - AND, - eqs, - NodeManager::currentNM()->mkNode(kind::OR, eq1, eq2)); + info.d_conc = NodeManager::currentNM()->mkNode(kind::OR, eq1, eq2); info.d_id = INFER_SSPLIT_VAR; info_valid = true; } |