blob: af8ee945d294d3895886e49f3bb75b8d3a846186 (
plain)
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
28
29
|
; COMMAND-LINE: --fmf-bound-lazy
; EXPECT: unsat
(set-option :incremental "false")
(set-info :status unsat)
(set-logic ALL)
(declare-fun Y () String)
(set-info :notes "ufP_1 is uf type conv P")
(declare-fun ufP_1 (Int) Int)
(set-info :notes "ufM_2 is uf type conv M")
(declare-fun ufM_2 (Int) Int)
(declare-fun z1_3 () String)
(declare-fun z2_4 () String)
(declare-fun z3_5 () String)
(declare-fun V_253 () String)
(declare-fun V_254 () String)
(assert (or (= Y "1") (= Y "0")))
(assert (>= (ufP_1 0) 32))
(assert
(forall ((V_243 Int))
(or
(not (and (>= V_243 0) (>= (+ (str.len Y) (* (- 1) V_243)) 1)))
(and
(or (not (= (str.len Y) (+ 1 V_243))) (= (ufP_1 V_243) (ufM_2 V_243)))
(not (>= (ufM_2 V_243) 10))
(not (or (not (= (str.len Y) (+ 1 V_243 (str.len V_253)))) (not (= Y (str.++ V_253 (ite (= (ufM_2 V_243) 0) "0" "1") V_254)))) ))) ))
(check-sat)
|
