Skip to content

Commit

Permalink
fix btor2 models
Browse files Browse the repository at this point in the history
  • Loading branch information
abolotina committed Nov 24, 2023
1 parent d55abc8 commit 311051e
Show file tree
Hide file tree
Showing 35 changed files with 2,285 additions and 2,240 deletions.
166 changes: 83 additions & 83 deletions lion/benchmarks/insertion-sort-il9.btor2

Large diffs are not rendered by default.

140 changes: 70 additions & 70 deletions lion/benchmarks/microbenchmark-il0.btor2
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
61 init 1 60 20
62 state 1 terminate-mode
63 init 1 62 20
64 not 1 1 60
64 not 1 60

; 32 64-bit general-purpose registers

Expand Down Expand Up @@ -570,14 +570,14 @@
36578401 ite 2 16578400 36578400 36574001
36578800 ite 1 16578800 21 36574400
36579200 eq 1 220 212
36579201 not 1 1 36579200
36579201 not 1 36579200
36579600 eq 1 200 200
36579601 not 1 1 36579600
36579601 not 1 36579600
36580000 eq 1 200 210
36580001 not 1 1 36580000
36580001 not 1 36580000
36580400 ite 2 16580400 200 36578001
36580800 eq 1 200 200
36580801 not 1 1 36580800
36580801 not 1 36580800
36581200 constd 2 18446744073709551608
36581201 add 2 206 36581200
36581202 ite 2 16581200 36581201 36577602
Expand Down Expand Up @@ -714,7 +714,7 @@
36600001 uext 2 36600000 63
36600002 ite 2 16600000 36600001 36599204
36600400 eq 1 210 200
36600401 not 1 1 36600400
36600401 not 1 36600400
36600800 constd 2 18446744073709551600
36600801 add 2 216 36600800
36600802 ite 2 16600800 36600801 36599202
Expand Down Expand Up @@ -744,7 +744,7 @@
36604401 uext 2 36604400 63
36604402 ite 2 16604400 36604401 36603601
36604800 eq 1 210 200
36604801 not 1 1 36604800
36604801 not 1 36604800
36605200 ite 2 16605200 200 36604402
36605600 constd 2 18446744073709551608
36605601 add 2 204 36605600
Expand Down Expand Up @@ -783,19 +783,19 @@
40000007 eq 1 234 40000006
40000008 constd 2 214
40000009 eq 1 234 40000008
41000000 and 1 1 36584400 40000007
41000000 and 1 36584400 40000007
41000001 ite 1 60 40000007 41000000
42000000 constd 2 0
42000001 state 2 read-counter
42000002 init 2 42000001 42000000
42000003 constd 2 0
42000004 eq 1 42000003 30
42000005 not 1 1 42000004
42000006 and 1 1 36584400 40000003
42000005 not 1 42000004
42000006 and 1 36584400 40000003
42000007 ite 1 42000006 21 41000001
42000008 ult 1 30 42000001
42000009 not 1 1 42000008
42000010 and 1 1 42000009 42000005
42000009 not 1 42000008
42000010 and 1 42000009 42000005
42000011 constd 2 18446744073709551615
42000012 ite 2 42000010 42000011 30
42000013 ite 2 42000006 42000012 36607600
Expand All @@ -804,7 +804,7 @@
42000016 sub 2 224 220
42000017 constd 2 8
42000018 ult 1 42000016 42000017
42000019 not 1 1 42000018
42000019 not 1 42000018
42000020 ite 2 42000019 42000017 42000016
42000021 ult 1 42000001 42000020
42000022 ite 2 42000021 42000001 42000020
Expand Down Expand Up @@ -847,14 +847,14 @@
42000059 add 2 222 220
42000060 write 3 20000021 42000059 42000058
42000061 ult 1 220 224
42000062 and 1 1 42000061 42000008
42000063 and 1 1 40000003 42000062
42000064 and 1 1 60 42000063
42000062 and 1 42000061 42000008
42000063 and 1 40000003 42000062
42000064 and 1 60 42000063
42000065 ult 1 30 42000022
42000066 and 1 1 42000064 42000065
42000066 and 1 42000064 42000065
42000067 ite 3 42000066 42000060 36606002
42000068 add 2 220 42000022
42000069 and 1 1 42000005 42000021
42000069 and 1 42000005 42000021
42000070 constd 2 18446744073709551615
42000071 ite 2 42000069 42000070 42000068
42000072 ite 2 42000064 42000071 42000013
Expand All @@ -864,24 +864,24 @@
42000076 sub 2 42000001 42000022
42000077 ite 2 42000066 42000076 42000001
42000078 next 2 42000001 42000077
45000000 and 1 1 36584400 40000009
45000000 and 1 36584400 40000009
45000001 constd 2 73728
45000002 state 2 bump-pointer
45000003 init 2 45000002 45000001
45000004 ult 1 220 45000002
45000005 not 1 1 45000004
45000005 not 1 45000004
45000006 ult 1 220 204
45000007 and 1 1 45000005 45000006
45000007 and 1 45000005 45000006
45000008 eq 1 30 30
45000009 and 1 1 45000007 45000008
45000010 and 1 1 45000000 45000009
45000009 and 1 45000007 45000008
45000010 and 1 45000000 45000009
45000011 ite 2 45000010 220 45000002
45000012 next 2 45000002 45000011
45000013 not 1 1 45000009
45000014 and 1 1 45000000 45000013
45000013 not 1 45000009
45000014 and 1 45000000 45000013
45000015 ite 2 45000014 45000002 42000072
46000000 next 1 60 42000075
46000001 or 1 1 41000000 62
46000001 or 1 41000000 62
46000002 next 1 62 46000001

; control flow
Expand All @@ -896,7 +896,7 @@
56556001 init 1 56556000 20
56556002 ite 1 56556000 60 16555600
56556003 next 1 56556000 56556002
56556004 and 1 1 56556000 64
56556004 and 1 56556000 64
56556005 next 1 16556000 56556004
56556400 next 1 16556400 16556000
56556800 next 1 16556800 16556400
Expand All @@ -907,7 +907,7 @@
56558401 init 1 56558400 20
56558402 ite 1 56558400 60 16558000
56558403 next 1 56558400 56558402
56558404 and 1 1 56558400 64
56558404 and 1 56558400 64
56558405 next 1 16558400 56558404
56558800 next 1 16558800 16558400
56559200 next 1 16559200 16558800
Expand All @@ -917,7 +917,7 @@
56560800 next 1 16560800 16560400
56561200 next 1 16561200 16560800
56561600 eq 1 202 36561200
56561601 and 1 1 16610400 56561600
56561601 and 1 16610400 56561600
56561602 next 1 16561600 56561601
56562000 next 1 16562000 16561600
56562400 ite 1 16606400 21 16562000
Expand All @@ -929,7 +929,7 @@
56564001 init 1 56564000 20
56564002 ite 1 56564000 60 16563600
56564003 next 1 56564000 56564002
56564004 and 1 1 56564000 64
56564004 and 1 56564000 64
56564005 ite 1 16595600 21 56564004
56564006 next 1 16564000 56564005
56564400 next 1 16564400 16564000
Expand All @@ -943,7 +943,7 @@
56567201 init 1 56567200 20
56567202 ite 1 56567200 60 16566800
56567203 next 1 56567200 56567202
56567204 and 1 1 56567200 64
56567204 and 1 56567200 64
56567205 next 1 16567200 56567204
56567600 next 1 16567600 20
56568000 next 1 16568000 16567600
Expand All @@ -957,7 +957,7 @@
56570801 init 1 56570800 20
56570802 ite 1 56570800 60 16570400
56570803 next 1 56570800 56570802
56570804 and 1 1 56570800 64
56570804 and 1 56570800 64
56570805 next 1 16570800 56570804
56571200 next 1 16571200 20
56571600 next 1 16571600 16571200
Expand All @@ -972,7 +972,7 @@
56574801 init 1 56574800 20
56574802 ite 1 56574800 60 16574400
56574803 next 1 56574800 56574802
56574804 and 1 1 56574800 64
56574804 and 1 56574800 64
56574805 next 1 16574800 56574804
56575200 next 1 16575200 16590000
56575600 next 1 16575600 16575200
Expand All @@ -988,25 +988,25 @@
56579201 init 1 56579200 20
56579202 ite 1 56579200 60 16578800
56579203 next 1 56579200 56579202
56579204 and 1 1 56579200 64
56579204 and 1 56579200 64
56579205 next 1 16579200 56579204
56579600 and 1 1 16579200 36579201
56579600 and 1 16579200 36579201
56579601 next 1 16579600 56579600
56580000 and 1 1 16579200 36579200
56580001 and 1 1 16579600 36579601
56580000 and 1 16579200 36579200
56580001 and 1 16579600 36579601
56580002 ite 1 56580001 21 56580000
56580003 next 1 16580000 56580002
56580400 and 1 1 16580000 36580001
56580400 and 1 16580000 36580001
56580401 next 1 16580400 56580400
56580800 next 1 16580800 16580400
56581200 and 1 1 16579600 36579600
56581201 and 1 1 16580000 36580000
56581200 and 1 16579600 36579600
56581201 and 1 16580000 36580000
56581202 ite 1 56581201 21 56581200
56581203 and 1 1 16580800 36580801
56581203 and 1 16580800 36580801
56581204 ite 1 56581203 21 56581202
56581205 next 1 16581200 56581204
56581600 next 1 16581600 16581200
56582000 and 1 1 16580800 36580800
56582000 and 1 16580800 36580800
56582001 ite 1 16581600 21 56582000
56582002 next 1 16582000 56582001
56582400 next 1 16582400 20
Expand All @@ -1019,7 +1019,7 @@
56584801 init 1 56584800 20
56584802 ite 1 56584800 60 16584400
56584803 next 1 56584800 56584802
56584804 and 1 1 56584800 64
56584804 and 1 56584800 64
56584805 next 1 16584800 56584804
56585200 next 1 16585200 16584800
56585600 next 1 16585600 16561200
Expand All @@ -1035,7 +1035,7 @@
56589600 next 1 16589600 16589200
56590000 next 1 16590000 16589600
56590400 eq 1 202 36590000
56590401 and 1 1 16582000 56590400
56590401 and 1 16582000 56590400
56590402 next 1 16590400 56590401
56590800 next 1 16590800 16590400
56591200 next 1 16591200 16590800
Expand All @@ -1051,7 +1051,7 @@
56595200 next 1 16595200 16594800
56595600 next 1 16595600 16595200
56596000 eq 1 202 36595600
56596001 and 1 1 16567200 56596000
56596001 and 1 16567200 56596000
56596002 next 1 16596000 56596001
56596400 next 1 16596400 16596000
56596800 next 1 16596800 16596400
Expand All @@ -1065,27 +1065,27 @@
56599600 next 1 16599600 16599200
56600000 next 1 16600000 16599600
56600400 next 1 16600400 16600000
56600800 and 1 1 16600400 36600401
56600800 and 1 16600400 36600401
56600801 next 1 16600800 56600800
56601200 next 1 16601200 16600800
56601600 next 1 16601600 16601200
56602000 next 1 16602000 16601600
56602400 next 1 16602400 16602000
56602800 and 1 1 16600400 36600400
56602800 and 1 16600400 36600400
56602801 next 1 16602800 56602800
56603200 next 1 16603200 16602800
56603600 next 1 16603600 16603200
56604000 next 1 16604000 16603600
56604400 next 1 16604400 16604000
56604800 next 1 16604800 16604400
56605200 and 1 1 16604800 36604801
56605200 and 1 16604800 36604801
56605201 next 1 16605200 56605200
56605600 next 1 16605600 16605200
56606000 next 1 16606000 16605600
56606400 next 1 16606400 16606000
56606800 eq 1 202 36606400
56606801 next 1 16606800 20
56607200 and 1 1 16604800 36604800
56607200 and 1 16604800 36604800
56607201 ite 1 16606800 21 56607200
56607202 next 1 16607200 56607201
56607600 next 1 16607600 16607200
Expand Down Expand Up @@ -1138,28 +1138,28 @@

; checking syscall id

80000000 not 1 1 40000001
80000001 not 1 1 40000003
80000002 not 1 1 40000005
80000003 not 1 1 40000007
80000004 not 1 1 40000009
80000005 and 1 1 80000000 80000001
80000006 and 1 1 80000005 80000002
80000007 and 1 1 80000006 80000003
80000008 and 1 1 80000007 80000004
80000009 and 1 1 36584400 80000008
80000000 not 1 40000001
80000001 not 1 40000003
80000002 not 1 40000005
80000003 not 1 40000007
80000004 not 1 40000009
80000005 and 1 80000000 80000001
80000006 and 1 80000005 80000002
80000007 and 1 80000006 80000003
80000008 and 1 80000007 80000004
80000009 and 1 36584400 80000008
80000010 bad 80000009 invalid-syscall-id

; checking exit code

80000011 eq 1 220 30
80000012 not 1 1 80000011
80000013 and 1 1 41000000 80000012
80000012 not 1 80000011
80000013 and 1 41000000 80000012
80000014 bad 80000013 non-zero-exit-code

; checking good exit state

80000015 and 1 1 62 40000007
80000015 and 1 62 40000007
80000016 bad 80000015 exit-state

; checking division and remainder by zero
Expand All @@ -1180,24 +1180,24 @@
80000027 ult 1 36609600 80000021
80000028 bad 80000027 memory-access-below-data
80000029 ult 1 36609600 80000022
80000030 not 1 1 80000029
80000030 not 1 80000029
80000031 ult 1 36609600 80000023
80000032 and 1 1 80000030 80000031
80000032 and 1 80000030 80000031
80000033 bad 80000032 memory-access-between-data-and-heap
80000034 ult 1 36609600 80000024
80000035 not 1 1 80000034
80000035 not 1 80000034
80000036 ult 1 36609600 45000002
80000037 and 1 1 80000035 80000036
80000037 and 1 80000035 80000036
80000038 bad 80000037 memory-access-between-max-and-dyn-heap
80000039 ult 1 36609600 45000002
80000040 not 1 1 80000039
80000040 not 1 80000039
80000041 ult 1 36609600 204
80000042 and 1 1 80000040 80000041
80000042 and 1 80000040 80000041
80000043 bad 80000042 memory-access-between-heap-and-stack
80000044 ult 1 36609600 204
80000045 not 1 1 80000044
80000045 not 1 80000044
80000046 ult 1 36609600 80000025
80000047 and 1 1 80000045 80000046
80000047 and 1 80000045 80000046
80000048 bad 80000047 memory-access-between-dyn-and-max-stack
80000049 ult 1 80000026 36609600
80000050 bad 80000049 memory-access-above-stack
Expand Down
Loading

0 comments on commit 311051e

Please sign in to comment.