diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 | 9 |
2 files changed, 11 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 771b9f031..3daf646ab 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -76,7 +76,8 @@ TESTS = \ type002.smt2 \ crash-1019.smt2 \ norn-31.smt2 \ - strings-native-simple.cvc + strings-native-simple.cvc \ + cmu-2db2-extf-reg.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 new file mode 100644 index 000000000..b513494b8 --- /dev/null +++ b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun s () String) + +(assert (and (not (not (= (ite (= (str.indexof s "bar" 1) (- 1)) 1 0) 0))) (not (not (= (ite (= (str.indexof s "bar" 1) 3) 1 0) 0))))) + +(check-sat) |