test/regress/regress1/strings/artemis-0512-nonterm.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

(set-info :smt-lib-version 2.5)
(set-logic QF_SLIA)
(set-option :strings-exp true)
(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)