diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-13 16:29:01 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-13 16:29:01 -0500 |
| commit | d87431b64a27c073e31652166a24f0c87b22c041 (patch) | |
| tree | 196f945174c60d401c41c6112dcd8f30f2cbee80 /test | |
| parent | 199cf857baa106545196503cc4029e2b7771d1af (diff) | |
Update native language support for strings.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/strings-native-simple.cvc | 10 |
2 files changed, 12 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 2058f429b..771b9f031 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -75,7 +75,8 @@ TESTS = \ fmf001.smt2 \ type002.smt2 \ crash-1019.smt2 \ - norn-31.smt2 + norn-31.smt2 \ + strings-native-simple.cvc FAILING_TESTS = diff --git a/test/regress/regress0/strings/strings-native-simple.cvc b/test/regress/regress0/strings/strings-native-simple.cvc new file mode 100644 index 000000000..568452e12 --- /dev/null +++ b/test/regress/regress0/strings/strings-native-simple.cvc @@ -0,0 +1,10 @@ +% EXPECT: sat + +x : STRING; +y : STRING; + +ASSERT x = CONCAT( "abcd", y ); +ASSERT LENGTH( x ) >= 6; +ASSERT LENGTH( y ) < 5; + +CHECKSAT; |