Pastebin launched a little side project called VERYVIRAL.com, check it out ;-) Want more features on Pastebin? Sign Up, it's FREE!
Guest

z3-performance-issue_noinlining

By: a guest on Sep 21st, 2012  |  syntax: None  |  size: 5.63 KB  |  views: 25  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
  1. (set-option :print-success false)
  2. (set-info :smt-lib-version 2.0)
  3. (set-option :AUTO_CONFIG false)
  4. (set-option :MODEL_HIDE_UNUSED_PARTITIONS false)
  5. (set-option :MODEL_V2 true)
  6. (set-option :ASYNC_COMMANDS false)
  7. (set-option :PHASE_SELECTION 0)
  8. (set-option :RESTART_STRATEGY 0)
  9. (set-option :RESTART_FACTOR |1.5|)
  10. (set-option :ARITH_RANDOM_INITIAL_VALUE true)
  11. (set-option :CASE_SPLIT 3)
  12. (set-option :DELAY_UNITS true)
  13. (set-option :DELAY_UNITS_THRESHOLD 16)
  14. (set-option :NNF_SK_HACK true)
  15. (set-option :MBQI false)
  16. (set-option :QI_EAGER_THRESHOLD 100)
  17. (set-option :QI_COST |"(+ weight generation)"|)
  18. (set-option :TYPE_CHECK true)
  19. (set-option :BV_REFLECT true)
  20. ; done setting options
  21.  
  22. ; Boogie universal background predicate
  23. ; Copyright (c) 2004-2010, Microsoft Corp.
  24. (set-info :category "industrial")
  25. (declare-sort |T@U| 0)
  26. (declare-sort |T@T| 0)
  27. (declare-fun int_div (Int Int) Int)
  28. (declare-fun int_mod (Int Int) Int)
  29. (declare-fun UOrdering2 (|T@U| |T@U|) Bool)
  30. (declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)
  31.  
  32. (declare-fun tickleBool (Bool) Bool)
  33. (assert (and (tickleBool true) (tickleBool false)))
  34. (declare-fun Ctor (T@T) Int)
  35. (declare-fun intType () T@T)
  36. (declare-fun boolType () T@T)
  37. (declare-fun int_2_U (Int) T@U)
  38. (declare-fun U_2_int (T@U) Int)
  39. (declare-fun type (T@U) T@T)
  40. (declare-fun bool_2_U (Bool) T@U)
  41. (declare-fun U_2_bool (T@U) Bool)
  42. (declare-fun f (Int) Int)
  43. (declare-fun D () Int)
  44. (declare-fun MapType0Type (T@T T@T) T@T)
  45. (declare-fun MapType0TypeInv0 (T@T) T@T)
  46. (declare-fun MapType0TypeInv1 (T@T) T@T)
  47. (declare-fun MapType0Select (T@U T@U) T@U)
  48. (declare-fun MapType0Store (T@U T@U T@U) T@U)
  49. (declare-fun M () T@U)
  50. (declare-fun %lbl%+92 () Bool)
  51. (declare-fun a () Int)
  52. (declare-fun c () Int)
  53. (declare-fun b () Int)
  54. (declare-fun %lbl%@193 () Bool)
  55. (declare-fun t () Int)
  56. (declare-fun %lbl%+127 () Bool)
  57. (assert (and
  58. (= (Ctor intType) 0)
  59. (= (Ctor boolType) 1)
  60. (forall ((arg0 Int) ) (! (= (U_2_int (int_2_U arg0)) arg0)
  61.  :qid |typeInv:U_2_int|
  62.  :pattern ( (int_2_U arg0))
  63. ))
  64. (forall ((x T@U) ) (! (=> (= (type x) intType) (= (int_2_U (U_2_int x)) x))
  65.  :qid |cast:U_2_int|
  66.  :pattern ( (U_2_int x))
  67. ))
  68. (forall ((arg0@@0 Int) ) (! (= (type (int_2_U arg0@@0)) intType)
  69.  :qid |funType:int_2_U|
  70.  :pattern ( (int_2_U arg0@@0))
  71. ))
  72. (forall ((arg0@@1 Bool) ) (! (= (U_2_bool (bool_2_U arg0@@1)) arg0@@1)
  73.  :qid |typeInv:U_2_bool|
  74.  :pattern ( (bool_2_U arg0@@1))
  75. ))
  76. (forall ((x@@0 T@U) ) (! (=> (= (type x@@0) boolType) (= (bool_2_U (U_2_bool x@@0)) x@@0))
  77.  :qid |cast:U_2_bool|
  78.  :pattern ( (U_2_bool x@@0))
  79. ))
  80. (forall ((arg0@@2 Bool) ) (! (= (type (bool_2_U arg0@@2)) boolType)
  81.  :qid |funType:bool_2_U|
  82.  :pattern ( (bool_2_U arg0@@2))
  83. ))))
  84. (assert (forall ((x@@1 T@U) ) (! (UOrdering2 x@@1 x@@1)
  85.  :qid |bg:subtype-refl|
  86.  :no-pattern (U_2_int x@@1)
  87.  :no-pattern (U_2_bool x@@1)
  88. )))
  89. (assert (forall ((x@@2 T@U) (y T@U) (z T@U) ) (! (let ((alpha (type x@@2)))
  90. (=> (and
  91. (= (type y) alpha)
  92. (= (type z) alpha)
  93. (UOrdering2 x@@2 y)
  94. (UOrdering2 y z)) (UOrdering2 x@@2 z)))
  95.  :qid |bg:subtype-trans|
  96.  :pattern ( (UOrdering2 x@@2 y) (UOrdering2 y z))
  97. )))
  98. (assert (forall ((x@@3 T@U) (y@@0 T@U) ) (! (let ((alpha@@0 (type x@@3)))
  99. (=> (= (type y@@0) alpha@@0) (=> (and
  100. (UOrdering2 x@@3 y@@0)
  101. (UOrdering2 y@@0 x@@3)) (= x@@3 y@@0))))
  102.  :qid |bg:subtype-antisymm|
  103.  :pattern ( (UOrdering2 x@@3 y@@0) (UOrdering2 y@@0 x@@3))
  104. )))
  105. (assert (forall ((n Int) ) (! (= (f n) (* n D))
  106.  :qid |multipli.3:16|
  107.  :skolemid |0|
  108.  :pattern ( (f n))
  109. )))
  110. (assert (and
  111. (forall ((arg0@@3 T@T) (arg1 T@T) ) (! (= (Ctor (MapType0Type arg0@@3 arg1)) 2)
  112.  :qid |ctor:MapType0Type|
  113. ))
  114. (forall ((arg0@@4 T@T) (arg1@@0 T@T) ) (! (= (MapType0TypeInv0 (MapType0Type arg0@@4 arg1@@0)) arg0@@4)
  115.  :qid |typeInv:MapType0TypeInv0|
  116.  :pattern ( (MapType0Type arg0@@4 arg1@@0))
  117. ))
  118. (forall ((arg0@@5 T@T) (arg1@@1 T@T) ) (! (= (MapType0TypeInv1 (MapType0Type arg0@@5 arg1@@1)) arg1@@1)
  119.  :qid |typeInv:MapType0TypeInv1|
  120.  :pattern ( (MapType0Type arg0@@5 arg1@@1))
  121. ))
  122. (forall ((arg0@@6 T@U) (arg1@@2 T@U) ) (! (let ((aVar1 (MapType0TypeInv1 (type arg0@@6))))
  123. (= (type (MapType0Select arg0@@6 arg1@@2)) aVar1))
  124.  :qid |funType:MapType0Select|
  125.  :pattern ( (MapType0Select arg0@@6 arg1@@2))
  126. ))
  127. (forall ((arg0@@7 T@U) (arg1@@3 T@U) (arg2 T@U) ) (! (let ((aVar1@@0 (type arg2)))
  128. (let ((aVar0 (type arg1@@3)))
  129. (= (type (MapType0Store arg0@@7 arg1@@3 arg2)) (MapType0Type aVar0 aVar1@@0))))
  130.  :qid |funType:MapType0Store|
  131.  :pattern ( (MapType0Store arg0@@7 arg1@@3 arg2))
  132. ))
  133. (forall ((m T@U) (x0 T@U) (val T@U) ) (! (let ((aVar1@@1 (MapType0TypeInv1 (type m))))
  134. (=> (= (type val) aVar1@@1) (= (MapType0Select (MapType0Store m x0 val) x0) val)))
  135.  :qid |mapAx0:MapType0Select|
  136.  :weight 0
  137. ))
  138. (forall ((val@@0 T@U) (m@@0 T@U) (x0@@0 T@U) (y0 T@U) ) (! (or
  139. (= x0@@0 y0)
  140. (= (MapType0Select (MapType0Store m@@0 x0@@0 val@@0) y0) (MapType0Select m@@0 y0)))
  141.  :qid |mapAx1:MapType0Select:0|
  142.  :weight 0
  143. ))
  144. (forall ((val@@1 T@U) (m@@1 T@U) (x0@@1 T@U) (y0@@0 T@U) ) (! (or
  145. true
  146. (= (MapType0Select (MapType0Store m@@1 x0@@1 val@@1) y0@@0) (MapType0Select m@@1 y0@@0)))
  147.  :qid |mapAx2:MapType0Select|
  148.  :weight 0
  149. ))
  150. (= (type M) (MapType0Type intType intType))))
  151. (push 1)
  152. (set-info :boogie-vc-id test)
  153. (assert (not
  154. (let ((anon0_correct (=> (! (and %lbl%+92 true) :lblpos +92) (=> (and
  155. (< 0 a)
  156. (< (* 1000 a) (f 1))) (=> (and
  157. (< 0 c)
  158. (< (* 1000 c) (f 1))
  159. (= (* (f 100) b) (* a c))) (and
  160. (! (or %lbl%@193 (> (U_2_int (MapType0Select M (int_2_U t))) 0)) :lblneg @193)
  161. (=> (> (U_2_int (MapType0Select M (int_2_U t))) 0) true)))))))
  162. (let ((PreconditionGeneratedEntry_correct (=> (! (and %lbl%+127 true) :lblpos +127) anon0_correct)))
  163. PreconditionGeneratedEntry_correct))
  164. ))
  165. (check-sat)