diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-15 01:26:22 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-15 01:26:22 -0800 |
commit | 76dc42ce7e4a156b4381994b5562a41e5d6b9985 (patch) | |
tree | 8ee599bff81ed29bdcb77945de4cdc61c70e20be /src | |
parent | e644cb6dc8b5b8c64663bd4e57d14e1d86588695 (diff) |
simplify
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5179ddab3..71a0ef63a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3195,7 +3195,6 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal Node firstChar = stra.size() == 1 ? const_str : NodeManager::currentNM()->mkConst( isRev ? stra.suffix( 1 ) : stra.prefix( 1 ) ); Node sk = d_sk_cache.mkSkolemCached( other_str, - firstChar, isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT, "c_spt"); @@ -3570,11 +3569,10 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { } }else{ Node sk = d_sk_cache.mkSkolemCached( - nconst_k, firstChar, SkolemCache::SK_ID_DC_SPT, "dc_spt"); + nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt"); registerLength(sk, LENGTH_ONE); Node skr = d_sk_cache.mkSkolemCached(nconst_k, - firstChar, SkolemCache::SK_ID_DC_SPT_REM, "dc_spt_rem"); Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) ); |