summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/strings-native-simple.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/strings/strings-native-simple.cvc')
-rw-r--r--test/regress/regress0/strings/strings-native-simple.cvc10
1 files changed, 0 insertions, 10 deletions
diff --git a/test/regress/regress0/strings/strings-native-simple.cvc b/test/regress/regress0/strings/strings-native-simple.cvc
deleted file mode 100644
index 568452e12..000000000
--- a/test/regress/regress0/strings/strings-native-simple.cvc
+++ /dev/null
@@ -1,10 +0,0 @@
-% EXPECT: sat
-
-x : STRING;
-y : STRING;
-
-ASSERT x = CONCAT( "abcd", y );
-ASSERT LENGTH( x ) >= 6;
-ASSERT LENGTH( y ) < 5;
-
-CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback