Last change
on this file was
12,
checked in by cecile, 13 years ago
|
cusp added
|
-
Property svn:executable set to
*
|
File size:
6.0 KB
|
Rev | Line | |
---|
[12] | 1 | ( benchmark inf_bakery_mutex_1.smt |
---|
| 2 | :source { |
---|
| 3 | SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria |
---|
| 4 | Sorea, and Leonardo de Moura. Contact demoura@csl.sri.com for more |
---|
| 5 | information. |
---|
| 6 | |
---|
| 7 | This benchmark was automatically translated into SMT-LIB format by Albert Oliveras. |
---|
| 8 | } |
---|
| 9 | :status unsat |
---|
| 10 | :category { industrial } |
---|
| 11 | :difficulty { 0 } |
---|
| 12 | :logic QF_IDL |
---|
| 13 | :extrafuns ((x_2 Int )) |
---|
| 14 | :extrafuns ((uclid_ZERO Int )) |
---|
| 15 | :extrafuns ((x_14 Int )) |
---|
| 16 | :extrafuns ((x_5 Int )) |
---|
| 17 | :extrafuns ((x_6 Int )) |
---|
| 18 | :extrafuns ((x_7 Int )) |
---|
| 19 | :extrafuns ((x_8 Int )) |
---|
| 20 | :extrafuns ((x_9 Int )) |
---|
| 21 | :extrapreds ((x_0)) |
---|
| 22 | :extrapreds ((x_1)) |
---|
| 23 | :extrapreds ((x_3)) |
---|
| 24 | :extrapreds ((x_10)) |
---|
| 25 | :extrapreds ((x_11)) |
---|
| 26 | :extrapreds ((x_12)) |
---|
| 27 | :extrapreds ((x_13)) |
---|
| 28 | :extrapreds ((x_4)) |
---|
| 29 | :formula |
---|
| 30 | ( let ( ?t10 x_2 ) ( let ( ?t11 uclid_ZERO ) ( flet ( $t12 ( < x_2 uclid_ZERO ) ) ( flet ( $t13 ( not $t12 ) ) ( let ( ?t14 x_5 ) ( flet ( $t15 ( < x_5 uclid_ZERO ) ) ( flet ( $t16 ( not $t15 ) ) ( flet ( $t17 ( and $t13 $t16 ) ) ( let ( ?t18 x_6 ) ( flet ( $t19 ( < x_6 uclid_ZERO ) ) ( flet ( $t20 ( not $t19 ) ) ( flet ( $t21 ( and $t17 $t20 ) ) ( let ( ?t22 x_7 ) ( flet ( $t23 ( < x_7 uclid_ZERO ) ) ( flet ( $t24 ( not $t23 ) ) ( flet ( $t25 ( and $t21 $t24 ) ) ( flet ( $t26 x_0 ) ( flet ( $t27 ( not $t26 ) ) ( flet ( $t28 x_1 ) ( flet ( $t29 ( not $t28 ) ) ( flet ( $t30 ( and $t27 $t29 ) ) ( flet ( $t31 ( and $t25 $t30 ) ) ( flet ( $t32 ( = x_2 uclid_ZERO ) ) ( flet ( $t33 ( and $t31 $t32 ) ) ( flet ( $t34 x_3 ) ( flet ( $t35 ( not $t34 ) ) ( flet ( $t36 x_4 ) ( flet ( $t37 ( not $t36 ) ) ( flet ( $t38 ( and $t35 $t37 ) ) ( flet ( $t39 ( and $t33 $t38 ) ) ( flet ( $t40 ( = x_5 uclid_ZERO ) ) ( flet ( $t41 ( and $t39 $t40 ) ) ( let ( ?t42 x_8 ) ( flet ( $t43 ( = x_8 uclid_ZERO ) ) ( let ( ?t44 x_9 ) ( flet ( $t45 ( = x_9 uclid_ZERO ) ) ( flet ( $t46 ( and $t45 $t27 ) ) ( flet ( $t47 ( and $t46 $t29 ) ) ( flet ( $t49 ( = ( - x_7 x_5 ) 1 ) ) ( flet ( $t50 ( and $t47 $t49 ) ) ( flet ( $t51 x_10 ) ( flet ( $t52 ( and $t50 $t51 ) ) ( flet ( $t53 x_11 ) ( flet ( $t54 ( not $t53 ) ) ( flet ( $t55 ( and $t52 $t54 ) ) ( flet ( $t57 ( = ( - x_9 uclid_ZERO ) 1 ) ) ( flet ( $t58 ( and $t57 $t26 ) ) ( flet ( $t59 ( and $t58 $t29 ) ) ( flet ( $t60 ( < x_2 x_5 ) ) ( flet ( $t61 ( or $t40 $t60 ) ) ( flet ( $t62 ( and $t59 $t61 ) ) ( flet ( $t63 ( not $t51 ) ) ( flet ( $t64 ( and $t62 $t63 ) ) ( flet ( $t65 ( and $t64 $t53 ) ) ( flet ( $t66 ( = x_7 x_2 ) ) ( flet ( $t67 ( and $t65 $t66 ) ) ( flet ( $t68 ( or $t55 $t67 ) ) ( flet ( $t70 ( = ( - x_9 uclid_ZERO ) 2 ) ) ( flet ( $t71 ( and $t70 $t27 ) ) ( flet ( $t72 ( and $t71 $t28 ) ) ( flet ( $t73 ( = x_7 uclid_ZERO ) ) ( flet ( $t74 ( and $t72 $t73 ) ) ( flet ( $t75 ( and $t74 $t63 ) ) ( flet ( $t76 ( and $t75 $t54 ) ) ( flet ( $t77 ( or $t68 $t76 ) ) ( flet ( $t78 ( and $t43 $t77 ) ) ( flet ( $t79 x_12 ) ( flet ( $t80 ( not $t79 ) ) ( flet ( $t81 ( or $t80 $t34 ) ) ( flet ( $t82 ( or $t35 $t79 ) ) ( flet ( $t83 ( and $t81 $t82 ) ) ( flet ( $t84 ( and $t78 $t83 ) ) ( flet ( $t85 x_13 ) ( flet ( $t86 ( not $t85 ) ) ( flet ( $t87 ( or $t86 $t36 ) ) ( flet ( $t88 ( or $t37 $t85 ) ) ( flet ( $t89 ( and $t87 $t88 ) ) ( flet ( $t90 ( and $t84 $t89 ) ) ( flet ( $t91 ( = x_6 x_5 ) ) ( flet ( $t92 ( and $t90 $t91 ) ) ( flet ( $t93 ( = ( - x_8 uclid_ZERO ) 1 ) ) ( let ( ?t94 x_14 ) ( flet ( $t95 ( = x_14 uclid_ZERO ) ) ( flet ( $t96 ( and $t95 $t35 ) ) ( flet ( $t97 ( and $t96 $t37 ) ) ( flet ( $t99 ( = ( - x_6 x_2 ) 1 ) ) ( flet ( $t100 ( and $t97 $t99 ) ) ( flet ( $t101 ( and $t100 $t79 ) ) ( flet ( $t102 ( and $t101 $t86 ) ) ( flet ( $t103 ( = ( - x_14 uclid_ZERO ) 1 ) ) ( flet ( $t104 ( and $t103 $t34 ) ) ( flet ( $t105 ( and $t104 $t37 ) ) ( flet ( $t106 ( < x_5 x_2 ) ) ( flet ( $t107 ( or $t32 $t106 ) ) ( flet ( $t108 ( and $t105 $t107 ) ) ( flet ( $t109 ( and $t108 $t80 ) ) ( flet ( $t110 ( and $t109 $t85 ) ) ( flet ( $t111 ( and $t110 $t91 ) ) ( flet ( $t112 ( or $t102 $t111 ) ) ( flet ( $t113 ( = ( - x_14 uclid_ZERO ) 2 ) ) ( flet ( $t114 ( and $t113 $t35 ) ) ( flet ( $t115 ( and $t114 $t36 ) ) ( flet ( $t116 ( = x_6 uclid_ZERO ) ) ( flet ( $t117 ( and $t115 $t116 ) ) ( flet ( $t118 ( and $t117 $t80 ) ) ( flet ( $t119 ( and $t118 $t86 ) ) ( flet ( $t120 ( or $t112 $t119 ) ) ( flet ( $t121 ( and $t93 $t120 ) ) ( flet ( $t122 ( or $t63 $t26 ) ) ( flet ( $t123 ( or $t27 $t51 ) ) ( flet ( $t124 ( and $t122 $t123 ) ) ( flet ( $t125 ( and $t121 $t124 ) ) ( flet ( $t126 ( or $t54 $t28 ) ) ( flet ( $t127 ( or $t29 $t53 ) ) ( flet ( $t128 ( and $t126 $t127 ) ) ( flet ( $t129 ( and $t125 $t128 ) ) ( flet ( $t130 ( and $t129 $t66 ) ) ( flet ( $t131 ( or $t92 $t130 ) ) ( flet ( $t132 ( and $t41 $t131 ) ) ( flet ( $t133 ( and $t63 $t53 ) ) ( flet ( $t134 ( and $t133 $t80 ) ) ( flet ( $t135 ( and $t134 $t85 ) ) ( flet ( $t136 ( and $t27 $t28 ) ) ( flet ( $t137 ( and $t136 $t35 ) ) ( flet ( $t138 ( and $t137 $t36 ) ) ( flet ( $t139 ( or $t135 $t138 ) ) ( flet ( $t140 ( and $t132 $t139 ) ) ( flet ( $t141 ( or $t29 $t27 ) ) ( flet ( $t142 ( and $t140 $t141 ) ) ( flet ( $t143 ( or $t37 $t35 ) ) ( flet ( $t144 ( and $t142 $t143 ) ) ( flet ( $t145 ( or $t54 $t63 ) ) ( flet ( $t146 ( and $t144 $t145 ) ) ( flet ( $t147 ( or $t86 $t80 ) ) ( flet ( $t148 ( and $t146 $t147 ) ) ( flet ( $t149 ( not $t148 ) ) ( not $t149 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |
---|
Note: See
TracBrowser
for help on using the repository browser.