mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 03:25:43 +00:00
Add ABV model regression test
This commit is contained in:
copilot-swe-agent[bot]
GitHub
parent
25f86866d8
commit
936dc25c0c
2 changed files with 776 additions and 0 deletions
729
src/test/issue_7132.smt2
Normal file
729
src/test/issue_7132.smt2
Normal file
|
|
@ -0,0 +1,729 @@
|
||||||
|
;
|
||||||
|
(set-info :status unknown)
|
||||||
|
(set-logic ABV)
|
||||||
|
(declare-fun sp0 () (_ BitVec 32))
|
||||||
|
(declare-fun r0 () (_ BitVec 32))
|
||||||
|
(declare-fun id.m6 () (Array (_ BitVec 32) (_ BitVec 8)))
|
||||||
|
(declare-fun rc () (_ BitVec 32))
|
||||||
|
(declare-fun la1 () (_ BitVec 32))
|
||||||
|
(declare-fun dl3e () (_ BitVec 32))
|
||||||
|
(declare-fun dl3b () (_ BitVec 32))
|
||||||
|
(declare-fun dl1e () (_ BitVec 32))
|
||||||
|
(declare-fun dl1b () (_ BitVec 32))
|
||||||
|
(declare-fun sp3 () (_ BitVec 32))
|
||||||
|
(declare-fun sp2 () (_ BitVec 32))
|
||||||
|
(declare-fun r43 () (_ BitVec 32))
|
||||||
|
(declare-fun r42v () (_ BitVec 32))
|
||||||
|
(declare-fun r44 () (_ BitVec 32))
|
||||||
|
(declare-fun r42 () (_ BitVec 32))
|
||||||
|
(declare-fun sp08 () (_ BitVec 32))
|
||||||
|
(declare-fun r402 () (_ BitVec 32))
|
||||||
|
(declare-fun r403 () (_ BitVec 32))
|
||||||
|
(declare-fun i () (_ BitVec 32))
|
||||||
|
(declare-fun l3 () (_ BitVec 32))
|
||||||
|
(declare-fun r1 () (_ BitVec 32))
|
||||||
|
(declare-fun a () (_ BitVec 32))
|
||||||
|
(declare-fun b () (_ BitVec 32))
|
||||||
|
(declare-fun id.ma () (Array (_ BitVec 32) (_ BitVec 8)))
|
||||||
|
(declare-fun l1b () (_ BitVec 32))
|
||||||
|
(declare-fun l1ia () Bool)
|
||||||
|
(declare-fun la01 () (_ BitVec 32))
|
||||||
|
(declare-fun se () (_ BitVec 32))
|
||||||
|
(declare-fun stack_begin () (_ BitVec 32))
|
||||||
|
(declare-fun rodata.size () (_ BitVec 32))
|
||||||
|
(declare-fun ssz () (_ BitVec 32))
|
||||||
|
(declare-fun l1=/_end () (_ BitVec 32))
|
||||||
|
(declare-fun l1=/_begin () (_ BitVec 32))
|
||||||
|
(declare-fun l0e () (_ BitVec 32))
|
||||||
|
(declare-fun l0=/_begin () (_ BitVec 32))
|
||||||
|
(declare-fun re () (_ BitVec 32))
|
||||||
|
(declare-fun rodata_begin () (_ BitVec 32))
|
||||||
|
(declare-fun la0 () (_ BitVec 32))
|
||||||
|
(declare-fun la3 () (_ BitVec 32))
|
||||||
|
(declare-fun ma.LEA () (Array (_ BitVec 32) (_ BitVec 8)))
|
||||||
|
(declare-fun la14 () (_ BitVec 32))
|
||||||
|
(declare-fun la2e () (_ BitVec 32))
|
||||||
|
(declare-fun l2b () (_ BitVec 32))
|
||||||
|
(declare-fun l2ia () Bool)
|
||||||
|
(declare-fun l3e () (_ BitVec 32))
|
||||||
|
(declare-fun l3ia () Bool)
|
||||||
|
(declare-fun d4 () (_ BitVec 32))
|
||||||
|
(declare-fun m.Lfc.1%d=/ () (Array (_ BitVec 32) (_ BitVec 8)))
|
||||||
|
(declare-fun d2ia () Bool)
|
||||||
|
(declare-fun d2ls () (_ BitVec 32))
|
||||||
|
(declare-fun l2ls () (_ BitVec 32))
|
||||||
|
(declare-fun d1ia () Bool)
|
||||||
|
(declare-fun d3b () (_ BitVec 32))
|
||||||
|
(declare-fun l3b () (_ BitVec 32))
|
||||||
|
(declare-fun d3ls () (_ BitVec 32))
|
||||||
|
(declare-fun dl2 () (_ BitVec 32))
|
||||||
|
(declare-fun m.Lfc.1=/ () (Array (_ BitVec 32) (_ BitVec 8)))
|
||||||
|
(declare-fun m.Lfc.0=/ () (Array (_ BitVec 32) (_ BitVec 8)))
|
||||||
|
(declare-fun d1b4 () (_ BitVec 32))
|
||||||
|
(declare-fun l3ls () (_ BitVec 32))
|
||||||
|
(declare-fun m.Lfc.3%d=/ () (Array (_ BitVec 32) (_ BitVec 8)))
|
||||||
|
(assert
|
||||||
|
(let ((?x432 (bvadd sp0 (_ bv4294967292 32))))
|
||||||
|
(let ((r0x4 (bvmul (_ bv4 32) r0)))
|
||||||
|
(let ((?x824 (bvadd (bvadd sp0 r0x4) (_ bv4294965236 32))))
|
||||||
|
(let ((?x693 (bvadd ?x824 (_ bv3 32))))
|
||||||
|
(let ((?x834 (bvadd ?x824 (_ bv2 32))))
|
||||||
|
(let ((?x328 (bvadd ?x824 (_ bv1 32))))
|
||||||
|
(let ((?x222 (bvadd ?x824 (_ bv0 32))))
|
||||||
|
(let ((?x5 (bvadd sp0 (_ bv4294967283 32))))
|
||||||
|
(let (($x541 (= dl3e ?x5)))
|
||||||
|
(let ((?x890 (bvadd sp0 (_ bv4294965235 32))))
|
||||||
|
(let (($x682 (= dl1e ?x890)))
|
||||||
|
(let ((?x1152 (bvadd sp0 (_ bv4294964980 32))))
|
||||||
|
(let (($x852 (= dl1b ?x1152)))
|
||||||
|
(let ((?x375 (bvadd sp0 (_ bv4294964964 32))))
|
||||||
|
(let (($x653 (= sp3 ?x375)))
|
||||||
|
(let ((?x373 (bvadd sp0 (_ bv4294967288 32))))
|
||||||
|
(let (($x1049 (= sp2 ?x373)))
|
||||||
|
(let (($x1081 (= r44 ?x375)))
|
||||||
|
(let (($x986 (= r42 ?x373)))
|
||||||
|
(let (($x339 (= sp08 ?x432)))
|
||||||
|
(let (($x120 (= r402 ?x432)))
|
||||||
|
(let (($x995 (= r403 sp0)))
|
||||||
|
(let (($x449 (= i r0)))
|
||||||
|
(let ((?x1055 (bvadd la1 (_ bv4294967280 32))))
|
||||||
|
(let (($x271 (= ?x1055 r44)))
|
||||||
|
(let (($x764 (= a r1)))
|
||||||
|
(let ((?x1128 (bvadd la1 (_ bv2316 32))))
|
||||||
|
(let (($x599 (= ?x1128 sp0)))
|
||||||
|
(let ((?x288 (bvadd sp0 (_ bv8 32))))
|
||||||
|
(let ((?x913 (select id.m6 ?x288)))
|
||||||
|
(let ((?x1072 (bvadd ?x288 (_ bv1 32))))
|
||||||
|
(let ((?x15 (select id.m6 ?x1072)))
|
||||||
|
(let ((?x1008 (bvadd ?x288 (_ bv2 32))))
|
||||||
|
(let ((?x1218 (select id.m6 ?x1008)))
|
||||||
|
(let ((?x782 (bvadd ?x288 (_ bv3 32))))
|
||||||
|
(let ((?x421 (select id.m6 ?x782)))
|
||||||
|
(let ((?x530 (concat ?x421 (concat ?x1218 (concat ?x15 ?x913)))))
|
||||||
|
(let (($x287 (= b ?x530)))
|
||||||
|
(let ((?x1227 (bvadd sp0 (_ bv4 32))))
|
||||||
|
(let ((?x363 (select id.m6 ?x1227)))
|
||||||
|
(let ((?x207 (bvadd ?x1227 (_ bv1 32))))
|
||||||
|
(let ((?x1217 (select id.m6 ?x207)))
|
||||||
|
(let ((?x1073 (bvadd ?x1227 (_ bv2 32))))
|
||||||
|
(let ((?x127 (select id.m6 ?x1073)))
|
||||||
|
(let ((?x356 (bvadd ?x1227 (_ bv3 32))))
|
||||||
|
(let ((?x38 (select id.m6 ?x356)))
|
||||||
|
(let ((?x713 (concat ?x38 (concat ?x127 (concat ?x1217 ?x363)))))
|
||||||
|
(let (($x567 (= a ?x713)))
|
||||||
|
(let (($x1265 (= ?x1055 sp3)))
|
||||||
|
(let ((?x233 (select id.m6 sp0)))
|
||||||
|
(let ((?x338 (bvadd sp0 (_ bv1 32))))
|
||||||
|
(let ((?x171 (select id.m6 ?x338)))
|
||||||
|
(let ((?x1232 (bvadd sp0 (_ bv2 32))))
|
||||||
|
(let ((?x1079 (select id.m6 ?x1232)))
|
||||||
|
(let ((?x1070 (bvadd sp0 (_ bv3 32))))
|
||||||
|
(let ((?x291 (select id.m6 ?x1070)))
|
||||||
|
(let ((?x245 (concat ?x291 (concat ?x1079 (concat ?x171 ?x233)))))
|
||||||
|
(let (($x1014 (= rc ?x245)))
|
||||||
|
(let ((?x620 ((_ extract 3 0) la1)))
|
||||||
|
(let (($x234 (= (_ bv0 4) ?x620)))
|
||||||
|
(let (($x618 (= (select id.ma (bvadd ?x288 (_ bv0 32))) (_ bv5 8))))
|
||||||
|
(let (($x1279 (and (and $x618 (= (select id.ma ?x1072) (_ bv5 8))) (= (select id.ma ?x1008) (_ bv5 8)))))
|
||||||
|
(let (($x838 (and $x1279 (= (select id.ma ?x782) (_ bv5 8)))))
|
||||||
|
(let (($x471 (and (bvule ?x288 (bvsub (bvadd ?x288 (_ bv4 32)) (_ bv1 32))) $x838)))
|
||||||
|
(let (($x524 (= $x471 true)))
|
||||||
|
(let (($x774 (= (select id.ma (bvadd ?x373 (_ bv0 32))) (_ bv7 8))))
|
||||||
|
(let (($x987 (and $x774 (= (select id.ma (bvadd ?x373 (_ bv1 32))) (_ bv7 8)))))
|
||||||
|
(let (($x1262 (and $x987 (= (select id.ma (bvadd ?x373 (_ bv2 32))) (_ bv7 8)))))
|
||||||
|
(let (($x1254 (and $x1262 (= (select id.ma (bvadd ?x373 (_ bv3 32))) (_ bv7 8)))))
|
||||||
|
(let (($x1272 (and (bvule ?x373 (bvsub (bvadd ?x373 (_ bv4 32)) (_ bv1 32))) $x1254)))
|
||||||
|
(let (($x938 (= $x1272 true)))
|
||||||
|
(let (($x1310 (= (select id.ma (bvadd ?x432 (_ bv0 32))) (_ bv7 8))))
|
||||||
|
(let (($x1056 (and $x1310 (= (select id.ma (bvadd ?x432 (_ bv1 32))) (_ bv7 8)))))
|
||||||
|
(let (($x561 (and $x1056 (= (select id.ma (bvadd ?x432 (_ bv2 32))) (_ bv7 8)))))
|
||||||
|
(let (($x724 (and $x561 (= (select id.ma (bvadd ?x432 (_ bv3 32))) (_ bv7 8)))))
|
||||||
|
(let (($x343 (and (bvule ?x432 (bvsub (bvadd ?x432 (_ bv4 32)) (_ bv1 32))) $x724)))
|
||||||
|
(let (($x513 (= $x343 true)))
|
||||||
|
(let (($x1086 (= la1 l1b)))
|
||||||
|
(let (($x1327 (or l1ia $x1086)))
|
||||||
|
(let (($x168 (= $x1327 true)))
|
||||||
|
(let (($x50 (= (select id.ma (bvadd sp0 (_ bv0 32))) (_ bv7 8))))
|
||||||
|
(let (($x123 (and $x50 (= (select id.ma ?x338) (_ bv7 8)))))
|
||||||
|
(let (($x485 (and (and $x123 (= (select id.ma ?x1232) (_ bv7 8))) (= (select id.ma ?x1070) (_ bv7 8)))))
|
||||||
|
(let (($x1166 (and (bvule sp0 (bvsub ?x1227 (_ bv1 32))) $x485)))
|
||||||
|
(let (($x277 (= $x1166 true)))
|
||||||
|
(let ((?x590 (select id.ma (bvadd (bvadd sp0 (_ bv0 32)) (_ bv0 32)))))
|
||||||
|
(let (($x809 (or (= ?x590 (_ bv2 8)) (= ?x590 (_ bv3 8)))))
|
||||||
|
(let (($x857 (or (or $x809 (= ?x590 (_ bv4 8))) (= ?x590 (_ bv5 8)))))
|
||||||
|
(let (($x663 (and (distinct (_ bv1 32) (_ bv0 32)) true)))
|
||||||
|
(let (($x78 (and (and $x663 (bvule sp0 (bvsub ?x338 (_ bv1 32)))) (or $x857 (= ?x590 (_ bv7 8))))))
|
||||||
|
(let (($x623 (= $x78 true)))
|
||||||
|
(let (($x454 (bvsge r0 (_ bv0 32))))
|
||||||
|
(let (($x806 (= $x454 true)))
|
||||||
|
(let (($x462 (bvsle r0 (_ bv255 32))))
|
||||||
|
(let (($x57 (= $x462 true)))
|
||||||
|
(let (($x1246 (= sp3 ?x1055)))
|
||||||
|
(let (($x555 (or l1ia $x1246)))
|
||||||
|
(let (($x167 (= $x555 true)))
|
||||||
|
(let (($x146 (= la01 ?x288)))
|
||||||
|
(let (($x499 (= $x146 true)))
|
||||||
|
(let (($x646 (bvule r44 sp0)))
|
||||||
|
(let (($x825 (= $x646 true)))
|
||||||
|
(let (($x1127 (forall ((rsm-bounded-var! (_ BitVec 32)) )(let ((?x500 (select id.ma rsm-bounded-var!)))
|
||||||
|
(let (($x1133 (= ?x500 (_ bv7 8))))
|
||||||
|
(let (($x802 (= ?x500 (_ bv5 8))))
|
||||||
|
(let (($x671 (or (or (or (= ?x500 (_ bv2 8)) (= ?x500 (_ bv3 8))) (= ?x500 (_ bv4 8))) $x802)))
|
||||||
|
(let (($x836 (and (bvule stack_begin rsm-bounded-var!) (bvule rsm-bounded-var! se))))
|
||||||
|
(= $x836 (or $x671 $x1133))))))))
|
||||||
|
))
|
||||||
|
(let (($x808 (forall ((icm-bounded-var! (_ BitVec 32)) )(let ((?x500 (select id.ma icm-bounded-var!)))
|
||||||
|
(let (($x802 (= ?x500 (_ bv5 8))))
|
||||||
|
(let (($x1044 (bvule icm-bounded-var! l1=/_end)))
|
||||||
|
(let (($x236 (bvule l1=/_begin icm-bounded-var!)))
|
||||||
|
(= (and $x236 $x1044) $x802))))))
|
||||||
|
))
|
||||||
|
(let (($x927 (forall ((icm-bounded-var! (_ BitVec 32)) )(let ((?x500 (select id.ma icm-bounded-var!)))
|
||||||
|
(let (($x578 (= ?x500 (_ bv4 8))))
|
||||||
|
(let (($x1151 (bvule icm-bounded-var! l0e)))
|
||||||
|
(let (($x31 (bvule l0=/_begin icm-bounded-var!)))
|
||||||
|
(= (and $x31 $x1151) $x578))))))
|
||||||
|
))
|
||||||
|
(let ((?x823 (bvadd (bvadd (_ bv4294967295 32) stack_begin) ssz)))
|
||||||
|
(let (($x173 (= se ?x823)))
|
||||||
|
(let ((?x193 (bvadd (_ bv3 32) l1=/_begin)))
|
||||||
|
(let (($x320 (= l1=/_end ?x193)))
|
||||||
|
(let (($x634 (bvule stack_begin se)))
|
||||||
|
(let (($x199 (bvule l1=/_begin l1=/_end)))
|
||||||
|
(let ((?x447 (bvadd l0=/_begin (_ bv3 32))))
|
||||||
|
(let (($x521 (= l0e ?x447)))
|
||||||
|
(let (($x242 (bvule l0=/_begin l0e)))
|
||||||
|
(let (($x1201 (and (and (and (and (and (and $x242 $x521) $x199) $x634) $x320) $x173) $x927)))
|
||||||
|
(let (($x133 (and $x1201 $x808)))
|
||||||
|
(let (($x132 (and $x133 (not (= (_ bv0 32) ssz)))))
|
||||||
|
(let (($x1336 (forall ((icm-bounded-var! (_ BitVec 32)) )(let (($x593 (and (bvule rodata_begin icm-bounded-var!) (bvule icm-bounded-var! re))))
|
||||||
|
(= $x593 (= (select id.ma icm-bounded-var!) (_ bv8 8)))))
|
||||||
|
))
|
||||||
|
(let ((?x919 (bvadd (bvadd (_ bv4294967295 32) rodata_begin) rodata.size)))
|
||||||
|
(let (($x125 (= re ?x919)))
|
||||||
|
(let (($x576 (bvule rodata_begin re)))
|
||||||
|
(let (($x305 (and (and (and $x576 $x125) $x1336) $x132)))
|
||||||
|
(let (($x738 (and $x305 (not (= (_ bv0 32) rodata.size)))))
|
||||||
|
(let ((?x692 (bvadd (_ bv1 32) se)))
|
||||||
|
(let ((?x1176 (bvand (_ bv4294963200 32) ?x692)))
|
||||||
|
(let (($x1129 (= ?x692 ?x1176)))
|
||||||
|
(let ((?x1302 (bvand stack_begin (_ bv4294963200 32))))
|
||||||
|
(let (($x661 (= stack_begin ?x1302)))
|
||||||
|
(let ((?x1113 (bvand la01 (_ bv3 32))))
|
||||||
|
(let (($x275 (= (_ bv0 32) ?x1113)))
|
||||||
|
(let ((?x1247 (bvand la0 (_ bv3 32))))
|
||||||
|
(let (($x231 (= (_ bv0 32) ?x1247)))
|
||||||
|
(let (($x349 (bvuge l1=/_end l0=/_begin)))
|
||||||
|
(let (($x143 (bvuge l0e l1=/_begin)))
|
||||||
|
(let (($x951 (and $x143 $x349)))
|
||||||
|
(let (($x860 (not $x951)))
|
||||||
|
(let (($x1011 (and $x860 $x860)))
|
||||||
|
(let (($x1039 (bvuge re stack_begin)))
|
||||||
|
(let (($x1101 (bvuge se rodata_begin)))
|
||||||
|
(let (($x1282 (and $x1101 $x1039)))
|
||||||
|
(let (($x1239 (not $x1282)))
|
||||||
|
(let (($x56 (and $x1239 $x1239)))
|
||||||
|
(let (($x1068 (= (bvand ?x1227 (_ bv4294967280 32)) ?x1227)))
|
||||||
|
(let ((?x180 (bvadd sp0 (_ bv11 32))))
|
||||||
|
(let (($x30 (bvule ?x180 se)))
|
||||||
|
(let (($x252 (bvule sp0 ?x180)))
|
||||||
|
(let (($x1250 (bvule stack_begin sp0)))
|
||||||
|
(let (($x147 (= la01 l1=/_begin)))
|
||||||
|
(let (($x1131 (= la0 l0=/_begin)))
|
||||||
|
(let (($x387 (and (and (and (and (and (and $x1131 $x147) $x1250) $x252) $x30) $x1068) $x56)))
|
||||||
|
(let (($x1061 (and (and (and (and (and (and $x387 $x1011) $x231) $x275) $x661) $x1129) $x738)))
|
||||||
|
(let (($x1076 (and $x1061 $x1127)))
|
||||||
|
(let (($x254 (= (select id.ma (bvadd (_ bv0 32) (_ bv0 32))) (_ bv6 8))))
|
||||||
|
(let (($x249 (and (and $x663 (bvule (_ bv0 32) (bvsub (bvadd (_ bv0 32) (_ bv1 32)) (_ bv1 32)))) $x254)))
|
||||||
|
(let (($x1001 (and $x249 $x1076)))
|
||||||
|
(let (($x968 (= $x1001 true)))
|
||||||
|
(let (($x508 (= la0 ?x1227)))
|
||||||
|
(let (($x895 (= $x508 true)))
|
||||||
|
(let (($x335 (bvule r0 (_ bv255 32))))
|
||||||
|
(let (($x1194 (= $x335 true)))
|
||||||
|
(let (($x881 (= (select id.ma (bvadd ?x1227 (_ bv0 32))) (_ bv4 8))))
|
||||||
|
(let (($x197 (and (and $x881 (= (select id.ma ?x207) (_ bv4 8))) (= (select id.ma ?x1073) (_ bv4 8)))))
|
||||||
|
(let (($x945 (and $x197 (= (select id.ma ?x356) (_ bv4 8)))))
|
||||||
|
(let (($x490 (and (bvule ?x1227 (bvsub (bvadd ?x1227 (_ bv4 32)) (_ bv1 32))) $x945)))
|
||||||
|
(let (($x1050 (= $x490 true)))
|
||||||
|
(let (($x6 (= (_ bv255 32) r0)))
|
||||||
|
(let (($x223 (bvult r402 sp0)))
|
||||||
|
(let (($x849 (= $x223 true)))
|
||||||
|
(let (($x398 (bvult sp08 sp0)))
|
||||||
|
(let (($x240 (= $x398 true)))
|
||||||
|
(let (($x701 (bvule sp08 sp0)))
|
||||||
|
(let (($x1307 (= $x701 true)))
|
||||||
|
(let (($x122 (bvult r42 sp0)))
|
||||||
|
(let (($x477 (= $x122 true)))
|
||||||
|
(let (($x1171 (bvule r42 sp0)))
|
||||||
|
(let (($x677 (= $x1171 true)))
|
||||||
|
(let (($x647 (bvult r44 sp0)))
|
||||||
|
(let (($x731 (= $x647 true)))
|
||||||
|
(let (($x280 (bvule r42v sp0)))
|
||||||
|
(let (($x887 (= $x280 true)))
|
||||||
|
(let (($x514 (bvult r43 sp0)))
|
||||||
|
(let (($x510 (bvule r43 sp0)))
|
||||||
|
(let (($x1219 (= $x510 true)))
|
||||||
|
(let (($x1013 (bvult sp2 sp0)))
|
||||||
|
(let (($x588 (= $x1013 true)))
|
||||||
|
(let (($x1162 (bvule sp2 sp0)))
|
||||||
|
(let (($x531 (= $x1162 true)))
|
||||||
|
(let (($x843 (bvult sp3 sp0)))
|
||||||
|
(let (($x1341 (= $x843 true)))
|
||||||
|
(let (($x1110 (bvule sp3 sp0)))
|
||||||
|
(let (($x841 (= $x1110 true)))
|
||||||
|
(let (($x248 (bvult dl1b sp0)))
|
||||||
|
(let (($x788 (= $x248 true)))
|
||||||
|
(let (($x758 (bvule dl1b sp0)))
|
||||||
|
(let (($x227 (= $x758 true)))
|
||||||
|
(let (($x417 (bvult dl1e sp0)))
|
||||||
|
(let (($x289 (= $x417 true)))
|
||||||
|
(let (($x75 (bvule dl1e sp0)))
|
||||||
|
(let (($x84 (= $x75 true)))
|
||||||
|
(let (($x632 (bvult dl3b sp0)))
|
||||||
|
(let (($x410 (= $x632 true)))
|
||||||
|
(let (($x1216 (bvule dl3b sp0)))
|
||||||
|
(let (($x835 (= $x1216 true)))
|
||||||
|
(let (($x94 (bvult dl3e sp0)))
|
||||||
|
(let (($x976 (= $x94 true)))
|
||||||
|
(let (($x585 (bvule dl3e sp0)))
|
||||||
|
(let (($x1276 (= $x585 true)))
|
||||||
|
(let ((?x1083 (bvmul (_ bv4294967292 32) i)))
|
||||||
|
(let (($x910 (= la3 ?x1083)))
|
||||||
|
(let (($x212 (not $x910)))
|
||||||
|
(let (($x558 (= $x212 true)))
|
||||||
|
(let (($x551 (bvsle i (_ bv255 32))))
|
||||||
|
(let (($x129 (=> $x551 $x558)))
|
||||||
|
(let ((?x1120 (bvmul (_ bv4 32) i)))
|
||||||
|
(let ((?x1146 (bvadd la3 ?x1120)))
|
||||||
|
(let ((?x365 (bvsub ?x1146 ?x1120)))
|
||||||
|
(let (($x589 (bvsge ?x1120 (_ bv0 32))))
|
||||||
|
(let (($x1023 (ite $x589 (bvuge ?x1146 ?x365) (bvult ?x1146 ?x365))))
|
||||||
|
(let (($x1220 (= $x1023 true)))
|
||||||
|
(let (($x166 (=> $x551 $x1220)))
|
||||||
|
(let (($x73 (= (bvand ?x1146 (_ bv4294967292 32)) ?x1146)))
|
||||||
|
(let (($x1095 (= $x73 true)))
|
||||||
|
(let (($x877 (=> $x551 $x1095)))
|
||||||
|
(let ((?x828 (bvadd a ?x1120)))
|
||||||
|
(let (($x1118 (= (bvand ?x828 (_ bv4294967292 32)) ?x828)))
|
||||||
|
(let (($x557 (= $x1118 true)))
|
||||||
|
(let (($x304 (=> $x551 $x557)))
|
||||||
|
(let ((?x433 (bvsub la3 (_ bv0 32))))
|
||||||
|
(let (($x112 (bvult la3 ?x433)))
|
||||||
|
(let (($x660 (bvuge la3 ?x433)))
|
||||||
|
(let (($x232 (ite (bvsge (_ bv0 32) (_ bv0 32)) $x660 $x112)))
|
||||||
|
(let (($x851 (= $x232 true)))
|
||||||
|
(let (($x318 (=> $x551 $x851)))
|
||||||
|
(let ((?x981 ((_ sign_extend 32) i)))
|
||||||
|
(let ((?x460 (bvmul (_ bv4 64) ?x981)))
|
||||||
|
(let ((?x148 ((_ extract 63 32) ?x460)))
|
||||||
|
(let (($x994 (= (_ bv0 32) ?x148)))
|
||||||
|
(let (($x791 (= $x994 true)))
|
||||||
|
(let (($x355 (=> $x551 $x791)))
|
||||||
|
(let (($x903 (bvslt i (_ bv0 32))))
|
||||||
|
(let ((?x761 (ite $x903 (_ bv4294967295 32) (_ bv0 32))))
|
||||||
|
(let (($x821 (= ?x148 ?x761)))
|
||||||
|
(let (($x361 (= $x821 true)))
|
||||||
|
(let (($x755 (=> $x551 $x361)))
|
||||||
|
(let (($x34 (ite $x589 (bvuge ?x828 (bvsub ?x828 ?x1120)) (bvult ?x828 (bvsub ?x828 ?x1120)))))
|
||||||
|
(let (($x579 (= $x34 true)))
|
||||||
|
(let (($x422 (=> $x551 $x579)))
|
||||||
|
(let (($x188 (= a ?x1083)))
|
||||||
|
(let (($x190 (not $x188)))
|
||||||
|
(let (($x1285 (= $x190 true)))
|
||||||
|
(let (($x332 (=> $x551 $x1285)))
|
||||||
|
(let (($x717 (forall ((icm-bounded-var! (_ BitVec 32)) )(let (($x526 (bvule icm-bounded-var! la14)))
|
||||||
|
(let (($x1337 (bvule l1b icm-bounded-var!)))
|
||||||
|
(= (and $x1337 $x526) (= (select ma.LEA icm-bounded-var!) (_ bv2 8))))))
|
||||||
|
))
|
||||||
|
(let (($x518 (xor l1ia $x717)))
|
||||||
|
(let (($x1139 (= $x518 true)))
|
||||||
|
(let (($x106 (forall ((icm-bounded-var! (_ BitVec 32)) )(let ((?x799 (select ma.LEA icm-bounded-var!)))
|
||||||
|
(let (($x1260 (= ?x799 (_ bv1 8))))
|
||||||
|
(let (($x1206 (bvule icm-bounded-var! la2e)))
|
||||||
|
(let (($x520 (bvule l2b icm-bounded-var!)))
|
||||||
|
(= (and $x520 $x1206) $x1260))))))
|
||||||
|
))
|
||||||
|
(let (($x198 (xor l2ia $x106)))
|
||||||
|
(let (($x1062 (= $x198 true)))
|
||||||
|
(let (($x762 (= (_ bv256 32) d4)))
|
||||||
|
(let (($x1100 (bvule l1b la14)))
|
||||||
|
(let (($x1130 (or l1ia $x1100)))
|
||||||
|
(let (($x744 (= $x1130 true)))
|
||||||
|
(let (($x346 (forall ((mae-bounded-var! (_ BitVec 32)) )(let ((?x1098 (select id.m6 mae-bounded-var!)))
|
||||||
|
(let ((?x453 (select m.Lfc.1%d=/ mae-bounded-var!)))
|
||||||
|
(let ((?x459 (select ma.LEA (bvadd mae-bounded-var! (_ bv0 32)))))
|
||||||
|
(let (($x663 (and (distinct (_ bv1 32) (_ bv0 32)) true)))
|
||||||
|
(let (($x1290 (and $x663 (bvule mae-bounded-var! (bvsub (bvadd mae-bounded-var! (_ bv1 32)) (_ bv1 32))))))
|
||||||
|
(=> (and $x1290 (= ?x459 (_ bv2 8))) (= ?x453 ?x1098))))))))
|
||||||
|
))
|
||||||
|
(let (($x1244 (and true $x346)))
|
||||||
|
(let (($x1242 (= $x1244 true)))
|
||||||
|
(let ((?x753 (select id.ma (bvadd (bvadd sp3 (_ bv0 32)) (_ bv0 32)))))
|
||||||
|
(let (($x409 (or (= ?x753 (_ bv2 8)) (= ?x753 (_ bv3 8)))))
|
||||||
|
(let (($x781 (or (or $x409 (= ?x753 (_ bv4 8))) (= ?x753 (_ bv5 8)))))
|
||||||
|
(let (($x278 (bvule sp3 (bvsub (bvadd sp3 (_ bv1 32)) (_ bv1 32)))))
|
||||||
|
(let (($x1210 (and (and $x663 $x278) (or $x781 (and true (= ?x753 (_ bv7 8)))))))
|
||||||
|
(let (($x149 (= $x1210 true)))
|
||||||
|
(let (($x619 (= la3 l2b)))
|
||||||
|
(let (($x458 (or l2ia $x619)))
|
||||||
|
(let (($x703 (= $x458 true)))
|
||||||
|
(let (($x830 (= l2ia d2ia)))
|
||||||
|
(let (($x1031 (= $x830 true)))
|
||||||
|
(let (($x540 (= l2ls d2ls)))
|
||||||
|
(let (($x1207 (or l2ia $x540)))
|
||||||
|
(let (($x935 (= $x1207 true)))
|
||||||
|
(let (($x1020 (= l1ia d1ia)))
|
||||||
|
(let (($x1168 (= $x1020 true)))
|
||||||
|
(let (($x1245 (forall ((maemvs-bounded-var! (_ BitVec 32)) )(let ((?x799 (select ma.LEA maemvs-bounded-var!)))
|
||||||
|
(let (($x1260 (= ?x799 (_ bv1 8))))
|
||||||
|
(let (($x991 (or false $x1260)))
|
||||||
|
(let ((?x500 (select id.ma maemvs-bounded-var!)))
|
||||||
|
(let (($x1133 (= ?x500 (_ bv7 8))))
|
||||||
|
(let (($x813 (and (=> (and (not $x991) (not $x1133)) (= ?x799 ?x500)) (=> $x991 (or $x1133 (= ?x500 (_ bv9 8)))))))
|
||||||
|
(and $x813 (=> $x1133 (or $x991 (= ?x799 (_ bv9 8))))))))))))
|
||||||
|
))
|
||||||
|
(let (($x875 (= $x1245 true)))
|
||||||
|
(let (($x954 (= l3b d3b)))
|
||||||
|
(let (($x492 (or l3ia $x954)))
|
||||||
|
(let (($x128 (= $x492 true)))
|
||||||
|
(let (($x244 (forall ((mia-bounded-var! (_ BitVec 32)) )(let ((?x799 (select ma.LEA mia-bounded-var!)))
|
||||||
|
(and (distinct ?x799 (_ bv3 8)) true)))
|
||||||
|
))
|
||||||
|
(let (($x598 (= l3ia $x244)))
|
||||||
|
(let (($x1193 (= $x598 true)))
|
||||||
|
(let (($x464 (= (_ bv0 32) d3ls)))
|
||||||
|
(let (($x286 (not $x464)))
|
||||||
|
(let (($x587 (or l3ia $x286)))
|
||||||
|
(let (($x1140 (= $x587 true)))
|
||||||
|
(let (($x1315 (= la3 dl2)))
|
||||||
|
(let (($x748 (or l2ia $x1315)))
|
||||||
|
(let (($x187 (= $x748 true)))
|
||||||
|
(let ((?x1208 (select id.ma (bvadd (bvadd r44 (_ bv0 32)) (_ bv0 32)))))
|
||||||
|
(let (($x1082 (or (and true (= ?x1208 (_ bv2 8))) (and true (= ?x1208 (_ bv3 8))))))
|
||||||
|
(let (($x1052 (or (or $x1082 (and true (= ?x1208 (_ bv4 8)))) (and true (= ?x1208 (_ bv5 8))))))
|
||||||
|
(let (($x383 (bvule r44 (bvsub (bvadd r44 (_ bv1 32)) (_ bv1 32)))))
|
||||||
|
(let (($x627 (and (and $x663 $x383) (or $x1052 (= ?x1208 (_ bv7 8))))))
|
||||||
|
(let (($x91 (= $x627 true)))
|
||||||
|
(let (($x1042 (= l3 l3b)))
|
||||||
|
(let (($x511 (or l3ia $x1042)))
|
||||||
|
(let (($x720 (= $x511 true)))
|
||||||
|
(let (($x592 (bvule r44 l3b)))
|
||||||
|
(let (($x704 (or l3ia $x592)))
|
||||||
|
(let (($x202 (= $x704 true)))
|
||||||
|
(let ((?x829 (bvadd (_ bv4294967295 32) l3b)))
|
||||||
|
(let ((?x327 (bvadd ?x829 d3ls)))
|
||||||
|
(let (($x354 (bvule ?x327 l3e)))
|
||||||
|
(let (($x334 (or l3ia $x354)))
|
||||||
|
(let (($x892 (= $x334 true)))
|
||||||
|
(let (($x1317 (= (_ bv1024 32) d3ls)))
|
||||||
|
(let ((?x1109 (bvadd l3 (_ bv4294966000 32))))
|
||||||
|
(let (($x427 (= sp3 ?x1109)))
|
||||||
|
(let (($x256 (or l3ia $x427)))
|
||||||
|
(let (($x909 (= $x256 true)))
|
||||||
|
(let ((?x1319 (bvadd (_ bv4294967295 32) l2b)))
|
||||||
|
(let ((?x359 (bvadd ?x1319 d2ls)))
|
||||||
|
(let (($x220 (bvule ?x359 la2e)))
|
||||||
|
(let (($x1202 (or l2ia $x220)))
|
||||||
|
(let (($x186 (= $x1202 true)))
|
||||||
|
(let (($x1297 (bvule l2b la2e)))
|
||||||
|
(let (($x805 (or l2ia $x1297)))
|
||||||
|
(let (($x372 (= $x805 true)))
|
||||||
|
(let ((?x815 (bvadd (_ bv4294967295 32) l1b)))
|
||||||
|
(let ((?x1126 (bvadd ?x815 d4)))
|
||||||
|
(let (($x493 (bvule ?x1126 la14)))
|
||||||
|
(let (($x384 (or l1ia $x493)))
|
||||||
|
(let (($x1335 (= $x384 true)))
|
||||||
|
(let (($x1024 (bvule r44 l1b)))
|
||||||
|
(let (($x736 (or l1ia $x1024)))
|
||||||
|
(let (($x789 (= $x736 true)))
|
||||||
|
(let ((?x922 (select id.m6 l1=/_begin)))
|
||||||
|
(let ((?x747 (bvadd l1=/_begin (_ bv1 32))))
|
||||||
|
(let ((?x119 (select id.m6 ?x747)))
|
||||||
|
(let ((?x322 (bvadd l1=/_begin (_ bv2 32))))
|
||||||
|
(let ((?x1270 (select id.m6 ?x322)))
|
||||||
|
(let ((?x374 (bvadd l1=/_begin (_ bv3 32))))
|
||||||
|
(let ((?x534 (select id.m6 ?x374)))
|
||||||
|
(let ((?x562 (select m.Lfc.1=/ l1=/_begin)))
|
||||||
|
(let ((?x537 (select m.Lfc.1=/ ?x747)))
|
||||||
|
(let ((?x1089 (select m.Lfc.1=/ ?x322)))
|
||||||
|
(let ((?x1161 (select m.Lfc.1=/ ?x374)))
|
||||||
|
(let (($x109 (= (concat ?x1161 (concat ?x1089 (concat ?x537 ?x562))) (concat ?x534 (concat ?x1270 (concat ?x119 ?x922))))))
|
||||||
|
(let (($x779 (and true $x109)))
|
||||||
|
(let (($x300 (= $x779 true)))
|
||||||
|
(let (($x1197 (bvult l3e sp2)))
|
||||||
|
(let (($x494 (or l3ia $x1197)))
|
||||||
|
(let (($x1258 (= $x494 true)))
|
||||||
|
(let ((?x1080 (bvmul (_ bv4294967295 32) d3ls)))
|
||||||
|
(let ((?x496 (bvadd l3b ?x1080)))
|
||||||
|
(let (($x711 (bvule r44 ?x496)))
|
||||||
|
(let (($x151 (or l3ia $x711)))
|
||||||
|
(let (($x396 (= $x151 true)))
|
||||||
|
(let (($x985 (forall ((icm-bounded-var! (_ BitVec 32)) )(let (($x1009 (bvule icm-bounded-var! l3e)))
|
||||||
|
(let (($x81 (bvule l3b icm-bounded-var!)))
|
||||||
|
(= (and $x81 $x1009) (= (select ma.LEA icm-bounded-var!) (_ bv3 8))))))
|
||||||
|
))
|
||||||
|
(let (($x888 (xor l3ia $x985)))
|
||||||
|
(let (($x570 (= $x888 true)))
|
||||||
|
(let ((?x110 (select id.m6 l0=/_begin)))
|
||||||
|
(let ((?x457 (bvadd l0=/_begin (_ bv1 32))))
|
||||||
|
(let ((?x159 (select id.m6 ?x457)))
|
||||||
|
(let ((?x684 (bvadd l0=/_begin (_ bv2 32))))
|
||||||
|
(let ((?x247 (select id.m6 ?x684)))
|
||||||
|
(let ((?x639 (select id.m6 ?x447)))
|
||||||
|
(let ((?x83 (select m.Lfc.0=/ l0=/_begin)))
|
||||||
|
(let ((?x206 (select m.Lfc.0=/ ?x457)))
|
||||||
|
(let ((?x643 (select m.Lfc.0=/ ?x684)))
|
||||||
|
(let ((?x342 (select m.Lfc.0=/ ?x447)))
|
||||||
|
(let (($x1173 (= (concat ?x342 (concat ?x643 (concat ?x206 ?x83))) (concat ?x639 (concat ?x247 (concat ?x159 ?x110))))))
|
||||||
|
(let (($x872 (and true $x1173)))
|
||||||
|
(let (($x1025 (= $x872 true)))
|
||||||
|
(let (($x1261 (= l3e ?x327)))
|
||||||
|
(let (($x837 (or l3ia $x1261)))
|
||||||
|
(let (($x1027 (= $x837 true)))
|
||||||
|
(let (($x200 (= la2e ?x359)))
|
||||||
|
(let (($x348 (or l2ia $x200)))
|
||||||
|
(let (($x102 (= $x348 true)))
|
||||||
|
(let (($x635 (= la14 ?x1126)))
|
||||||
|
(let (($x165 (or l1ia $x635)))
|
||||||
|
(let (($x279 (= $x165 true)))
|
||||||
|
(let (($x475 (bvule l3b l3e)))
|
||||||
|
(let (($x115 (or l3ia $x475)))
|
||||||
|
(let (($x649 (= $x115 true)))
|
||||||
|
(let (($x204 (not l2ia)))
|
||||||
|
(let (($x840 (= $x204 true)))
|
||||||
|
(let (($x104 (= (_ bv0 32) d4)))
|
||||||
|
(let (($x1236 (not $x104)))
|
||||||
|
(let (($x98 (or l1ia $x1236)))
|
||||||
|
(let (($x85 (= $x98 true)))
|
||||||
|
(let (($x904 (= $x551 true)))
|
||||||
|
(let (($x960 (= l1b d1b4)))
|
||||||
|
(let (($x1273 (or l1ia $x960)))
|
||||||
|
(let (($x714 (= $x1273 true)))
|
||||||
|
(let (($x382 (not l3ia)))
|
||||||
|
(let (($x1018 (= $x382 true)))
|
||||||
|
(let (($x51 (= l3ls d3ls)))
|
||||||
|
(let (($x1190 (or l3ia $x51)))
|
||||||
|
(let (($x939 (= $x1190 true)))
|
||||||
|
(let (($x1278 (= (_ bv0 32) d2ls)))
|
||||||
|
(let (($x573 (not $x1278)))
|
||||||
|
(let (($x664 (or l2ia $x573)))
|
||||||
|
(let (($x1119 (= $x664 true)))
|
||||||
|
(let (($x931 (forall ((mia-bounded-var! (_ BitVec 32)) )(let ((?x799 (select ma.LEA mia-bounded-var!)))
|
||||||
|
(and (distinct ?x799 (_ bv1 8)) true)))
|
||||||
|
))
|
||||||
|
(let (($x891 (= l2ia $x931)))
|
||||||
|
(let (($x848 (= $x891 true)))
|
||||||
|
(let (($x607 (or l2ia true)))
|
||||||
|
(let (($x404 (= $x607 true)))
|
||||||
|
(let (($x1205 (forall ((mae-bounded-var! (_ BitVec 32)) )(let ((?x1098 (select id.m6 mae-bounded-var!)))
|
||||||
|
(let ((?x429 (select m.Lfc.3%d=/ mae-bounded-var!)))
|
||||||
|
(let ((?x459 (select ma.LEA (bvadd mae-bounded-var! (_ bv0 32)))))
|
||||||
|
(let (($x663 (and (distinct (_ bv1 32) (_ bv0 32)) true)))
|
||||||
|
(let (($x1290 (and $x663 (bvule mae-bounded-var! (bvsub (bvadd mae-bounded-var! (_ bv1 32)) (_ bv1 32))))))
|
||||||
|
(=> (and $x1290 (= ?x459 (_ bv3 8))) (= ?x429 ?x1098))))))))
|
||||||
|
))
|
||||||
|
(let (($x113 (and true $x1205)))
|
||||||
|
(let (($x793 (= $x113 true)))
|
||||||
|
(let (($x553 (not l1ia)))
|
||||||
|
(let (($x1005 (= $x553 true)))
|
||||||
|
(let (($x538 (= (_ bv1024 32) d2ls)))
|
||||||
|
(let (($x847 (= b b)))
|
||||||
|
(let (($x164 (bvult la14 sp2)))
|
||||||
|
(let (($x18 (or l1ia $x164)))
|
||||||
|
(let (($x285 (= $x18 true)))
|
||||||
|
(let (($x889 (bvsge i (_ bv0 32))))
|
||||||
|
(let (($x659 (= $x889 true)))
|
||||||
|
(let (($x566 (bvule i (_ bv255 32))))
|
||||||
|
(let (($x721 (= $x566 true)))
|
||||||
|
(let ((?x695 (bvadd sp3 (_ bv16 32))))
|
||||||
|
(let (($x839 (= dl1b ?x695)))
|
||||||
|
(let (($x442 (bvugt dl1b sp3)))
|
||||||
|
(let (($x1235 (= $x442 true)))
|
||||||
|
(let (($x583 (bvuge dl1b sp3)))
|
||||||
|
(let (($x92 (= $x583 true)))
|
||||||
|
(let (($x377 (bvuge dl1e sp3)))
|
||||||
|
(let (($x203 (= $x377 true)))
|
||||||
|
(let ((?x1325 (bvadd sp3 (_ bv1296 32))))
|
||||||
|
(let (($x1228 (= dl3b ?x1325)))
|
||||||
|
(let (($x1037 (bvugt dl3b sp3)))
|
||||||
|
(let (($x638 (= $x1037 true)))
|
||||||
|
(let (($x1022 (bvuge dl3b sp3)))
|
||||||
|
(let (($x100 (= $x1022 true)))
|
||||||
|
(let (($x141 (bvuge dl3e sp3)))
|
||||||
|
(let (($x131 (= $x141 true)))
|
||||||
|
(let (($x581 (and $x840 $x1005)))
|
||||||
|
(let (($x169 (and $x581 $x1018)))
|
||||||
|
(let (($x776 (and $x169 $x131)))
|
||||||
|
(let (($x1296 (and $x776 $x100)))
|
||||||
|
(let (($x832 (and $x1296 $x638)))
|
||||||
|
(let (($x1267 (and $x832 $x1228)))
|
||||||
|
(let (($x181 (and $x1267 $x203)))
|
||||||
|
(let (($x507 (and $x181 $x92)))
|
||||||
|
(let (($x842 (and $x507 $x1235)))
|
||||||
|
(let (($x59 (and $x842 $x839)))
|
||||||
|
(let (($x988 (and $x59 $x721)))
|
||||||
|
(let (($x1249 (and $x988 $x659)))
|
||||||
|
(let (($x1099 (and $x1249 $x285)))
|
||||||
|
(let (($x1225 (and $x1099 $x538)))
|
||||||
|
(let (($x977 (and $x1225 $x1005)))
|
||||||
|
(let (($x298 (and $x977 $x793)))
|
||||||
|
(let (($x175 (and $x298 $x404)))
|
||||||
|
(let (($x58 (and $x175 $x848)))
|
||||||
|
(let (($x491 (and $x58 $x1119)))
|
||||||
|
(let (($x972 (and $x491 $x939)))
|
||||||
|
(let (($x624 (and $x972 $x1018)))
|
||||||
|
(let (($x923 (and $x624 $x714)))
|
||||||
|
(let (($x1306 (and $x923 $x904)))
|
||||||
|
(let (($x49 (and $x1306 $x85)))
|
||||||
|
(let (($x996 (and $x49 $x840)))
|
||||||
|
(let (($x845 (and $x996 $x649)))
|
||||||
|
(let (($x358 (and $x845 $x279)))
|
||||||
|
(let (($x777 (and $x358 $x102)))
|
||||||
|
(let (($x347 (and $x777 $x1027)))
|
||||||
|
(let (($x456 (and $x347 $x1025)))
|
||||||
|
(let (($x1255 (and $x456 $x570)))
|
||||||
|
(let (($x142 (and $x1255 $x396)))
|
||||||
|
(let (($x353 (and $x142 $x1258)))
|
||||||
|
(let (($x215 (and $x353 $x300)))
|
||||||
|
(let (($x114 (and $x215 $x789)))
|
||||||
|
(let (($x1016 (and $x114 $x1335)))
|
||||||
|
(let (($x140 (and $x1016 $x372)))
|
||||||
|
(let (($x281 (and $x140 $x186)))
|
||||||
|
(let (($x64 (and $x281 $x909)))
|
||||||
|
(let (($x820 (and $x64 $x1317)))
|
||||||
|
(let (($x461 (and $x820 $x892)))
|
||||||
|
(let (($x1231 (and $x461 $x202)))
|
||||||
|
(let (($x70 (and $x1231 $x720)))
|
||||||
|
(let (($x933 (and $x70 $x91)))
|
||||||
|
(let (($x481 (and $x933 $x187)))
|
||||||
|
(let (($x1308 (and $x481 $x1140)))
|
||||||
|
(let (($x124 (and $x1308 $x1193)))
|
||||||
|
(let (($x221 (and $x124 $x128)))
|
||||||
|
(let (($x611 (and $x221 $x875)))
|
||||||
|
(let (($x803 (and $x611 $x1168)))
|
||||||
|
(let (($x103 (and $x803 $x935)))
|
||||||
|
(let (($x145 (and $x103 $x1031)))
|
||||||
|
(let (($x871 (and $x145 $x703)))
|
||||||
|
(let (($x258 (and $x871 $x149)))
|
||||||
|
(let (($x1060 (and $x258 $x1242)))
|
||||||
|
(let (($x344 (and $x1060 $x744)))
|
||||||
|
(let (($x1003 (and $x344 $x762)))
|
||||||
|
(let (($x733 (and $x1003 $x1062)))
|
||||||
|
(let (($x817 (and $x733 $x1139)))
|
||||||
|
(let (($x645 (and $x817 $x332)))
|
||||||
|
(let (($x690 (and $x645 $x422)))
|
||||||
|
(let (($x336 (and $x690 $x755)))
|
||||||
|
(let (($x154 (and $x336 $x355)))
|
||||||
|
(let (($x1004 (and $x154 $x318)))
|
||||||
|
(let (($x582 (and $x1004 $x304)))
|
||||||
|
(let (($x1214 (and $x582 $x877)))
|
||||||
|
(let (($x770 (and $x1214 $x166)))
|
||||||
|
(let (($x1078 (and $x770 $x129)))
|
||||||
|
(let (($x14 (and $x1078 $x1276)))
|
||||||
|
(let (($x769 (and $x14 $x976)))
|
||||||
|
(let (($x1253 (and $x769 $x835)))
|
||||||
|
(let (($x699 (and $x1253 $x410)))
|
||||||
|
(let (($x1108 (and $x699 $x84)))
|
||||||
|
(let (($x818 (and $x1108 $x289)))
|
||||||
|
(let (($x331 (and $x818 $x227)))
|
||||||
|
(let (($x804 (and $x331 $x788)))
|
||||||
|
(let (($x1224 (and $x804 $x841)))
|
||||||
|
(let (($x1032 (and $x1224 $x1341)))
|
||||||
|
(let (($x628 (and $x1032 $x531)))
|
||||||
|
(let (($x80 (and $x628 $x588)))
|
||||||
|
(let (($x1093 (and $x80 $x1219)))
|
||||||
|
(let (($x866 (and $x1093 $x887)))
|
||||||
|
(let (($x1287 (and $x866 $x825)))
|
||||||
|
(let (($x1226 (and $x1287 $x731)))
|
||||||
|
(let (($x11 (and $x1226 $x677)))
|
||||||
|
(let (($x184 (and $x11 $x477)))
|
||||||
|
(let (($x47 (and $x184 $x1307)))
|
||||||
|
(let (($x1002 (and $x47 $x240)))
|
||||||
|
(let (($x556 (and $x1002 $x849)))
|
||||||
|
(let (($x969 (and $x556 $x6)))
|
||||||
|
(let (($x896 (and $x969 $x1050)))
|
||||||
|
(let (($x1040 (and $x896 $x1194)))
|
||||||
|
(let (($x688 (and $x1040 $x895)))
|
||||||
|
(let (($x1332 (and $x688 $x968)))
|
||||||
|
(let (($x868 (and $x1332 $x825)))
|
||||||
|
(let (($x797 (and $x868 $x499)))
|
||||||
|
(let (($x61 (and $x797 $x167)))
|
||||||
|
(let (($x967 (and $x61 $x57)))
|
||||||
|
(let (($x937 (and $x967 $x806)))
|
||||||
|
(let (($x246 (and $x937 $x623)))
|
||||||
|
(let (($x24 (and $x246 $x277)))
|
||||||
|
(let (($x192 (and $x24 $x168)))
|
||||||
|
(let (($x400 (and $x192 $x513)))
|
||||||
|
(let (($x1111 (and $x400 $x938)))
|
||||||
|
(let (($x957 (and $x1111 $x524)))
|
||||||
|
(let (($x257 (and $x957 $x234)))
|
||||||
|
(let (($x144 (and $x257 $x1014)))
|
||||||
|
(let (($x402 (and $x144 $x1265)))
|
||||||
|
(let (($x657 (and $x402 $x567)))
|
||||||
|
(let (($x243 (and $x657 $x287)))
|
||||||
|
(let (($x79 (and $x243 $x599)))
|
||||||
|
(let (($x547 (and $x79 $x764)))
|
||||||
|
(let (($x705 (and $x547 $x271)))
|
||||||
|
(let (($x948 (and $x705 $x449)))
|
||||||
|
(let (($x273 (and $x948 $x995)))
|
||||||
|
(let (($x156 (and $x273 $x120)))
|
||||||
|
(let (($x1010 (and $x156 $x339)))
|
||||||
|
(let (($x908 (and $x1010 $x986)))
|
||||||
|
(let (($x1153 (and $x908 $x1081)))
|
||||||
|
(let (($x959 (and $x1153 $x1049)))
|
||||||
|
(let (($x710 (and $x959 $x653)))
|
||||||
|
(let (($x297 (and $x710 $x852)))
|
||||||
|
(let (($x161 (and $x297 $x682)))
|
||||||
|
(let (($x487 (and $x161 $x541)))
|
||||||
|
(let (($x516 (and $x551 $x487)))
|
||||||
|
(let (($x272 (and $x1081 $x516)))
|
||||||
|
(let (($x730 (= (select id.ma (bvadd ?x693 (_ bv0 32))) (_ bv7 8))))
|
||||||
|
(let (($x1058 (= (select id.ma (bvadd ?x693 (_ bv0 32))) (_ bv5 8))))
|
||||||
|
(let (($x1043 (= (select id.ma (bvadd ?x693 (_ bv0 32))) (_ bv4 8))))
|
||||||
|
(let (($x260 (= (select id.ma (bvadd ?x693 (_ bv0 32))) (_ bv3 8))))
|
||||||
|
(let (($x261 (= (select id.ma (bvadd ?x693 (_ bv0 32))) (_ bv2 8))))
|
||||||
|
(let (($x942 (= (select id.ma (bvadd ?x834 (_ bv0 32))) (_ bv7 8))))
|
||||||
|
(let (($x1035 (= (select id.ma (bvadd ?x834 (_ bv0 32))) (_ bv5 8))))
|
||||||
|
(let (($x413 (= (select id.ma (bvadd ?x834 (_ bv0 32))) (_ bv4 8))))
|
||||||
|
(let (($x1199 (= (select id.ma (bvadd ?x834 (_ bv0 32))) (_ bv3 8))))
|
||||||
|
(let (($x864 (= (select id.ma (bvadd ?x834 (_ bv0 32))) (_ bv2 8))))
|
||||||
|
(let (($x208 (= (select id.ma (bvadd ?x328 (_ bv0 32))) (_ bv7 8))))
|
||||||
|
(let (($x388 (= (select id.ma (bvadd ?x328 (_ bv0 32))) (_ bv5 8))))
|
||||||
|
(let (($x163 (= (select id.ma (bvadd ?x328 (_ bv0 32))) (_ bv4 8))))
|
||||||
|
(let (($x1175 (= (select id.ma (bvadd ?x328 (_ bv0 32))) (_ bv3 8))))
|
||||||
|
(let (($x36 (= (select id.ma (bvadd ?x328 (_ bv0 32))) (_ bv2 8))))
|
||||||
|
(let (($x1154 (= (select id.ma (bvadd ?x222 (_ bv0 32))) (_ bv7 8))))
|
||||||
|
(let (($x340 (= (select id.ma (bvadd ?x222 (_ bv0 32))) (_ bv5 8))))
|
||||||
|
(let (($x1122 (= (select id.ma (bvadd ?x222 (_ bv0 32))) (_ bv4 8))))
|
||||||
|
(let (($x865 (= (select id.ma (bvadd ?x222 (_ bv0 32))) (_ bv3 8))))
|
||||||
|
(let (($x814 (= (select id.ma (bvadd ?x222 (_ bv0 32))) (_ bv2 8))))
|
||||||
|
(let (($x134 (or (or (or (or $x814 $x865) $x1122) $x340) $x1154)))
|
||||||
|
(let (($x1159 (and $x134 (or (or (or (or $x36 $x1175) $x163) $x388) $x208))))
|
||||||
|
(let (($x691 (and $x1159 (or (or (or (or $x864 $x1199) $x413) $x1035) $x942))))
|
||||||
|
(let (($x1096 (and $x691 (or (or (or (or $x261 $x260) $x1043) $x1058) $x730))))
|
||||||
|
(let (($x1180 (and (bvule ?x824 (bvsub (bvadd ?x824 (_ bv4 32)) (_ bv1 32))) $x1096)))
|
||||||
|
(let ((sel.id.ma.3 (select id.ma (bvadd (bvadd r1 r0x4) (_ bv3 32)))))
|
||||||
|
(let ((sel.id.ma.3.68 (or (= sel.id.ma.3 (_ bv6 8)) (= sel.id.ma.3 (_ bv8 8)))))
|
||||||
|
(let ((sel.id.ma.2 (select id.ma (bvadd (bvadd r1 r0x4) (_ bv2 32)))))
|
||||||
|
(let ((sel.id.ma.2.68 (or (= sel.id.ma.2 (_ bv6 8)) (= sel.id.ma.2 (_ bv8 8)))))
|
||||||
|
(let ((sel.id.ma.1 (select id.ma (bvadd (bvadd r1 r0x4) (_ bv1 32)))))
|
||||||
|
(let ((sel.id.ma.1.68 (or (= sel.id.ma.1 (_ bv6 8)) (= sel.id.ma.1 (_ bv8 8)))))
|
||||||
|
(let ((sel.id.ma.0 (select id.ma (bvadd (bvadd r1 r0x4) (_ bv0 32)))))
|
||||||
|
(let ((sel.id.ma.0.68 (or (= sel.id.ma.0 (_ bv6 8)) (= sel.id.ma.0 (_ bv8 8)))))
|
||||||
|
(let ((?x675 (bvadd r1 r0x4)))
|
||||||
|
(let ((id.ma.assert (and (bvule ?x675 (bvsub (bvadd ?x675 (_ bv4 32)) (_ bv1 32))) (and (and (and sel.id.ma.0.68 sel.id.ma.1.68) sel.id.ma.2.68) sel.id.ma.3.68)))) ; <-- assertion over id.ma
|
||||||
|
(let (($x1277 (bvule ?x1146 (bvsub (bvadd ?x1146 (_ bv4 32)) (_ bv1 32)))))
|
||||||
|
(let (($x408 (= $x1277 true)))
|
||||||
|
(let (($x702 (=> $x551 $x408)))
|
||||||
|
(let (($x760 (bvule ?x828 (bvsub (bvadd ?x828 (_ bv4 32)) (_ bv1 32)))))
|
||||||
|
(let (($x63 (= $x760 true)))
|
||||||
|
(let (($x879 (=> $x551 $x63)))
|
||||||
|
(let (($x1213 (and $x879 $x702)))
|
||||||
|
(let (($x1274 (and $x1213 id.ma.assert)))
|
||||||
|
(let (($x1069 (and $x1274 $x1180)))
|
||||||
|
(let (($x89 (and $x1069 $x272)))
|
||||||
|
(let (($x484 (=> $x89 false)))
|
||||||
|
(not $x484)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
||||||
|
(check-sat)
|
||||||
|
(get-model)
|
||||||
|
|
@ -4,6 +4,9 @@ Copyright (c) 2025 Microsoft Corporation
|
||||||
|
|
||||||
#include "api/z3.h"
|
#include "api/z3.h"
|
||||||
#include "util/util.h"
|
#include "util/util.h"
|
||||||
|
#include <fstream>
|
||||||
|
#include <sstream>
|
||||||
|
#include <stdexcept>
|
||||||
#include <string>
|
#include <string>
|
||||||
|
|
||||||
// x mod 7 = 0 & (x*y) mod 7 != 0 should be unsat
|
// x mod 7 = 0 & (x*y) mod 7 != 0 should be unsat
|
||||||
|
|
@ -84,8 +87,52 @@ static void test_const_array_store_chain_unsat() {
|
||||||
Z3_del_context(ctx);
|
Z3_del_context(ctx);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
static std::string read_sibling_file(char const* current_file, char const* sibling) {
|
||||||
|
std::string path = current_file;
|
||||||
|
size_t pos = path.find_last_of("/\\");
|
||||||
|
ENSURE(pos != std::string::npos);
|
||||||
|
path.resize(pos + 1);
|
||||||
|
path += sibling;
|
||||||
|
std::ifstream in(path);
|
||||||
|
if (!in.good())
|
||||||
|
throw std::runtime_error("failed to open test file: " + path);
|
||||||
|
std::ostringstream out;
|
||||||
|
out << in.rdbuf();
|
||||||
|
return out.str();
|
||||||
|
}
|
||||||
|
|
||||||
|
static void test_abv_model_roundtrip_issue_7132() {
|
||||||
|
Z3_config cfg = Z3_mk_config();
|
||||||
|
Z3_context ctx = Z3_mk_context(cfg);
|
||||||
|
|
||||||
|
std::string benchmark = read_sibling_file(__FILE__, "issue_7132.smt2");
|
||||||
|
size_t tail = benchmark.rfind("(check-sat)");
|
||||||
|
ENSURE(tail != std::string::npos);
|
||||||
|
benchmark.resize(tail);
|
||||||
|
benchmark += R"(
|
||||||
|
(check-sat)
|
||||||
|
(get-value ((select id.ma (bvadd r1 (bvmul #x00000004 r0)))))
|
||||||
|
(get-value ((select id.ma (bvadd r1 (bvmul #x00000004 r0) #x00000001))))
|
||||||
|
(get-value ((select id.ma (bvadd r1 (bvmul #x00000004 r0) #x00000002))))
|
||||||
|
(get-value ((select id.ma (bvadd r1 (bvmul #x00000004 r0) #x00000003))))
|
||||||
|
)";
|
||||||
|
|
||||||
|
std::string resp = Z3_eval_smtlib2_string(ctx, benchmark.c_str());
|
||||||
|
std::istringstream in(resp);
|
||||||
|
std::string line;
|
||||||
|
ENSURE(static_cast<bool>(std::getline(in, line)));
|
||||||
|
ENSURE(line == "sat");
|
||||||
|
for (unsigned i = 0; i < 4; ++i) {
|
||||||
|
ENSURE(static_cast<bool>(std::getline(in, line)));
|
||||||
|
ENSURE(line.find("#x06") != std::string::npos || line.find("#x08") != std::string::npos);
|
||||||
|
}
|
||||||
|
Z3_del_config(cfg);
|
||||||
|
Z3_del_context(ctx);
|
||||||
|
}
|
||||||
|
|
||||||
void tst_mod_factor() {
|
void tst_mod_factor() {
|
||||||
test_mod_factor_mod_path();
|
test_mod_factor_mod_path();
|
||||||
test_mod_factor_idiv_path();
|
test_mod_factor_idiv_path();
|
||||||
test_const_array_store_chain_unsat();
|
test_const_array_store_chain_unsat();
|
||||||
|
test_abv_model_roundtrip_issue_7132();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue