summaryrefslogtreecommitdiff
path: root/src/theory/strings/skolem_cache.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/skolem_cache.h')
-rw-r--r--src/theory/strings/skolem_cache.h3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index b1dc48f75..2cd03bfe6 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -68,8 +68,7 @@ class SkolemCache
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_X,
- SK_ID_V_SPT_Y,
+ SK_ID_V_SPT,
SK_ID_V_SPT_REV,
// a != "" ^ b = "c" ^ a ++ a' != b ++ b' =>
// exists k, k_rem.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback