| # RUN: %kleaver -print-smtlib %s > %t1.smt2 |
| # RUN: diff %t1.smt2 %p/print-smt.smt2.good |
| # Query 0 -- Type: InitialValues, Instructions: 27 |
| (query [] false) |
| |
| # Query 1 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13) [] |
| [unnamed_1]) |
| |
| # Query 2 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 16) [] |
| [unnamed_1]) |
| |
| # Query 3 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ule 51630448 |
| (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))))) [] |
| [unnamed_1]) |
| |
| # Query 4 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 30832 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 3)) [] |
| [unnamed_1]) |
| |
| # Query 5 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ule 51599616 |
| (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))))) [] |
| [unnamed_1]) |
| |
| # Query 6 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 31312 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 4)) [] |
| [unnamed_1]) |
| |
| # Query 7 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ule 51599136 |
| (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))))) [] |
| [unnamed_1]) |
| |
| # Query 8 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 31760 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 16)) [] |
| [unnamed_1]) |
| |
| # Query 9 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ule 51598688 |
| (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))))) [] |
| [unnamed_1]) |
| |
| # Query 10 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 111120 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 4)) [] |
| [unnamed_1]) |
| |
| # Query 11 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ule 51519328 |
| (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))))) [] |
| [unnamed_1]) |
| |
| # Query 12 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 51648704) [] |
| [unnamed_1]) |
| |
| # Query 13 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446744073709533360 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 4)) [] |
| [unnamed_1]) |
| |
| # Query 14 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 51648736) [] |
| [unnamed_1]) |
| |
| # Query 15 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446744073709533328 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 4)) [] |
| [unnamed_1]) |
| |
| # Query 16 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 51649264) [] |
| [unnamed_1]) |
| |
| # Query 17 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446744073709532800 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 4)) [] |
| [unnamed_1]) |
| |
| # Query 18 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 140298479681184) [] |
| [unnamed_1]) |
| |
| # Query 19 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446603775281500880 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 1536)) [] |
| [unnamed_1]) |
| |
| # Query 20 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 140298479682720) [] |
| [unnamed_1]) |
| |
| # Query 21 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446603775281499344 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 1536)) [] |
| [unnamed_1]) |
| |
| # Query 22 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 140298479685280) [] |
| [unnamed_1]) |
| |
| # Query 23 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446603775281496784 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 768)) [] |
| [unnamed_1]) |
| |
| # Query 24 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 140298496902856) [] |
| [unnamed_1]) |
| |
| # Query 25 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446603775264279208 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 4)) [] |
| [unnamed_1]) |
| |
| # Query 26 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 140298496902864) [] |
| [unnamed_1]) |
| |
| # Query 27 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446603775264279200 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 8)) [] |
| [unnamed_1]) |
| |
| # Query 28 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 140298496902872) [] |
| [unnamed_1]) |
| |
| # Query 29 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446603775264279192 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 8)) [] |
| [unnamed_1]) |
| |
| # Query 30 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Ult (Add w64 51630448 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 140298496902880) [] |
| [unnamed_1]) |
| |
| # Query 31 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [] (Eq false |
| (Ult (Add w64 18446603775264279184 |
| (Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1)))) |
| 8)) [] |
| [unnamed_1]) |
| |
| # Query 32 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13))] |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) [] |
| [unnamed_1]) |
| |
| # Query 33 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1))] |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) [] |
| [unnamed_1]) |
| |
| # Query 34 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13))] |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) [] |
| [unnamed_1]) |
| |
| # Query 35 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1))] |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) [] |
| [unnamed_1]) |
| |
| # Query 36 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1))] |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) [] |
| [unnamed_1]) |
| |
| # Query 37 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1))] |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1)) [] |
| [unnamed_1]) |
| |
| # Query 38 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Eq false (Eq 18446744073657921168 N0)) [] |
| [unnamed_1]) |
| |
| # Query 39 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744069414584319) [] |
| [unnamed_1]) |
| |
| # Query 40 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744071562067967) [] |
| [unnamed_1]) |
| |
| # Query 41 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744072635809791) [] |
| [unnamed_1]) |
| |
| # Query 42 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073172680703) [] |
| [unnamed_1]) |
| |
| # Query 43 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073441116159) [] |
| [unnamed_1]) |
| |
| # Query 44 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073575333887) [] |
| [unnamed_1]) |
| |
| # Query 45 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073642442751) [] |
| [unnamed_1]) |
| |
| # Query 46 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073675997183) [] |
| [unnamed_1]) |
| |
| # Query 47 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073692774399) [] |
| [unnamed_1]) |
| |
| # Query 48 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073701163007) [] |
| [unnamed_1]) |
| |
| # Query 49 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073705357311) [] |
| [unnamed_1]) |
| |
| # Query 50 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073707454463) [] |
| [unnamed_1]) |
| |
| # Query 51 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073708503039) [] |
| [unnamed_1]) |
| |
| # Query 52 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709027327) [] |
| [unnamed_1]) |
| |
| # Query 53 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709289471) [] |
| [unnamed_1]) |
| |
| # Query 54 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709420543) [] |
| [unnamed_1]) |
| |
| # Query 55 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709486079) [] |
| [unnamed_1]) |
| |
| # Query 56 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709518847) [] |
| [unnamed_1]) |
| |
| # Query 57 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709535231) [] |
| [unnamed_1]) |
| |
| # Query 58 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709543423) [] |
| [unnamed_1]) |
| |
| # Query 59 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709547519) [] |
| [unnamed_1]) |
| |
| # Query 60 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709549567) [] |
| [unnamed_1]) |
| |
| # Query 61 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709550591) [] |
| [unnamed_1]) |
| |
| # Query 62 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551103) [] |
| [unnamed_1]) |
| |
| # Query 63 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551359) [] |
| [unnamed_1]) |
| |
| # Query 64 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551487) [] |
| [unnamed_1]) |
| |
| # Query 65 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551551) [] |
| [unnamed_1]) |
| |
| # Query 66 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551583) [] |
| [unnamed_1]) |
| |
| # Query 67 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551599) [] |
| [unnamed_1]) |
| |
| # Query 68 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551607) [] |
| [unnamed_1]) |
| |
| # Query 69 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551611) [] |
| [unnamed_1]) |
| |
| # Query 70 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551613) [] |
| [unnamed_1]) |
| |
| # Query 71 -- Type: InitialValues, Instructions: 27 |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709532800 N0) 1))] |
| (Ule (Add w64 51630448 N0) 18446744073709551612) [] |
| [unnamed_1]) |
| |
| # Query 72 -- Type: InitialValues, Instructions: 30 |
| array const_arr2[4] : w32 -> w8 = [121 101 115 0] |
| array unnamed[4] : w32 -> w8 = symbolic |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Ult N1:(Add w64 31312 N0) 1)] |
| (Eq false |
| (Eq (ReadLSB w32 0 unnamed) |
| (ReadLSB w32 N2:(Extract w32 0 N1) const_arr2))) [] |
| [unnamed |
| unnamed_1]) |
| |
| # Query 73 -- Type: InitialValues, Instructions: 31 |
| array unnamed[4] : w32 -> w8 = symbolic |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Ult N1:(Add w64 18446744073709533360 N0) 1)] |
| (Eq (ReadLSB w32 0 unnamed) |
| (ReadLSB w32 N2:(Extract w32 0 N1) unnamed)) [] |
| [unnamed_1 |
| unnamed]) |
| |
| # Query 74 -- Type: InitialValues, Instructions: 37 |
| array unnamed[4] : w32 -> w8 = symbolic |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| array const_arr5[4] : w32 -> w8 = [171 171 171 171] |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Ult N1:(Add w64 18446744073709533328 N0) 1)] |
| (Eq false |
| (Eq (ReadLSB w32 0 unnamed) |
| (ReadLSB w32 N2:(Extract w32 0 N1) const_arr5))) [] |
| [unnamed_1 |
| unnamed]) |
| |
| # Query 75 -- Type: InitialValues, Instructions: 40 |
| array unnamed[4] : w32 -> w8 = symbolic |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| array const_arr1[16] : w32 -> w8 = [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0] |
| (query [(Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)] |
| (Eq false |
| (Eq (ReadLSB w32 0 unnamed) |
| (ReadLSB w32 N1:(Extract w32 0 N0) const_arr1))) [] |
| [unnamed |
| unnamed_1]) |
| |
| # Query 76 -- Type: InitialValues, Instructions: 50 |
| array unnamed[4] : w32 -> w8 = symbolic |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| array const_arr4[4] : w32 -> w8 = [171 171 171 171] |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Ult N1:(Add w64 111120 N0) 1)] |
| (Eq false |
| (Eq (ReadLSB w32 0 unnamed) |
| (ReadLSB w32 N2:(Extract w32 0 N1) const_arr4))) [] |
| [unnamed_1 |
| unnamed]) |
| |
| # Query 77 -- Type: InitialValues, Instructions: 51 |
| array unnamed[4] : w32 -> w8 = symbolic |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| array const_arr3[16] : w32 -> w8 = [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0] |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Ult N1:(Add w64 31760 N0) 13)] |
| (Eq false |
| (Eq (ReadLSB w32 0 unnamed) |
| (ReadLSB w32 N2:(Extract w32 0 N1) const_arr3))) [] |
| [unnamed |
| unnamed_1]) |
| |
| # Query 78 -- Type: InitialValues, Instructions: 96 |
| array unnamed[4] : w32 -> w8 = symbolic |
| array unnamed_1[4] : w32 -> w8 = symbolic |
| (query [(Eq false |
| (Ult N0:(Mul w64 4 |
| (SExt w64 (ReadLSB w32 0 unnamed_1))) |
| 13)) |
| (Eq false |
| (Ult (Add w64 31312 N0) 1)) |
| (Eq false |
| (Ult (Add w64 31760 N0) 13)) |
| (Eq false |
| (Ult (Add w64 111120 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533360 N0) 1)) |
| (Eq false |
| (Ult (Add w64 18446744073709533328 N0) 1)) |
| (Ult N1:(Add w64 18446744073709532800 N0) 1)] |
| (Eq false |
| (Eq (ReadLSB w32 0 unnamed) |
| (ReadLSB w32 N2:(Extract w32 0 N1) unnamed_1))) [] |
| [unnamed_1 |
| unnamed]) |
| |