diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-20 17:10:03 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-20 17:10:03 -0500 |
| commit | 453ae55ac7adcda70b4dfbc95c78e899961c8e2d (patch) | |
| tree | d74bc7ca24a3b33410458c5b138d87c4f610ab39 /test/regress/regress0/strings | |
| parent | d5d05e4723581c86808a866af1a9f20343ed36dc (diff) | |
Minor fix to strings, cleanup in datatypes.
Diffstat (limited to 'test/regress/regress0/strings')
| -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) |