diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-22 18:23:23 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-22 18:23:23 -0800 |
commit | 29badd153b7ece62ff18d5545ed8054389e79a77 (patch) | |
tree | e6c43c29406e779de59845518cd930048a7a4d58 | |
parent | c8f205e9eafbb9b6df3c6624405b36dec5723c38 (diff) |
split different
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4eaa9c3aa..becf66ada 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3302,10 +3302,10 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, "c_spt"); Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl; //set info - info.d_conc = other_str.eqNode( + info.d_conc = nm->mkNode(OR, other_str.eqNode(prea), other_str.eqNode( isRev ? utils::mkNConcat(sk, prea) - : utils::mkNConcat(prea, sk)); - info.d_new_skolem[LENGTH_SPLIT].push_back(sk); + : utils::mkNConcat(prea, sk))); + info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk); info.d_id = INFER_SSPLIT_CST_PROP; info_valid = true; } @@ -3348,12 +3348,12 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi, other_str, isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT, - "c_spt"); + "vc_spt"); Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (serial) " << std::endl; - info.d_conc = other_str.eqNode( + info.d_conc = nm->mkNode(OR, other_str.eqNode(firstChar), other_str.eqNode( isRev ? utils::mkNConcat(sk, firstChar) - : utils::mkNConcat(firstChar, sk)); - info.d_new_skolem[LENGTH_SPLIT].push_back(sk); + : utils::mkNConcat(firstChar, sk))); + info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk); info.d_id = INFER_SSPLIT_CST; info_valid = true; } |