diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-18 17:21:17 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-18 17:21:31 -0500 |
| commit | c7f820d981d63b6fe2b0f4469b7b4527318f61d0 (patch) | |
| tree | dd02a26234dfbe0e15d1cad8cc6806dfcabf6ff6 /src | |
| parent | 53d625529c90c81b46a08811e4143552095fff9a (diff) | |
Minor fix for strings
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4526300f8..0062028fe 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2954,7 +2954,7 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { } }else{ Node sk = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt, "dc_spt", 2 ); - Node skr = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt_rem, "dc_spt_rem", -1 ); + Node skr = mkSkolemCached( nconst_k, firstChar, sk_id_dc_spt_rem, "dc_spt_rem" ); Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) ); eq1 = Rewriter::rewrite( eq1 ); Node eq2 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, skr ) ); |