From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sun, 18 Sep 2016 22:21:17 +0000 (-0500)
Subject: Minor fix for strings
X-Git-Tag: cvc5-1.0.0~6028^2~41
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c7f820d981d63b6fe2b0f4469b7b4527318f61d0;p=cvc5.git

Minor fix for strings
---

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 ) );