blob: 78cdb2a8cf7a088207f372c717cd39bf8ea6805b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-option :strings-exp true)
(set-info :status sat)
(declare-const x String)
(declare-const y String)
(declare-const m String)
(declare-const n String)
(assert (str.in.re x (re.+ (re.range "0" "9"))))
(assert (= 0 (str.to.int x)))
(assert (not (= x "")))
(assert (not (= x "0")))
(assert (not (= x "3")))
(assert (not (= x "T")))
(assert (not (= x "8")))
(assert (not (= x "")))
(assert (not (= x "5")))
(assert (not (= x "<")))
(assert (not (= x "N")))
(check-sat)
|
