blob: d90dae95ee7e8da819624a3195d842c6423db3f7 (
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(benchmark mode_cntrl.induction.smt
:source {
The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html.
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
:status unsat
:category { industrial }
:difficulty { 0 }
:logic QF_LRA
:extrafuns ((x_0 Real))
:extrapreds ((x_1))
:extrapreds ((x_2))
:extrapreds ((x_3))
:extrafuns ((x_4 Real))
:extrafuns ((x_5 Real))
:extrafuns ((x_6 Real))
:extrafuns ((x_7 Real))
:extrapreds ((x_8))
:extrafuns ((x_9 Real))
:extrafuns ((x_10 Real))
:extrapreds ((x_11))
:extrapreds ((x_12))
:extrapreds ((x_13))
:extrapreds ((x_14))
:extrapreds ((x_15))
:extrapreds ((x_16))
:extrapreds ((x_17))
:extrapreds ((x_18))
:extrapreds ((x_19))
:extrapreds ((x_20))
:extrapreds ((x_21))
:extrapreds ((x_22))
:extrafuns ((x_23 Real))
:extrafuns ((x_24 Real))
:extrafuns ((x_25 Real))
:extrafuns ((x_26 Real))
:extrafuns ((x_27 Real))
:extrafuns ((x_28 Real))
:extrafuns ((x_29 Real))
:extrapreds ((x_30))
:extrapreds ((x_31))
:extrapreds ((x_32))
:extrapreds ((x_33))
:extrapreds ((x_34))
:extrapreds ((x_35))
:extrapreds ((x_36))
:extrapreds ((x_37))
:extrafuns ((x_38 Real))
:extrafuns ((x_39 Real))
:extrafuns ((x_40 Real))
:extrafuns ((x_41 Real))
:extrafuns ((x_42 Real))
:extrafuns ((x_43 Real))
:extrafuns ((x_44 Real))
:extrafuns ((x_45 Real))
:extrafuns ((x_46 Real))
:extrafuns ((x_47 Real))
:extrafuns ((x_48 Real))
:extrafuns ((x_49 Real))
:extrafuns ((x_50 Real))
:extrafuns ((x_51 Real))
:extrafuns ((x_52 Real))
:extrapreds ((x_53))
:extrafuns ((x_54 Real))
:extrafuns ((x_55 Real))
:extrafuns ((x_56 Real))
:formula
(let (?cvcl_26 (+ x_4 x_5)) (flet ($cvcl_73 (<= x_6 x_7)) (flet ($cvcl_54 (iff x_8 x_2)) (flet ($cvcl_77 (= x_9 0)) (flet ($cvcl_10 $cvcl_77) (flet ($cvcl_11 (< x_6 x_10)) (flet ($cvcl_38 (= x_7 x_6)) (flet ($cvcl_61 $cvcl_38) (flet ($cvcl_81 (= x_9 2)) (flet ($cvcl_62 $cvcl_81) (flet ($cvcl_64 (iff x_11 x_12)) (flet ($cvcl_65 (and (iff x_13 x_14) (iff x_15 x_16))) (flet ($cvcl_52 (iff x_17 x_18)) (flet ($cvcl_53 (and (iff x_19 x_20) (iff x_21 x_22))) (flet ($cvcl_66 (= x_23 x_24)) (flet ($cvcl_67 (and (= x_25 x_26) (= x_27 x_28))) (flet ($cvcl_21 (= x_29 x_10)) (flet ($cvcl_51 (iff x_30 x_3)) (flet ($cvcl_49 (iff x_31 x_32)) (flet ($cvcl_50 (and (iff x_33 x_34) (iff x_35 x_36))) (flet ($cvcl_68 (iff x_37 x_1)) (let (?cvcl_74 (- x_38 x_4)) (flet ($cvcl_80 (= x_9 1)) (flet ($cvcl_42 $cvcl_80) (let (?cvcl_46 (+ x_5 x_4)) (flet ($cvcl_41 (<= x_39 x_7)) (flet ($cvcl_48 (iff x_11 (or x_12 (and $cvcl_41 x_32) ))) (flet ($cvcl_28 (<= x_42 ?cvcl_26)) (flet ($cvcl_30 (<= x_43 ?cvcl_26)) (flet ($cvcl_22 (<= x_42 x_5)) (flet ($cvcl_27 $cvcl_22) (flet ($cvcl_24 (<= x_43 x_5)) (flet ($cvcl_29 $cvcl_24) (flet ($cvcl_23 (not x_14)) (flet ($cvcl_33 $cvcl_23) (flet ($cvcl_55 (< x_42 x_6)) (flet ($cvcl_56 (= x_7 x_42)) (flet ($cvcl_25 (not x_16)) (flet ($cvcl_35 $cvcl_25) (flet ($cvcl_57 (< x_43 x_6)) (flet ($cvcl_58 (= x_7 x_43)) (flet ($cvcl_14 (not x_12)) (flet ($cvcl_37 $cvcl_14) (flet ($cvcl_75 (not $cvcl_73)) (flet ($cvcl_32 (not x_34)) (flet ($cvcl_34 (not x_36)) (flet ($cvcl_36 (not x_32)) (flet ($cvcl_39 (and (not $cvcl_22) (<= x_42 x_7))) (flet ($cvcl_40 (and (not $cvcl_24) (<= x_43 x_7))) (flet ($cvcl_47 (and (iff x_13 (or x_14 (and $cvcl_39 x_34) )) (iff x_15 (or x_16 (and $cvcl_40 x_36) )))) (flet ($cvcl_31 (<= x_39 ?cvcl_26)) (flet ($cvcl_59 (< x_39 x_6)) (flet ($cvcl_60 (= x_7 x_39)) (flet ($cvcl_63 (<= (ite x_18 (ite x_22 (ite x_20 3 2) x_40) (ite x_22 x_40 (ite x_20 1 0))) (* (* (ite x_12 (ite x_16 (ite x_14 0 1) x_41) (ite x_16 x_41 (ite x_14 2 3))) 1) (/ 1 2)))) (flet ($cvcl_76 $cvcl_41) (flet ($cvcl_43 (not $cvcl_28)) (flet ($cvcl_44 (not $cvcl_30)) (flet ($cvcl_0 (and (not (<= x_39 x_5)) $cvcl_41)) (flet ($cvcl_1 $cvcl_0) (flet ($cvcl_4 (and (not (<= x_44 x_5)) (<= x_44 x_7))) (flet ($cvcl_2 $cvcl_4) (flet ($cvcl_5 $cvcl_0) (flet ($cvcl_6 $cvcl_4) (flet ($cvcl_45 (not $cvcl_31)) (flet ($cvcl_20 (= x_23 0)) (flet ($cvcl_9 (= x_23 3)) (flet ($cvcl_16 (= x_25 0)) (flet ($cvcl_7 (= x_25 3)) (flet ($cvcl_18 (= x_27 0)) (flet ($cvcl_8 (= x_27 3)) (flet ($cvcl_69 (= x_0 0)) (flet ($cvcl_71 (not $cvcl_69)) (flet ($cvcl_70 (= x_0 1)) (flet ($cvcl_72 (not $cvcl_70)) (flet ($cvcl_3 (and (not (<= x_47 x_5)) (<= x_47 x_7))) (flet ($cvcl_12 (= x_25 (ite $cvcl_23 (ite (and $cvcl_39 (< x_26 3)) (+ x_26 1) x_26) x_26))) (flet ($cvcl_13 (= x_27 (ite $cvcl_25 (ite (and $cvcl_40 (< x_28 3)) (+ x_28 1) x_28) x_28))) (flet ($cvcl_15 (or x_14 $cvcl_7 )) (flet ($cvcl_17 (or x_16 $cvcl_8 )) (flet ($cvcl_19 (or x_12 $cvcl_9 )) (flet ($cvcl_78 (not x_37)) (flet ($cvcl_79 (not x_8)) (flet ($cvcl_82 (not x_30)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_9 2) (>= x_9 0)) (<= x_0 2)) (>= x_0 0)) (> x_4 0)) (>= x_4 0)) (>= x_5 0)) (>= x_6 0)) (>= x_7 0)) (>= x_10 0)) (or (or (or $cvcl_20 (= x_23 1) ) (= x_23 2) ) $cvcl_9 )) (not (< x_23 0))) (<= x_23 3)) (or (or (or (= x_24 0) (= x_24 1) ) (= x_24 2) ) (= x_24 3) )) (not (< x_24 0))) (<= x_24 3)) (or (or (or $cvcl_16 (= x_25 1) ) (= x_25 2) ) $cvcl_7 )) (not (< x_25 0))) (<= x_25 3)) (or (or (or (= x_26 0) (= x_26 1) ) (= x_26 2) ) (= x_26 3) )) (not (< x_26 0))) (<= x_26 3)) (or (or (or $cvcl_18 (= x_27 1) ) (= x_27 2) ) $cvcl_8 )) (not (< x_27 0))) (<= x_27 3)) (or (or (or (= x_28 0) (= x_28 1) ) (= x_28 2) ) (= x_28 3) )) (not (< x_28 0))) (<= x_28 3)) (>= x_29 0)) (>= x_38 0)) (>= x_39 0)) (>= x_42 0)) (>= x_43 0)) (>= x_44 0)) (>= x_47 0)) (>= x_50 0)) (>= x_51 0)) (not (<= x_52 (* x_4 3)))) (>= x_52 0)) (>= x_54 0)) (>= x_55 0)) (>= x_56 0)) (or $cvcl_71 (and x_1 x_2) )) (or $cvcl_72 (and x_3 x_2) )) (or (not (= x_0 2)) (and x_3 x_1) )) (= x_40 (ite x_20 2 1))) (= x_41 (ite x_14 1 2))) (= x_45 (ite $cvcl_1 2 1))) (= x_46 (ite $cvcl_5 2 1))) (= x_48 (+ (ite $cvcl_3 (ite $cvcl_2 (ite $cvcl_1 3 2) x_45) (ite $cvcl_2 x_45 (ite $cvcl_1 1 0))) x_24))) (= x_49 (+ (ite $cvcl_3 (ite $cvcl_6 (ite $cvcl_5 3 2) x_46) (ite $cvcl_6 x_46 (ite $cvcl_5 1 0))) x_24))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_10 $cvcl_11) $cvcl_38) $cvcl_12) $cvcl_13) (= x_23 (ite $cvcl_14 (ite (not (< x_48 3)) 3 x_48) x_24))) (iff x_13 $cvcl_15)) (iff x_15 $cvcl_17)) (iff x_11 $cvcl_19)) $cvcl_51) $cvcl_21) (and (and (and (and (and (and (and (and (and (and $cvcl_10 (not $cvcl_11)) x_30) (= x_7 x_10)) $cvcl_12) $cvcl_13) (= x_23 (ite $cvcl_14 (ite (not (< x_49 3)) 3 x_49) x_24))) (iff x_13 (or $cvcl_15 $cvcl_16 ))) (iff x_15 (or $cvcl_17 $cvcl_18 ))) (iff x_11 (or $cvcl_19 $cvcl_20 ))) $cvcl_21) ) $cvcl_49) $cvcl_50) $cvcl_68) $cvcl_52) $cvcl_53) $cvcl_54) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_42 (or (or (and (and (and (not $cvcl_27) $cvcl_33) $cvcl_32) $cvcl_28) (and (and (and (not $cvcl_29) $cvcl_35) $cvcl_34) $cvcl_30) ) (and (and $cvcl_37 $cvcl_36) $cvcl_31) )) $cvcl_78) (or (or (or (or $cvcl_27 $cvcl_43 ) x_34 ) x_14 ) (not (< x_7 x_42)) )) (or (or (or (or $cvcl_29 $cvcl_44 ) x_36 ) x_16 ) (not (< x_7 x_43)) )) (or (or (or $cvcl_45 x_32 ) x_12 ) (not (< x_7 x_39)) )) (or (or (or (and (and (and (and $cvcl_32 $cvcl_33) $cvcl_28) $cvcl_55) $cvcl_56) (and (and (and (and $cvcl_34 $cvcl_35) $cvcl_30) $cvcl_57) $cvcl_58) ) (and (and (and (and $cvcl_36 $cvcl_37) $cvcl_31) $cvcl_59) $cvcl_60) ) (and (< x_6 ?cvcl_46) $cvcl_61) )) (iff x_33 (or x_34 $cvcl_39 ))) (iff x_35 (or x_36 $cvcl_40 ))) (iff x_31 (or x_32 $cvcl_41 ))) $cvcl_47) $cvcl_48) (and (and (and (and (and (and (and (and (and $cvcl_42 (or (or (or $cvcl_27 x_34 ) x_14 ) $cvcl_43 )) (or (or (or $cvcl_29 x_36 ) x_16 ) $cvcl_44 )) (or (or x_32 x_12 ) $cvcl_45 )) x_37) (= x_7 ?cvcl_46)) $cvcl_47) $cvcl_48) $cvcl_49) $cvcl_50) ) $cvcl_66) $cvcl_67) $cvcl_21) $cvcl_51) $cvcl_52) $cvcl_53) $cvcl_54) ) (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_62 $cvcl_63) $cvcl_79) (or (or (or $cvcl_27 x_20 ) x_14 ) (<= x_7 x_42) )) (or (or (or $cvcl_29 x_22 ) x_16 ) (<= x_7 x_43) )) (or (or x_18 x_12 ) (<= x_7 x_39) )) (or (or (or (and (and (and (and (not x_20) $cvcl_33) (< x_5 x_42)) $cvcl_55) $cvcl_56) (and (and (and (and (not x_22) $cvcl_35) (< x_5 x_43)) $cvcl_57) $cvcl_58) ) (and (and (and (not x_18) $cvcl_37) $cvcl_59) $cvcl_60) ) $cvcl_61 )) (iff x_19 (or x_20 (= x_42 x_7) ))) (iff x_21 (or x_22 (= x_43 x_7) ))) (iff x_17 (or x_18 (= x_39 x_7) ))) $cvcl_64) $cvcl_65) (and (and (and (and (and (and (and $cvcl_62 (not $cvcl_63)) x_8) $cvcl_64) $cvcl_65) (= x_7 x_5)) $cvcl_52) $cvcl_53) ) $cvcl_66) $cvcl_67) $cvcl_21) $cvcl_51) $cvcl_49) $cvcl_50) $cvcl_68) )) (or (or (and $cvcl_69 (= x_9 (ite (not x_3) x_0 1))) (and $cvcl_70 (= x_9 (ite (not x_1) x_0 2))) ) (and (and $cvcl_71 $cvcl_72) (= x_9 x_0)) )) (or (and (and $cvcl_73 (not (<= x_38 x_50))) (not (<= x_50 ?cvcl_74))) (and $cvcl_75 (= x_50 x_42)) )) (or (and (and $cvcl_73 (not (<= x_38 x_51))) (not (<= x_51 ?cvcl_74))) (and $cvcl_75 (= x_51 x_43)) )) (or (and (and $cvcl_73 (= x_38 (+ x_6 x_52))) x_53) (and (and $cvcl_75 (not x_53)) (= x_38 x_6)) )) (or (and (and (and (and $cvcl_76 (not (<= x_54 x_7))) (not (<= x_55 x_7))) (< x_54 x_55)) (< x_55 x_56)) (and (and (and (not $cvcl_76) (= x_54 x_39)) (= x_55 x_44)) (= x_56 x_47)) )) (or (or (and $cvcl_77 (or $cvcl_78 $cvcl_79 )) (and $cvcl_80 (or $cvcl_82 $cvcl_79 )) ) (and $cvcl_81 (or $cvcl_82 $cvcl_78 )) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)
|
