diff options
Diffstat (limited to 'test/regress/regress0/strings')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/artemis-0512-nonterm.smt2 | 25 |
2 files changed, 27 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index dd3c6b53a..ddc0eae7c 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -47,7 +47,8 @@ TESTS = \ loop007.smt2 \ loop008.smt2 \ loop009.smt2 \ - reloop.smt2 + reloop.smt2 \ + artemis-0512-nonterm.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 b/test/regress/regress0/strings/artemis-0512-nonterm.smt2 new file mode 100644 index 000000000..ed97f36dd --- /dev/null +++ b/test/regress/regress0/strings/artemis-0512-nonterm.smt2 @@ -0,0 +1,25 @@ +(set-logic QF_S) +(set-info :status unsat) + +(declare-const Y String) +(assert + (or + (= Y "01") + (= Y "02") + (= Y "03") + (= Y "04") + (= Y "05") + (= Y "06") + (= Y "07") + (= Y "08") + (= Y "09") + (= Y "10") + (= Y "11") + (= Y "12") + ) +) + +(assert (= (<= (str.to.int Y) 31) false)) + +(check-sat) + |