blob: bc2d0166c7f54c142933dc91946da61038d08fe7 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(set-option :incremental false)
(set-info :status sat)
(set-logic QF_UFLIA)
(declare-fun format (Int) Int)
(declare-fun arg1 () Int)
(declare-fun fmt1 () Int)
(declare-fun s_count (Int) Int)
(declare-fun fmt0 () Int)
(declare-fun x_count (Int) Int)
(check-sat-assuming ( (let ((_let_0 (* (- 1) fmt1))) (let ((_let_1 (+ _let_0 fmt0))) (let ((_let_2 (* (- 1) (x_count 7)))) (let ((_let_3 (+ fmt1 (- 2) (* (- 1) fmt0)))) (let ((_let_4 (s_count _let_3))) (let ((_let_5 (>= (x_count 1) 0))) (and true (>= _let_1 (- 8)) (>= (+ (x_count 6) _let_2) 0) (>= fmt1 7) (<= arg1 6) (not (= 0 (+ _let_4 (* (- 1) (s_count 5))))) (<= _let_1 (- 7)) (or false false (<= (+ arg1 (* (- 1) fmt0)) 1) (<= (+ _let_0 arg1) 0)) _let_5 (<= (format 7) 0) (or false false false false false _let_5 (= 0 (+ _let_2 (x_count _let_3))) (= 0 (+ _let_4 (* (- 1) (s_count 6))))) (>= (format (+ 1 fmt1)) 0) (>= (format 4) 0) (<= (format 9) 0) (>= (format fmt1) 0) (>= (format 12) 0) (= 0 (format arg1))))))))) ))
|
