summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2015-09-28 10:56:28 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2015-09-28 10:56:28 +0200
commite00d64b2e4eb32a8ea21e211957d708afa89405a (patch)
treea9d0d546941afd1792c8901b63b861b5225d6b13 /test/regress/regress0/strings
parentfd186a7a53bc6c521eea2b83a5529ec2854d4428 (diff)
Add missing regression
Diffstat (limited to 'test/regress/regress0/strings')
-rwxr-xr-xtest/regress/regress0/strings/idof-triv.smt27
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/idof-triv.smt2 b/test/regress/regress0/strings/idof-triv.smt2
new file mode 100755
index 000000000..314adedf8
--- /dev/null
+++ b/test/regress/regress0/strings/idof-triv.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :strings-exp true)
+(declare-fun string () String)
+;(assert (= string "::"))
+(assert (> (str.indexof string ":" 0) 0))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback