summaryrefslogtreecommitdiff
path: root/test/regress/regress0
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0')
-rw-r--r--test/regress/regress0/strings/Makefile.am3
-rw-r--r--test/regress/regress0/strings/issue1189.smt26
2 files changed, 8 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 6cdba7c9d..e27a1bfcd 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -89,7 +89,8 @@ TESTS = \
repl-empty-sem.smt2 \
bug799-min.smt2 \
strings-charat.cvc \
- issue1105.smt2
+ issue1105.smt2 \
+ issue1189.smt2
FAILING_TESTS =
diff --git a/test/regress/regress0/strings/issue1189.smt2 b/test/regress/regress0/strings/issue1189.smt2
new file mode 100644
index 000000000..fae641ea8
--- /dev/null
+++ b/test/regress/regress0/strings/issue1189.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :strings-exp true)
+(declare-const x Int)
+(assert (str.contains (str.++ "some text" (int.to.str x) "tor") "vector"))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback