source: vis_dev/cusp-1.1/examples/inf-bakery-mutex-1/inf-bakery-mutex-1.smt @ 18

Last change on this file since 18 was 12, checked in by cecile, 13 years ago

cusp added
  • Property svn:executable set to *
File size: 6.0 KB
Line 
1( benchmark inf_bakery_mutex_1.smt
2:source {
3SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
4Sorea, and Leonardo de Moura.  Contact demoura@csl.sri.com for more
5information.
6
7This 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.