diff options
Diffstat (limited to 'test/regress/regress0/strings/artemis-0512-nonterm.smt2')
| -rw-r--r-- | test/regress/regress0/strings/artemis-0512-nonterm.smt2 | 25 |
1 files changed, 25 insertions, 0 deletions
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) + |