API tools faq
paste
Advertisement
Guest User

Invalid (SAT) VC in SMT2 language

a guest
Nov 12th, 2013
214
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Scheme 23.85 KB | None | 0 0
raw download clone embed print report
  1. (declare-sort T12)
  2. (declare-const v_15 T12)
  3. (declare-const x_0 T12)
  4. (declare-const t T12)
  5. (declare-const anc_1047I T12)
  6. (declare-sort T14)
  7. (declare-const z T14)
  8. (declare-const d T12)
  9. (declare-const a T12)
  10. (declare-const x T14)
  11. (declare-const anc_1045I T12)
  12. (declare-const b T12)
  13. (declare-const y T14)
  14. (declare-const c T12)
  15. (declare-const anc_1056I T12)
  16. (declare-const anc_1063I T12)
  17. (declare-fun Rmem1 (T12 T14) Bool)
  18. (declare-fun Rtos0 (T12 T14 T14) Bool)
  19. (assert (= t x_0))
  20. (declare-fun set480 (T14) Bool)
  21. (assert (forall ((bv0 T14))
  22.   (! (= (set480 bv0) (= bv0 z)) :pattern ((set480 bv0)))))
  23. (declare-fun set481 (T14 T14) Bool)
  24. (assert (forall ((bv1 T14) (bv0 T14))
  25.   (! (= (set481 bv0 bv1) (and (Rmem1 anc_1047I bv0) (set480 bv1)))
  26.      :pattern ((set481 bv0 bv1))
  27.      :pattern ((Rmem1 anc_1047I bv0) (set480 bv1)))))
  28. (declare-fun set482 (T14) Bool)
  29. (assert (forall ((bv0 T14))
  30.   (! (= (set482 bv0) (= bv0 z)) :pattern ((set482 bv0)))))
  31. (declare-fun set483 (T14 T14) Bool)
  32. (assert (forall ((bv1 T14) (bv0 T14))
  33.   (! (= (set483 bv0 bv1) (and (set482 bv0) (Rmem1 d bv1)))
  34.      :pattern ((set483 bv0 bv1))
  35.      :pattern ((set482 bv0) (Rmem1 d bv1)))))
  36. (declare-fun set484 (T14 T14) Bool)
  37. (assert (forall ((bv1 T14) (bv0 T14))
  38.   (! (= (set484 bv0 bv1) (and (Rmem1 anc_1047I bv0) (Rmem1 d bv1)))
  39.      :pattern ((set484 bv0 bv1))
  40.      :pattern ((Rmem1 anc_1047I bv0) (Rmem1 d bv1)))))
  41. (declare-fun set485 (T14 T14) Bool)
  42. (assert (forall ((bv1 T14) (bv0 T14))
  43.   (! (= (set485 bv0 bv1) (or (set483 bv0 bv1) (set484 bv0 bv1)))
  44.      :pattern ((set485 bv0 bv1))
  45.      :pattern ((set483 bv0 bv1))
  46.      :pattern ((set484 bv0 bv1)))))
  47. (declare-fun set486 (T14 T14) Bool)
  48. (assert (forall ((bv1 T14) (bv0 T14))
  49.   (! (= (set486 bv0 bv1) (or (set481 bv0 bv1) (set485 bv0 bv1)))
  50.      :pattern ((set486 bv0 bv1))
  51.      :pattern ((set481 bv0 bv1))
  52.      :pattern ((set485 bv0 bv1)))))
  53. (declare-fun set487 (T14 T14) Bool)
  54. (assert (forall ((bv1 T14) (bv0 T14))
  55.   (! (= (set487 bv0 bv1) (or (Rtos0 d bv0 bv1) (Rtos0 anc_1047I bv0 bv1)))
  56.      :pattern ((set487 bv0 bv1))
  57.      :pattern ((Rtos0 d bv0 bv1))
  58.      :pattern ((Rtos0 anc_1047I bv0 bv1)))))
  59. (declare-fun set488 (T14 T14) Bool)
  60. (assert (forall ((bv1 T14) (bv0 T14))
  61.   (! (= (set488 bv0 bv1) (or (set486 bv0 bv1) (set487 bv0 bv1)))
  62.      :pattern ((set488 bv0 bv1))
  63.      :pattern ((set486 bv0 bv1))
  64.      :pattern ((set487 bv0 bv1)))))
  65. (assert (forall ((bv1 T14) (bv0 T14))
  66.   (! (= (Rtos0 t bv0 bv1) (set488 bv0 bv1))
  67.      :pattern ((Rtos0 t bv0 bv1))
  68.      :pattern ((set488 bv0 bv1)))))
  69. (declare-fun set489 (T14) Bool)
  70. (assert (forall ((bv0 T14))
  71.   (! (= (set489 bv0) (= bv0 z)) :pattern ((set489 bv0)))))
  72. (declare-fun set490 (T14 T14) Bool)
  73. (assert (forall ((bv1 T14) (bv0 T14))
  74.   (! (= (set490 bv0 bv1) (and (Rmem1 anc_1047I bv0) (set489 bv1)))
  75.      :pattern ((set490 bv0 bv1))
  76.      :pattern ((Rmem1 anc_1047I bv0) (set489 bv1)))))
  77. (declare-fun set491 (T14) Bool)
  78. (assert (forall ((bv0 T14))
  79.   (! (= (set491 bv0) (= bv0 z)) :pattern ((set491 bv0)))))
  80. (declare-fun set492 (T14 T14) Bool)
  81. (assert (forall ((bv1 T14) (bv0 T14))
  82.   (! (= (set492 bv0 bv1) (and (set491 bv0) (Rmem1 d bv1)))
  83.      :pattern ((set492 bv0 bv1))
  84.      :pattern ((set491 bv0) (Rmem1 d bv1)))))
  85. (declare-fun set493 (T14 T14) Bool)
  86. (assert (forall ((bv1 T14) (bv0 T14))
  87.   (! (= (set493 bv0 bv1) (and (Rmem1 anc_1047I bv0) (Rmem1 d bv1)))
  88.      :pattern ((set493 bv0 bv1))
  89.      :pattern ((Rmem1 anc_1047I bv0) (Rmem1 d bv1)))))
  90. (declare-fun set494 (T14 T14) Bool)
  91. (assert (forall ((bv1 T14) (bv0 T14))
  92.   (! (= (set494 bv0 bv1) (or (set492 bv0 bv1) (set493 bv0 bv1)))
  93.      :pattern ((set494 bv0 bv1))
  94.      :pattern ((set492 bv0 bv1))
  95.      :pattern ((set493 bv0 bv1)))))
  96. (declare-fun set496 (T14) Bool)
  97. (assert (forall ((bv0 T14))
  98.   (! (= (set496 bv0) (= bv0 z)) :pattern ((set496 bv0)))))
  99. (declare-fun set497 (T14) Bool)
  100. (assert (forall ((bv0 T14))
  101.   (! (= (set497 bv0) (or (Rmem1 d bv0) (Rmem1 anc_1047I bv0)))
  102.      :pattern ((set497 bv0))
  103.      :pattern ((Rmem1 d bv0))
  104.      :pattern ((Rmem1 anc_1047I bv0)))))
  105. (declare-fun set498 (T14) Bool)
  106. (assert (forall ((bv0 T14))
  107.   (! (= (set498 bv0) (or (set496 bv0) (set497 bv0)))
  108.      :pattern ((set498 bv0))
  109.      :pattern ((set496 bv0))
  110.      :pattern ((set497 bv0)))))
  111. (assert (forall ((bv0 T14))
  112.   (! (= (Rmem1 t bv0) (set498 bv0))
  113.      :pattern ((Rmem1 t bv0))
  114.      :pattern ((set498 bv0)))))
  115. (declare-fun set500 (T14) Bool)
  116. (assert (forall ((bv0 T14))
  117.   (! (= (set500 bv0) (= bv0 z)) :pattern ((set500 bv0)))))
  118. (declare-fun set501 (T14 T14) Bool)
  119. (assert (forall ((bv1 T14) (bv0 T14))
  120.   (! (= (set501 bv0 bv1) (and (Rmem1 b bv0) (set500 bv1)))
  121.      :pattern ((set501 bv0 bv1))
  122.      :pattern ((Rmem1 b bv0) (set500 bv1)))))
  123. (declare-fun set502 (T14) Bool)
  124. (assert (forall ((bv0 T14))
  125.   (! (= (set502 bv0) (= bv0 z)) :pattern ((set502 bv0)))))
  126. (declare-fun set503 (T14 T14) Bool)
  127. (assert (forall ((bv1 T14) (bv0 T14))
  128.   (! (= (set503 bv0 bv1) (and (set502 bv0) (Rmem1 d bv1)))
  129.      :pattern ((set503 bv0 bv1))
  130.      :pattern ((set502 bv0) (Rmem1 d bv1)))))
  131. (declare-fun set504 (T14 T14) Bool)
  132. (assert (forall ((bv1 T14) (bv0 T14))
  133.   (! (= (set504 bv0 bv1) (and (Rmem1 b bv0) (Rmem1 d bv1)))
  134.      :pattern ((set504 bv0 bv1))
  135.      :pattern ((Rmem1 b bv0) (Rmem1 d bv1)))))
  136. (declare-fun set505 (T14 T14) Bool)
  137. (assert (forall ((bv1 T14) (bv0 T14))
  138.   (! (= (set505 bv0 bv1) (or (set503 bv0 bv1) (set504 bv0 bv1)))
  139.      :pattern ((set505 bv0 bv1))
  140.      :pattern ((set503 bv0 bv1))
  141.      :pattern ((set504 bv0 bv1)))))
  142. (declare-fun set506 (T14 T14) Bool)
  143. (assert (forall ((bv1 T14) (bv0 T14))
  144.   (! (= (set506 bv0 bv1) (or (set501 bv0 bv1) (set505 bv0 bv1)))
  145.      :pattern ((set506 bv0 bv1))
  146.      :pattern ((set501 bv0 bv1))
  147.      :pattern ((set505 bv0 bv1)))))
  148. (declare-fun set507 (T14 T14) Bool)
  149. (assert (forall ((bv1 T14) (bv0 T14))
  150.   (! (= (set507 bv0 bv1)
  151.         (or (Rtos0 d bv0 bv1) (Rtos0 b bv0 bv1)))
  152.      :pattern ((set507 bv0 bv1))
  153.      :pattern ((Rtos0 d bv0 bv1))
  154.      :pattern ((Rtos0 b bv0 bv1)))))
  155. (declare-fun set508 (T14 T14) Bool)
  156. (assert (forall ((bv1 T14) (bv0 T14))
  157.   (! (= (set508 bv0 bv1) (or (set506 bv0 bv1) (set507 bv0 bv1)))
  158.      :pattern ((set508 bv0 bv1))
  159.      :pattern ((set506 bv0 bv1))
  160.      :pattern ((set507 bv0 bv1)))))
  161. (assert (forall ((bv1 T14) (bv0 T14))
  162.   (! (= (Rtos0 anc_1063I bv0 bv1) (set508 bv0 bv1))
  163.      :pattern ((Rtos0 anc_1063I bv0 bv1))
  164.      :pattern ((set508 bv0 bv1)))))
  165. (declare-fun set509 (T14) Bool)
  166. (assert (forall ((bv0 T14))
  167.   (! (= (set509 bv0) (= bv0 z)) :pattern ((set509 bv0)))))
  168. (declare-fun set510 (T14 T14) Bool)
  169. (assert (forall ((bv1 T14) (bv0 T14))
  170.   (! (= (set510 bv0 bv1) (and (Rmem1 b bv0) (set509 bv1)))
  171.      :pattern ((set510 bv0 bv1))
  172.      :pattern ((Rmem1 b bv0) (set509 bv1)))))
  173. (declare-fun set511 (T14) Bool)
  174. (assert (forall ((bv0 T14))
  175.   (! (= (set511 bv0) (= bv0 z)) :pattern ((set511 bv0)))))
  176. (declare-fun set512 (T14 T14) Bool)
  177. (assert (forall ((bv1 T14) (bv0 T14))
  178.   (! (= (set512 bv0 bv1) (and (set511 bv0) (Rmem1 d bv1)))
  179.      :pattern ((set512 bv0 bv1))
  180.      :pattern ((set511 bv0) (Rmem1 d bv1)))))
  181. (declare-fun set513 (T14 T14) Bool)
  182. (assert (forall ((bv1 T14) (bv0 T14))
  183.   (! (= (set513 bv0 bv1) (and (Rmem1 b bv0) (Rmem1 d bv1)))
  184.      :pattern ((set513 bv0 bv1))
  185.      :pattern ((Rmem1 b bv0) (Rmem1 d bv1)))))
  186. (declare-fun set514 (T14 T14) Bool)
  187. (assert (forall ((bv1 T14) (bv0 T14))
  188.   (! (= (set514 bv0 bv1) (or (set512 bv0 bv1) (set513 bv0 bv1)))
  189.      :pattern ((set514 bv0 bv1))
  190.      :pattern ((set512 bv0 bv1))
  191.      :pattern ((set513 bv0 bv1)))))
  192. (declare-fun set516 (T14) Bool)
  193. (assert (forall ((bv0 T14))
  194.   (! (= (set516 bv0) (= bv0 z)) :pattern ((set516 bv0)))))
  195. (declare-fun set517 (T14) Bool)
  196. (assert (forall ((bv0 T14))
  197.   (! (= (set517 bv0) (or (Rmem1 d bv0) (Rmem1 b bv0)))
  198.      :pattern ((set517 bv0))
  199.      :pattern ((Rmem1 d bv0))
  200.      :pattern ((Rmem1 b bv0)))))
  201. (declare-fun set518 (T14) Bool)
  202. (assert (forall ((bv0 T14))
  203.   (! (= (set518 bv0) (or (set516 bv0) (set517 bv0)))
  204.      :pattern ((set518 bv0))
  205.      :pattern ((set516 bv0))
  206.      :pattern ((set517 bv0)))))
  207. (assert (forall ((bv0 T14))
  208.   (! (= (Rmem1 anc_1063I bv0) (set518 bv0))
  209.      :pattern ((Rmem1 anc_1063I bv0))
  210.      :pattern ((set518 bv0)))))
  211. (declare-fun set520 (T14) Bool)
  212. (assert (forall ((bv0 T14))
  213.   (! (= (set520 bv0) (= bv0 x)) :pattern ((set520 bv0)))))
  214. (declare-fun set521 (T14 T14) Bool)
  215. (assert (forall ((bv1 T14) (bv0 T14))
  216.   (! (= (set521 bv0 bv1) (and (Rmem1 a bv0) (set520 bv1)))
  217.      :pattern ((set521 bv0 bv1))
  218.      :pattern ((Rmem1 a bv0) (set520 bv1)))))
  219. (declare-fun set522 (T14) Bool)
  220. (assert (forall ((bv0 T14))
  221.   (! (= (set522 bv0) (= bv0 x)) :pattern ((set522 bv0)))))
  222. (declare-fun set523 (T14 T14) Bool)
  223. (assert (forall ((bv1 T14) (bv0 T14))
  224.   (! (= (set523 bv0 bv1) (and (set522 bv0) (Rmem1 c bv1)))
  225.      :pattern ((set523 bv0 bv1))
  226.      :pattern ((set522 bv0) (Rmem1 c bv1)))))
  227. (declare-fun set524 (T14 T14) Bool)
  228. (assert (forall ((bv1 T14) (bv0 T14))
  229.   (! (= (set524 bv0 bv1) (and (Rmem1 a bv0) (Rmem1 c bv1)))
  230.      :pattern ((set524 bv0 bv1))
  231.      :pattern ((Rmem1 a bv0) (Rmem1 c bv1)))))
  232. (declare-fun set525 (T14 T14) Bool)
  233. (assert (forall ((bv1 T14) (bv0 T14))
  234.   (! (= (set525 bv0 bv1) (or (set523 bv0 bv1) (set524 bv0 bv1)))
  235.      :pattern ((set525 bv0 bv1))
  236.      :pattern ((set523 bv0 bv1))
  237.      :pattern ((set524 bv0 bv1)))))
  238. (declare-fun set526 (T14 T14) Bool)
  239. (assert (forall ((bv1 T14) (bv0 T14))
  240.   (! (= (set526 bv0 bv1) (or (set521 bv0 bv1) (set525 bv0 bv1)))
  241.      :pattern ((set526 bv0 bv1))
  242.      :pattern ((set521 bv0 bv1))
  243.      :pattern ((set525 bv0 bv1)))))
  244. (declare-fun set527 (T14 T14) Bool)
  245. (assert (forall ((bv1 T14) (bv0 T14))
  246.   (! (= (set527 bv0 bv1)
  247.         (or (Rtos0 c bv0 bv1) (Rtos0 a bv0 bv1)))
  248.      :pattern ((set527 bv0 bv1))
  249.      :pattern ((Rtos0 c bv0 bv1))
  250.      :pattern ((Rtos0 a bv0 bv1)))))
  251. (declare-fun set528 (T14 T14) Bool)
  252. (assert (forall ((bv1 T14) (bv0 T14))
  253.   (! (= (set528 bv0 bv1) (or (set526 bv0 bv1) (set527 bv0 bv1)))
  254.      :pattern ((set528 bv0 bv1))
  255.      :pattern ((set526 bv0 bv1))
  256.      :pattern ((set527 bv0 bv1)))))
  257. (assert (forall ((bv1 T14) (bv0 T14))
  258.   (! (= (Rtos0 anc_1056I bv0 bv1) (set528 bv0 bv1))
  259.      :pattern ((Rtos0 anc_1056I bv0 bv1))
  260.      :pattern ((set528 bv0 bv1)))))
  261. (declare-fun set529 (T14) Bool)
  262. (assert (forall ((bv0 T14))
  263.   (! (= (set529 bv0) (= bv0 x)) :pattern ((set529 bv0)))))
  264. (declare-fun set530 (T14 T14) Bool)
  265. (assert (forall ((bv1 T14) (bv0 T14))
  266.   (! (= (set530 bv0 bv1) (and (Rmem1 a bv0) (set529 bv1)))
  267.      :pattern ((set530 bv0 bv1))
  268.      :pattern ((Rmem1 a bv0) (set529 bv1)))))
  269. (declare-fun set531 (T14) Bool)
  270. (assert (forall ((bv0 T14))
  271.   (! (= (set531 bv0) (= bv0 x)) :pattern ((set531 bv0)))))
  272. (declare-fun set532 (T14 T14) Bool)
  273. (assert (forall ((bv1 T14) (bv0 T14))
  274.   (! (= (set532 bv0 bv1) (and (set531 bv0) (Rmem1 c bv1)))
  275.      :pattern ((set532 bv0 bv1))
  276.      :pattern ((set531 bv0) (Rmem1 c bv1)))))
  277. (declare-fun set533 (T14 T14) Bool)
  278. (assert (forall ((bv1 T14) (bv0 T14))
  279.   (! (= (set533 bv0 bv1) (and (Rmem1 a bv0) (Rmem1 c bv1)))
  280.      :pattern ((set533 bv0 bv1))
  281.      :pattern ((Rmem1 a bv0) (Rmem1 c bv1)))))
  282. (declare-fun set534 (T14 T14) Bool)
  283. (assert (forall ((bv1 T14) (bv0 T14))
  284.   (! (= (set534 bv0 bv1) (or (set532 bv0 bv1) (set533 bv0 bv1)))
  285.      :pattern ((set534 bv0 bv1))
  286.      :pattern ((set532 bv0 bv1))
  287.      :pattern ((set533 bv0 bv1)))))
  288. (declare-fun set536 (T14) Bool)
  289. (assert (forall ((bv0 T14))
  290.   (! (= (set536 bv0) (= bv0 x)) :pattern ((set536 bv0)))))
  291. (declare-fun set537 (T14) Bool)
  292. (assert (forall ((bv0 T14))
  293.   (! (= (set537 bv0) (or (Rmem1 c bv0) (Rmem1 a bv0)))
  294.      :pattern ((set537 bv0))
  295.      :pattern ((Rmem1 c bv0))
  296.      :pattern ((Rmem1 a bv0)))))
  297. (declare-fun set538 (T14) Bool)
  298. (assert (forall ((bv0 T14))
  299.   (! (= (set538 bv0) (or (set536 bv0) (set537 bv0)))
  300.      :pattern ((set538 bv0))
  301.      :pattern ((set536 bv0))
  302.      :pattern ((set537 bv0)))))
  303. (assert (forall ((bv0 T14))
  304.   (! (= (Rmem1 anc_1056I bv0) (set538 bv0))
  305.      :pattern ((Rmem1 anc_1056I bv0))
  306.      :pattern ((set538 bv0)))))
  307. (declare-fun set540 (T14) Bool)
  308. (assert (forall ((bv0 T14))
  309.   (! (= (set540 bv0) (= bv0 y)) :pattern ((set540 bv0)))))
  310. (declare-fun set541 (T14 T14) Bool)
  311. (assert (forall ((bv1 T14) (bv0 T14))
  312.   (! (= (set541 bv0 bv1) (and (Rmem1 b bv0) (set540 bv1)))
  313.      :pattern ((set541 bv0 bv1))
  314.      :pattern ((Rmem1 b bv0) (set540 bv1)))))
  315. (declare-fun set542 (T14) Bool)
  316. (assert (forall ((bv0 T14))
  317.   (! (= (set542 bv0) (= bv0 y)) :pattern ((set542 bv0)))))
  318. (declare-fun set543 (T14 T14) Bool)
  319. (assert (forall ((bv1 T14) (bv0 T14))
  320.   (! (= (set543 bv0 bv1) (and (set542 bv0) (Rmem1 c bv1)))
  321.      :pattern ((set543 bv0 bv1))
  322.      :pattern ((set542 bv0) (Rmem1 c bv1)))))
  323. (declare-fun set544 (T14 T14) Bool)
  324. (assert (forall ((bv1 T14) (bv0 T14))
  325.   (! (= (set544 bv0 bv1) (and (Rmem1 b bv0) (Rmem1 c bv1)))
  326.      :pattern ((set544 bv0 bv1))
  327.      :pattern ((Rmem1 b bv0) (Rmem1 c bv1)))))
  328. (declare-fun set545 (T14 T14) Bool)
  329. (assert (forall ((bv1 T14) (bv0 T14))
  330.   (! (= (set545 bv0 bv1) (or (set543 bv0 bv1) (set544 bv0 bv1)))
  331.      :pattern ((set545 bv0 bv1))
  332.      :pattern ((set543 bv0 bv1))
  333.      :pattern ((set544 bv0 bv1)))))
  334. (declare-fun set546 (T14 T14) Bool)
  335. (assert (forall ((bv1 T14) (bv0 T14))
  336.   (! (= (set546 bv0 bv1) (or (set541 bv0 bv1) (set545 bv0 bv1)))
  337.      :pattern ((set546 bv0 bv1))
  338.      :pattern ((set541 bv0 bv1))
  339.      :pattern ((set545 bv0 bv1)))))
  340. (declare-fun set547 (T14 T14) Bool)
  341. (assert (forall ((bv1 T14) (bv0 T14))
  342.   (! (= (set547 bv0 bv1) (or (Rtos0 c bv0 bv1) (Rtos0 b bv0 bv1)))
  343.      :pattern ((set547 bv0 bv1))
  344.      :pattern ((Rtos0 c bv0 bv1))
  345.      :pattern ((Rtos0 b bv0 bv1)))))
  346. (declare-fun set548 (T14 T14) Bool)
  347. (assert (forall ((bv1 T14) (bv0 T14))
  348.   (! (= (set548 bv0 bv1) (or (set546 bv0 bv1) (set547 bv0 bv1)))
  349.      :pattern ((set548 bv0 bv1))
  350.      :pattern ((set546 bv0 bv1))
  351.      :pattern ((set547 bv0 bv1)))))
  352. (assert (forall ((bv1 T14) (bv0 T14))
  353.   (! (= (Rtos0 anc_1045I bv0 bv1) (set548 bv0 bv1))
  354.      :pattern ((Rtos0 anc_1045I bv0 bv1))
  355.      :pattern ((set548 bv0 bv1)))))
  356. (declare-fun set549 (T14) Bool)
  357. (assert (forall ((bv0 T14))
  358.   (! (= (set549 bv0) (= bv0 y)) :pattern ((set549 bv0)))))
  359. (declare-fun set550 (T14 T14) Bool)
  360. (assert (forall ((bv1 T14) (bv0 T14))
  361.   (! (= (set550 bv0 bv1) (and (Rmem1 b bv0) (set549 bv1)))
  362.      :pattern ((set550 bv0 bv1))
  363.      :pattern ((Rmem1 b bv0) (set549 bv1)))))
  364. (declare-fun set551 (T14) Bool)
  365. (assert (forall ((bv0 T14))
  366.   (! (= (set551 bv0) (= bv0 y)) :pattern ((set551 bv0)))))
  367. (declare-fun set552 (T14 T14) Bool)
  368. (assert (forall ((bv1 T14) (bv0 T14))
  369.   (! (= (set552 bv0 bv1) (and (set551 bv0) (Rmem1 c bv1)))
  370.      :pattern ((set552 bv0 bv1))
  371.      :pattern ((set551 bv0) (Rmem1 c bv1)))))
  372. (declare-fun set553 (T14 T14) Bool)
  373. (assert (forall ((bv1 T14) (bv0 T14))
  374.   (! (= (set553 bv0 bv1) (and (Rmem1 b bv0) (Rmem1 c bv1)))
  375.      :pattern ((set553 bv0 bv1))
  376.      :pattern ((Rmem1 b bv0) (Rmem1 c bv1)))))
  377. (declare-fun set554 (T14 T14) Bool)
  378. (assert (forall ((bv1 T14) (bv0 T14))
  379.   (! (= (set554 bv0 bv1) (or (set552 bv0 bv1) (set553 bv0 bv1)))
  380.      :pattern ((set554 bv0 bv1))
  381.      :pattern ((set552 bv0 bv1))
  382.      :pattern ((set553 bv0 bv1)))))
  383. (declare-fun set556 (T14) Bool)
  384. (assert (forall ((bv0 T14))
  385.   (! (= (set556 bv0) (= bv0 y)) :pattern ((set556 bv0)))))
  386. (declare-fun set557 (T14) Bool)
  387. (assert (forall ((bv0 T14))
  388.   (! (= (set557 bv0) (or (Rmem1 c bv0) (Rmem1 b bv0)))
  389.      :pattern ((set557 bv0))
  390.      :pattern ((Rmem1 c bv0))
  391.      :pattern ((Rmem1 b bv0)))))
  392. (declare-fun set558 (T14) Bool)
  393. (assert (forall ((bv0 T14))
  394.   (! (= (set558 bv0) (or (set556 bv0) (set557 bv0)))
  395.      :pattern ((set558 bv0))
  396.      :pattern ((set556 bv0))
  397.      :pattern ((set557 bv0)))))
  398. (assert (forall ((bv0 T14))
  399.   (! (= (Rmem1 anc_1045I bv0) (set558 bv0))
  400.      :pattern ((Rmem1 anc_1045I bv0))
  401.      :pattern ((set558 bv0)))))
  402. (declare-fun set560 (T14) Bool)
  403. (assert (forall ((bv0 T14))
  404.   (! (= (set560 bv0) (= bv0 x)) :pattern ((set560 bv0)))))
  405. (declare-fun set561 (T14 T14) Bool)
  406. (assert (forall ((bv1 T14) (bv0 T14))
  407.   (! (= (set561 bv0 bv1) (and (Rmem1 a bv0) (set560 bv1)))
  408.      :pattern ((set561 bv0 bv1))
  409.      :pattern ((Rmem1 a bv0) (set560 bv1)))))
  410. (declare-fun set562 (T14) Bool)
  411. (assert (forall ((bv0 T14))
  412.   (! (= (set562 bv0) (= bv0 x)) :pattern ((set562 bv0)))))
  413. (declare-fun set563 (T14 T14) Bool)
  414. (assert (forall ((bv1 T14) (bv0 T14))
  415.   (! (= (set563 bv0 bv1) (and (set562 bv0) (Rmem1 anc_1045I bv1)))
  416.      :pattern ((set563 bv0 bv1))
  417.      :pattern ((set562 bv0) (Rmem1 anc_1045I bv1)))))
  418. (declare-fun set564 (T14 T14) Bool)
  419. (assert (forall ((bv1 T14) (bv0 T14))
  420.   (! (= (set564 bv0 bv1) (and (Rmem1 a bv0) (Rmem1 anc_1045I bv1)))
  421.      :pattern ((set564 bv0 bv1))
  422.      :pattern ((Rmem1 a bv0) (Rmem1 anc_1045I bv1)))))
  423. (declare-fun set565 (T14 T14) Bool)
  424. (assert (forall ((bv1 T14) (bv0 T14))
  425.   (! (= (set565 bv0 bv1) (or (set563 bv0 bv1) (set564 bv0 bv1)))
  426.      :pattern ((set565 bv0 bv1))
  427.      :pattern ((set563 bv0 bv1))
  428.      :pattern ((set564 bv0 bv1)))))
  429. (declare-fun set566 (T14 T14) Bool)
  430. (assert (forall ((bv1 T14) (bv0 T14))
  431.   (! (= (set566 bv0 bv1) (or (set561 bv0 bv1) (set565 bv0 bv1)))
  432.      :pattern ((set566 bv0 bv1))
  433.      :pattern ((set561 bv0 bv1))
  434.      :pattern ((set565 bv0 bv1)))))
  435. (declare-fun set567 (T14 T14) Bool)
  436. (assert (forall ((bv1 T14) (bv0 T14))
  437.   (! (= (set567 bv0 bv1) (or (Rtos0 anc_1045I bv0 bv1) (Rtos0 a bv0 bv1)))
  438.      :pattern ((set567 bv0 bv1))
  439.      :pattern ((Rtos0 anc_1045I bv0 bv1))
  440.      :pattern ((Rtos0 a bv0 bv1)))))
  441. (declare-fun set568 (T14 T14) Bool)
  442. (assert (forall ((bv1 T14) (bv0 T14))
  443.   (! (= (set568 bv0 bv1) (or (set566 bv0 bv1) (set567 bv0 bv1)))
  444.      :pattern ((set568 bv0 bv1))
  445.      :pattern ((set566 bv0 bv1))
  446.      :pattern ((set567 bv0 bv1)))))
  447. (assert (forall ((bv1 T14) (bv0 T14))
  448.   (! (= (Rtos0 anc_1047I bv0 bv1) (set568 bv0 bv1))
  449.      :pattern ((Rtos0 anc_1047I bv0 bv1))
  450.      :pattern ((set568 bv0 bv1)))))
  451. (declare-fun set569 (T14) Bool)
  452. (assert (forall ((bv0 T14))
  453.   (! (= (set569 bv0) (= bv0 x)) :pattern ((set569 bv0)))))
  454. (declare-fun set570 (T14 T14) Bool)
  455. (assert (forall ((bv1 T14) (bv0 T14))
  456.   (! (= (set570 bv0 bv1) (and (Rmem1 a bv0) (set569 bv1)))
  457.      :pattern ((set570 bv0 bv1))
  458.      :pattern ((Rmem1 a bv0) (set569 bv1)))))
  459. (declare-fun set571 (T14) Bool)
  460. (assert (forall ((bv0 T14))
  461.   (! (= (set571 bv0) (= bv0 x)) :pattern ((set571 bv0)))))
  462. (declare-fun set572 (T14 T14) Bool)
  463. (assert (forall ((bv1 T14) (bv0 T14))
  464.   (! (= (set572 bv0 bv1) (and (set571 bv0) (Rmem1 anc_1045I bv1)))
  465.      :pattern ((set572 bv0 bv1))
  466.      :pattern ((set571 bv0) (Rmem1 anc_1045I bv1)))))
  467. (declare-fun set573 (T14 T14) Bool)
  468. (assert (forall ((bv1 T14) (bv0 T14))
  469.   (! (= (set573 bv0 bv1) (and (Rmem1 a bv0) (Rmem1 anc_1045I bv1)))
  470.      :pattern ((set573 bv0 bv1))
  471.      :pattern ((Rmem1 a bv0) (Rmem1 anc_1045I bv1)))))
  472. (declare-fun set574 (T14 T14) Bool)
  473. (assert (forall ((bv1 T14) (bv0 T14))
  474.   (! (= (set574 bv0 bv1) (or (set572 bv0 bv1) (set573 bv0 bv1)))
  475.      :pattern ((set574 bv0 bv1))
  476.      :pattern ((set572 bv0 bv1))
  477.      :pattern ((set573 bv0 bv1)))))
  478. (declare-fun set576 (T14) Bool)
  479. (assert (forall ((bv0 T14))
  480.   (! (= (set576 bv0) (= bv0 x)) :pattern ((set576 bv0)))))
  481. (declare-fun set577 (T14) Bool)
  482. (assert (forall ((bv0 T14))
  483.   (! (= (set577 bv0) (or (Rmem1 anc_1045I bv0) (Rmem1 a bv0)))
  484.      :pattern ((set577 bv0))
  485.      :pattern ((Rmem1 anc_1045I bv0))
  486.      :pattern ((Rmem1 a bv0)))))
  487. (declare-fun set578 (T14) Bool)
  488. (assert (forall ((bv0 T14))
  489.   (! (= (set578 bv0) (or (set576 bv0) (set577 bv0)))
  490.      :pattern ((set578 bv0))
  491.      :pattern ((set576 bv0))
  492.      :pattern ((set577 bv0)))))
  493. (assert (forall ((bv0 T14))
  494.   (! (= (Rmem1 anc_1047I bv0) (set578 bv0))
  495.      :pattern ((Rmem1 anc_1047I bv0))
  496.      :pattern ((set578 bv0)))))
  497. (declare-fun set580 (T14) Bool)
  498. (assert (forall ((bv0 T14))
  499.   (! (= (set580 bv0) (= bv0 y)) :pattern ((set580 bv0)))))
  500. (declare-fun set581 (T14 T14) Bool)
  501. (assert (forall ((bv1 T14) (bv0 T14))
  502.   (! (= (set581 bv0 bv1) (and (Rmem1 anc_1056I bv0) (set580 bv1)))
  503.      :pattern ((set581 bv0 bv1))
  504.      :pattern ((Rmem1 anc_1056I bv0) (set580 bv1)))))
  505. (declare-fun set582 (T14) Bool)
  506. (assert (forall ((bv0 T14))
  507.   (! (= (set582 bv0) (= bv0 y)) :pattern ((set582 bv0)))))
  508. (declare-fun set583 (T14 T14) Bool)
  509. (assert (forall ((bv1 T14) (bv0 T14))
  510.   (! (= (set583 bv0 bv1) (and (set582 bv0) (Rmem1 anc_1063I bv1)))
  511.      :pattern ((set583 bv0 bv1))
  512.      :pattern ((set582 bv0) (Rmem1 anc_1063I bv1)))))
  513. (declare-fun set584 (T14 T14) Bool)
  514. (assert (forall ((bv1 T14) (bv0 T14))
  515.   (! (= (set584 bv0 bv1) (and (Rmem1 anc_1056I bv0) (Rmem1 anc_1063I bv1)))
  516.      :pattern ((set584 bv0 bv1))
  517.      :pattern ((Rmem1 anc_1056I bv0) (Rmem1 anc_1063I bv1)))))
  518. (declare-fun set585 (T14 T14) Bool)
  519. (assert (forall ((bv1 T14) (bv0 T14))
  520.   (! (= (set585 bv0 bv1) (or (set583 bv0 bv1) (set584 bv0 bv1)))
  521.      :pattern ((set585 bv0 bv1))
  522.      :pattern ((set583 bv0 bv1))
  523.      :pattern ((set584 bv0 bv1)))))
  524. (declare-fun set586 (T14 T14) Bool)
  525. (assert (forall ((bv1 T14) (bv0 T14))
  526.   (! (= (set586 bv0 bv1) (or (set581 bv0 bv1) (set585 bv0 bv1)))
  527.      :pattern ((set586 bv0 bv1))
  528.      :pattern ((set581 bv0 bv1))
  529.      :pattern ((set585 bv0 bv1)))))
  530. (declare-fun set587 (T14 T14) Bool)
  531. (assert (forall ((bv1 T14) (bv0 T14))
  532.   (! (= (set587 bv0 bv1)
  533.         (or (Rtos0 anc_1063I bv0 bv1) (Rtos0 anc_1056I bv0 bv1)))
  534.      :pattern ((set587 bv0 bv1))
  535.      :pattern ((Rtos0 anc_1063I bv0 bv1))
  536.      :pattern ((Rtos0 anc_1056I bv0 bv1)))))
  537. (declare-fun set588 (T14 T14) Bool)
  538. (assert (forall ((bv1 T14) (bv0 T14))
  539.   (! (= (set588 bv0 bv1) (or (set586 bv0 bv1) (set587 bv0 bv1)))
  540.      :pattern ((set588 bv0 bv1))
  541.      :pattern ((set586 bv0 bv1))
  542.      :pattern ((set587 bv0 bv1)))))
  543. (assert (forall ((bv1 T14) (bv0 T14))
  544.   (! (= (Rtos0 v_15 bv0 bv1) (set588 bv0 bv1))
  545.      :pattern ((Rtos0 v_15 bv0 bv1))
  546.      :pattern ((set588 bv0 bv1)))))
  547. (declare-fun set589 (T14) Bool)
  548. (assert (forall ((bv0 T14))
  549.   (! (= (set589 bv0) (= bv0 y)) :pattern ((set589 bv0)))))
  550. (declare-fun set590 (T14 T14) Bool)
  551. (assert (forall ((bv1 T14) (bv0 T14))
  552.   (! (= (set590 bv0 bv1) (and (Rmem1 anc_1056I bv0) (set589 bv1)))
  553.      :pattern ((set590 bv0 bv1))
  554.      :pattern ((Rmem1 anc_1056I bv0) (set589 bv1)))))
  555. (declare-fun set591 (T14) Bool)
  556. (assert (forall ((bv0 T14))
  557.   (! (= (set591 bv0) (= bv0 y)) :pattern ((set591 bv0)))))
  558. (declare-fun set592 (T14 T14) Bool)
  559. (assert (forall ((bv1 T14) (bv0 T14))
  560.   (! (= (set592 bv0 bv1) (and (set591 bv0) (Rmem1 anc_1063I bv1)))
  561.      :pattern ((set592 bv0 bv1))
  562.      :pattern ((set591 bv0) (Rmem1 anc_1063I bv1)))))
  563. (declare-fun set593 (T14 T14) Bool)
  564. (assert (forall ((bv1 T14) (bv0 T14))
  565.   (! (= (set593 bv0 bv1) (and (Rmem1 anc_1056I bv0) (Rmem1 anc_1063I bv1)))
  566.      :pattern ((set593 bv0 bv1))
  567.      :pattern ((Rmem1 anc_1056I bv0) (Rmem1 anc_1063I bv1)))))
  568. (declare-fun set594 (T14 T14) Bool)
  569. (assert (forall ((bv1 T14) (bv0 T14))
  570.   (! (= (set594 bv0 bv1) (or (set592 bv0 bv1) (set593 bv0 bv1)))
  571.      :pattern ((set594 bv0 bv1))
  572.      :pattern ((set592 bv0 bv1))
  573.      :pattern ((set593 bv0 bv1)))))
  574. (declare-fun set596 (T14) Bool)
  575. (assert (forall ((bv0 T14))
  576.   (! (= (set596 bv0) (= bv0 y)) :pattern ((set596 bv0)))))
  577. (declare-fun set597 (T14) Bool)
  578. (assert (forall ((bv0 T14))
  579.   (! (= (set597 bv0) (or (Rmem1 anc_1063I bv0) (Rmem1 anc_1056I bv0)))
  580.      :pattern ((set597 bv0))
  581.      :pattern ((Rmem1 anc_1063I bv0))
  582.      :pattern ((Rmem1 anc_1056I bv0)))))
  583. (declare-fun set598 (T14) Bool)
  584. (assert (forall ((bv0 T14))
  585.   (! (= (set598 bv0) (or (set596 bv0) (set597 bv0)))
  586.      :pattern ((set598 bv0))
  587.      :pattern ((set596 bv0))
  588.      :pattern ((set597 bv0)))))
  589. (assert (forall ((bv0 T14))
  590.   (! (= (Rmem1 v_15 bv0) (set598 bv0))
  591.      :pattern ((Rmem1 v_15 bv0))
  592.      :pattern ((set598 bv0)))))
  593. (assert (not (forall ((bv1 T14) (bv0 T14))
  594.        (! (= (Rtos0 v_15 bv0 bv1) (Rtos0 x_0 bv0 bv1))
  595.           :pattern ((Rtos0 v_15 bv0 bv1))
  596.           :pattern ((Rtos0 x_0 bv0 bv1))))))
  597. (check-sat)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!