diff options
Diffstat (limited to 'src/theory/strings/skolem_cache.h')
| -rw-r--r-- | src/theory/strings/skolem_cache.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index c1e3c7214..8fcf46c14 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -59,10 +59,6 @@ class SkolemCache // exists k. a = "c" ++ k SK_ID_VC_SPT, SK_ID_VC_SPT_REV, - // a != "" ^ b = "cccccccc" ^ len(a)!=len(b) a ++ a' = b = b' => - // exists k. a = "cccc" ++ k OR ( len(k) > 0 ^ "cccc" = a ++ k ) - SK_ID_VC_BIN_SPT, - SK_ID_VC_BIN_SPT_REV, // a != "" ^ b != "" ^ len(a)!=len(b) ^ a ++ a' = b ++ b' => // exists k. len( k )>0 ^ ( a ++ k = b OR a = b ++ k ) SK_ID_V_SPT, |