296670420958aa9cf6573b1c72dd7932faa46a31
2 YICES
=~
/projects
/yices-2.4
.2/bin
/yices-smt
17 $( for i in $(seq 0 $ITERATIONS); do
18 echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int) (p$i Int)"
24 (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0) (= p0 0))
26 for i
in $
(seq 1 $ITERATIONS); do
32 (and ;-- SPECIAL CASE FOR STATE S(0)
36 (= a$i (- a$((i-1)) p$i))
37 (= b$i (- b$((i-1)) p$i))
38 (= c$i (- c$((i-1)) p$i))
50 (and ;-- CASE FOR STATE A(1)
52 (>= d$i 0) (<= d$i t$((i-1)))
53 (<= d$i (+ p$i (- $AMAX a$((i-1)))))
54 (= t$i (- t$((i-1)) d$i))
55 (= a$i (- (+ a$((i-1)) d$i) p$i))
57 (= b$i (- b$((i-1)) p$i))
58 (= c$i (- c$((i-1)) p$i))
60 (and ;-- CAME FROM S(0)
63 ) (and ;-- CAME FROM B(2)
66 ) (and ;-- CAME FROM C(3)
72 (and ;-- CASE FOR STATE B(2)
74 (>= d$i 0) (<= d$i t$((i-1)))
75 (<= d$i (+ p$i (- $BMAX b$((i-1)))))
76 (= t$i (- t$((i-1)) d$i))
77 (= b$i (- (+ b$((i-1)) d$i) p$i))
79 (= a$i (- a$((i-1)) p$i))
80 (= c$i (- c$((i-1)) p$i))
83 (and ;-- CAME FROM S(0)
86 ) (and ;-- CAME FROM A(1)
89 ) (and ;-- CAME FROM C(3)
95 (and ;-- CASE FOR STATE C(3)
97 (>= d$i 0) (<= d$i t$((i-1)))
98 (<= d$i (+ p$i (- $CMAX c$((i-1)))))
99 (= t$i (- t$((i-1)) d$i))
100 (= c$i (- (+ c$((i-1)) d$i) p$i))
101 (= a$i (- a$((i-1)) p$i))
102 (= b$i (- b$((i-1)) p$i))
104 (and ;-- CAME FROM A(1)
107 ) (and ;-- CAME FROM B(2)
121 until generate
$it 300 |
$YICES |
grep "unsat"
125 generate
9 300 |
$YICES -m |
sort