1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2
new file mode 100644
index 000000000..5c4771d71
--- /dev/null
+++ b/test/regress/regress0/strings/cardinality.smt2
@@ -0,0 +1,23 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(set-option :str-cardinality 2)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(declare-fun i () Int)
+
+(assert (= i 1))
+(assert (= (str.len x) i))
+(assert (= (str.len y) i))
+(assert (= (str.len z) i))
+(assert (= (str.len w) 2))
+
+(assert (not (=  x y)))
+(assert (not (=  x z)))
+(assert (not (=  z y)))
+
+
+(check-sat)