diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-24 23:27:44 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-24 23:47:26 -0800 |
commit | cbc95f2b8b73de8d2fe04a54c908a11ceed135f1 (patch) | |
tree | a4a7a3bad1482129db76687a59f4aa71c8fc1022 | |
parent | dd29958ff0c78c099f540f080e455d843caf1c6b (diff) |
Fix skolem length
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1bc104096..9949bcea4 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3758,7 +3758,8 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { { Node sk = d_sk_cache.mkSkolemCached( nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt"); - d_im.registerLength(sk, LENGTH_ONE); + d_im.registerLength(sk, LENGTH_SPLIT); + Node lenreq = nm->mkNode(STRING_LENGTH, sk).eqNode(d_one); Node skr = d_sk_cache.mkSkolemCached(nconst_k, SkolemCache::SK_ID_DC_SPT_REM, @@ -3776,7 +3777,7 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { antec, nm->mkNode( OR, - nm->mkNode(AND, eq1, sk.eqNode(firstChar).negate()), + nm->mkNode(AND, lenreq, eq1, sk.eqNode(firstChar).negate()), eq2), "D-DISL-CSplit"); d_im.sendPhaseRequirement(eq1, true); |