projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
53d6255
)
Minor fix for strings
author
ajreynol
<andrew.j.reynolds@gmail.com>
Sun, 18 Sep 2016 22:21:17 +0000
(17:21 -0500)
committer
ajreynol
<andrew.j.reynolds@gmail.com>
Sun, 18 Sep 2016 22:21:31 +0000
(17:21 -0500)
src/theory/strings/theory_strings.cpp
patch
|
blob
|
history
diff --git
a/src/theory/strings/theory_strings.cpp
b/src/theory/strings/theory_strings.cpp
index 4526300f8cc9177da3af37acec88379f80664edc..0062028fe2c2e4df80d5b853cd12f373930f4cc9 100644
(file)
--- 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 ) );