Skip to content

Commit

Permalink
data for experiments
Browse files Browse the repository at this point in the history
  • Loading branch information
@FedericoAureliano
FedericoAureliano committed Oct 14, 2020
1 parent bde7f3f commit f1dc5bd
Show file tree
Hide file tree
Showing 27 changed files with 26,116 additions and 1 deletion.
3 changes: 2 additions & 1 deletion .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,5 @@
/build
/dist
medleysolver.egg-info
/tmp
*.smt2
.DS_STORE
997 changes: 997 additions & 0 deletions tmp/BV/Bitwuzla.csv
View file

Large diffs are not rendered by default.

997 changes: 997 additions & 0 deletions tmp/BV/CVC4.csv
View file

Large diffs are not rendered by default.

997 changes: 997 additions & 0 deletions tmp/BV/MathSAT.csv
View file

Large diffs are not rendered by default.

997 changes: 997 additions & 0 deletions tmp/BV/YICES.csv
View file

Large diffs are not rendered by default.

997 changes: 997 additions & 0 deletions tmp/BV/Z3.csv
View file

Large diffs are not rendered by default.

1,005 changes: 1,005 additions & 0 deletions tmp/QF_ABV/BOOLECTOR.csv
View file

Large diffs are not rendered by default.

1,005 changes: 1,005 additions & 0 deletions tmp/QF_ABV/Bitwuzla.csv
View file

Large diffs are not rendered by default.

1,005 changes: 1,005 additions & 0 deletions tmp/QF_ABV/CVC4.csv
View file

Large diffs are not rendered by default.

1,005 changes: 1,005 additions & 0 deletions tmp/QF_ABV/MathSAT.csv
View file

Large diffs are not rendered by default.

1,005 changes: 1,005 additions & 0 deletions tmp/QF_ABV/YICES.csv
View file

Large diffs are not rendered by default.

1,005 changes: 1,005 additions & 0 deletions tmp/QF_ABV/Z3.csv
View file

Large diffs are not rendered by default.

81 changes: 81 additions & 0 deletions tmp/QF_AUFBV/BOOLECTOR.csv
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_add1.short.smt2,"[0.34202651 0.14100191 0.1468618 0. 0. 0.
0. 0. 0.1465284 0. 0.09258251]",BOOLECTOR,0.05785703659057617,unsat,['BOOLECTOR'],[0.05785703659057617]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_add2.short.smt2,"[0.59079062 0.22138724 0.51085142 0. 0. 0.
0. 0. 0.43093923 0. 0.48598131]",BOOLECTOR,0.11310696601867676,unsat,['BOOLECTOR'],[0.11310696601867676]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_add3.short.smt2,"[0.50661739 0.17354007 0.33939902 0. 0. 0.
0. 0. 0.57330291 0. 0.31046162]",BOOLECTOR,0.09217405319213867,unsat,['BOOLECTOR'],[0.09217405319213867]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_add4.short.smt2,"[0.66621803 0.15175912 0.46371929 0. 0. 0.
0. 0. 0.63625899 0. 0.42485549]",BOOLECTOR,0.06513285636901855,unsat,['BOOLECTOR'],[0.06513285636901855]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_sub1.short.smt2,"[0.17604695 0.0555549 0.11405783 0. 0. 0.
0. 0. 0.03405573 0. 0.08188005]",BOOLECTOR,0.39084911346435547,unsat,['BOOLECTOR'],[0.39084911346435547]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_sub2.short.smt2,"[0.17062563 0.07511457 0.10325897 0. 0. 0.
0. 0. 0.0378198 0. 0.0728988 ]",BOOLECTOR,1.4936180114746094,unsat,['BOOLECTOR'],[1.4936180114746094]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_sub3.short.smt2,"[0.18680868 0.08319756 0.1136939 0. 0. 0.
0. 0. 0.04196576 0. 0.08050847]",BOOLECTOR,1.443289041519165,unsat,['BOOLECTOR'],[1.443289041519165]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_mul_aux2.short.smt2,"[4.38815263 1.35991594 5.18740813 0. 0. 0.
0. 0. 2.90628707 0. 5.3546817 ]",BOOLECTOR,0.596160888671875,unsat,['BOOLECTOR'],[0.596160888671875]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_mul_aux3.short.smt2,"[6.08878256 1.40641822 7.68416596 0. 0. 0.
0. 0. 3.53535354 0. 8.03241826]",BOOLECTOR,0.6037061214447021,unsat,['BOOLECTOR'],[0.6037061214447021]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_mul_aux4.short.smt2,"[4.54383954 0.99506087 5.6354792 0. 0. 0.
0. 0. 2.50996016 0. 5.85362666]",BOOLECTOR,0.5604190826416016,unsat,['BOOLECTOR'],[0.5604190826416016]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_aux1.short.smt2,"[1.54121037 1.54694301 1.71020856 0. 0. 0.
0. 0. 1.8358209 0. 1.81118012]",BOOLECTOR,0.13269305229187012,unsat,['BOOLECTOR'],[0.13269305229187012]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_aux11.short.smt2,"[2.06889691 0.76755529 1.72399621 0. 0. 0.
0. 0. 3.54970224 0. 1.69948934]",BOOLECTOR,0.14417290687561035,unsat,['BOOLECTOR'],[0.14417290687561035]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_aux12.short.smt2,"[2.26153146 0.90300966 1.93226483 0. 0. 0.
0. 0. 3.70854271 0. 1.91261352]",BOOLECTOR,0.1357719898223877,unsat,['BOOLECTOR'],[0.1357719898223877]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_init.short.smt2,"[0.53944158 0.12902693 0.26596816 0. 0. 0.
0. 0. 0.25621118 0. 0.16284551]",BOOLECTOR,0.08004999160766602,unsat,['BOOLECTOR'],[0.08004999160766602]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_init1.short.smt2,"[0.71322406 0.15941693 0.36484839 0. 0. 0.
0. 0. 0.31984036 0. 0.22481295]",BOOLECTOR,0.039388179779052734,unsat,['BOOLECTOR'],[0.039388179779052734]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_init2.short.smt2,[1. 1. 1. 0. 0. 0. 0. 0. 1. 0. 1.],BOOLECTOR,0.06903600692749023,unsat,['BOOLECTOR'],[0.06903600692749023]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.group_red1.short.smt2,"[0.27036161 0.09891834 0.29333647 0. 0. 0.
0. 0. 0.36566332 0. 0.30515565]",BOOLECTOR,0.10292792320251465,unsat,['BOOLECTOR'],[0.10292792320251465]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div1.short.smt2,"[0.26438188 0.12978245 0.24250733 0. 0. 0.
0. 0. 0.14532872 0. 0.21889701]",BOOLECTOR,0.06002306938171387,unsat,['BOOLECTOR'],[0.06002306938171387]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div10.short.smt2,"[0.19213902 0.08321571 0.16045381 0. 0. 0.
0. 0. 0.08965136 0. 0.13787234]",BOOLECTOR,0.0413820743560791,unsat,['BOOLECTOR'],[0.0413820743560791]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div12.short.smt2,"[0.2778022 0.07412796 0.2613769 0. 0. 0.
0. 0. 0.15962441 0. 0.23848816]",BOOLECTOR,0.05993986129760742,unsat,['BOOLECTOR'],[0.05993986129760742]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div14.short.smt2,"[0.272215 0.1240292 0.24383164 0. 0. 0.
0. 0. 0.17414966 0. 0.22040013]",BOOLECTOR,0.10140800476074219,unsat,['BOOLECTOR'],[0.10140800476074219]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mul_inner3.short.smt2,"[0.21069182 0.06350912 0.14654323 0. 0. 0.
0. 0. 0.20091324 0. 0.14621849]",BOOLECTOR,0.8901169300079346,sat,['BOOLECTOR'],[0.8901169300079346]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mul_inner4.short.smt2,"[0.14652157 0.05083207 0.15683985 0. 0. 0.
0. 0. 0.21407186 0. 0.1644887 ]",BOOLECTOR,1.541823148727417,sat,['BOOLECTOR'],[1.541823148727417]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.signHash3.short.smt2,"[2.20526823 0.69600499 2.21715328 0. 0. 0.
0. 0. 2.60714286 0. 2.27118644]",BOOLECTOR,1.8090240955352783,unsat,['BOOLECTOR'],[1.8090240955352783]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.signHash4.short.smt2,"[2.21059209 0.42492713 1.73134328 0. 0. 0.
0. 0. 3.89047936 0. 1.67644285]",BOOLECTOR,3.9702558517456055,unsat,['BOOLECTOR'],[3.9702558517456055]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.signHash5.short.smt2,"[2.12199313 0.43106194 1.67243697 0. 0. 0.
0. 0. 3.53789443 0. 1.61553589]",BOOLECTOR,1.607140064239502,unsat,['BOOLECTOR'],[1.607140064239502]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.sq_inner12.short.smt2,"[0.13404389 0.04282676 0.06303748 0. 0. 0.
0. 0. 0.03161492 0. 0.05785268]",BOOLECTOR,0.1456310749053955,sat,['BOOLECTOR'],[0.1456310749053955]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.sq_inner13.short.smt2,"[0.04740886 0.0353752 0.04592423 0. 0. 0.
0. 0. 0.03307607 0. 0.04589926]",BOOLECTOR,0.134552001953125,sat,['BOOLECTOR'],[0.134552001953125]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.sq_inner22.short.smt2,"[0.12091455 0.06337829 0.06472628 0. 0. 0.
0. 0. 0.03019213 0. 0.06088786]",BOOLECTOR,0.6920778751373291,sat,['BOOLECTOR'],[0.6920778751373291]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.sq_inner23.short.smt2,"[0.06554622 0.04550505 0.07467532 0. 0. 0.
0. 0. 0.03152124 0. 0.07613373]",BOOLECTOR,1.353247880935669,sat,['BOOLECTOR'],[1.353247880935669]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.verifySignature.short.smt2,"[1.97439353 0.475471 1.49476456 0. 0. 0.
0. 0. 3.1671834 0. 1.40299501]",BOOLECTOR,26.41321897506714,unsat,['BOOLECTOR'],[26.41321897506714]
./tmp/QF_AUFBV/opStructure_C_16_32_2_2.smt2,"[0.00517837 0.79948313 0.00657174 0. 0. 0.
0. 0. 0. 0. 0. ]",BOOLECTOR,60,timeout (60.0 s),['BOOLECTOR'],[60]
./tmp/QF_AUFBV/opStructure_MBA_6.smt2,"[2.02663578e-03 4.20336261e+00 2.71618625e-02 0.00000000e+00
0.00000000e+00 0.00000000e+00 0.00000000e+00 0.00000000e+00
0.00000000e+00 0.00000000e+00 0.00000000e+00]",BOOLECTOR,52.87152695655823,error,['BOOLECTOR'],[52.87152695655823]
./tmp/QF_AUFBV/opStructure_MBA_7.smt2,"[1.80365885e-03 1.44911930e+01 1.85185185e-02 0.00000000e+00
0.00000000e+00 0.00000000e+00 0.00000000e+00 0.00000000e+00
0.00000000e+00 0.00000000e+00 0.00000000e+00]",BOOLECTOR,57.35759401321411,error,['BOOLECTOR'],[57.35759401321411]
./tmp/QF_AUFBV/opStructure_NPT_1.smt2,"[0.00356994 0.01148702 0.00532954 0. 0. 0.
0. 0. 0. 0. 0. ]",BOOLECTOR,60,timeout (60.0 s),['BOOLECTOR'],[60]
./tmp/QF_AUFBV/opStructure_NPT_2.smt2,"[0.00379407 0.00933751 0.00585128 0. 0. 0.
0. 0. 0. 0. 0. ]",BOOLECTOR,60,timeout (60.0 s),['BOOLECTOR'],[60]
./tmp/QF_AUFBV/opStructure_O_16_24_2_2.smt2,"[0.00368906 0.85854528 0.00568967 0. 0. 0.
0. 0. 0. 0. 0. ]",BOOLECTOR,60,timeout (60.0 s),['BOOLECTOR'],[60]
./tmp/QF_AUFBV/opStructure_O_16_32_2_2.smt2,"[0.00398992 1.20034477 0.00616483 0. 0. 0.
0. 0. 0. 0. 0. ]",BOOLECTOR,60,timeout (60.0 s),['BOOLECTOR'],[60]
./tmp/QF_AUFBV/opStructure_O_32_16_2_2.smt2,"[0.00462963 0.83449639 0.00885936 0. 0. 0.
0. 0. 0. 0. 0. ]",BOOLECTOR,60,timeout (60.0 s),['BOOLECTOR'],[60]
./tmp/QF_AUFBV/opStructure_O_32_32_2_2.smt2,"[0.0045977 2.80746918 0.00874317 0. 0. 0.
0. 0. 0. 0. 0. ]",BOOLECTOR,60,timeout (60.0 s),['BOOLECTOR'],[60]
81 changes: 81 additions & 0 deletions tmp/QF_AUFBV/Bitwuzla.csv
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_add1.short.smt2,"[0.34202651 0.14100191 0.1468618 0. 0. 0.
0. 0. 0.1465284 0. 0.09258251]",Bitwuzla,0.061296939849853516,unsat,['Bitwuzla'],[0.061296939849853516]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_add2.short.smt2,"[0.59079062 0.22138724 0.51085142 0. 0. 0.
0. 0. 0.43093923 0. 0.48598131]",Bitwuzla,0.060302019119262695,unsat,['Bitwuzla'],[0.060302019119262695]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_add3.short.smt2,"[0.50661739 0.17354007 0.33939902 0. 0. 0.
0. 0. 0.57330291 0. 0.31046162]",Bitwuzla,0.09005093574523926,unsat,['Bitwuzla'],[0.09005093574523926]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_add4.short.smt2,"[0.66621803 0.15175912 0.46371929 0. 0. 0.
0. 0. 0.63625899 0. 0.42485549]",Bitwuzla,0.05489397048950195,unsat,['Bitwuzla'],[0.05489397048950195]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_sub1.short.smt2,"[0.17604695 0.0555549 0.11405783 0. 0. 0.
0. 0. 0.03405573 0. 0.08188005]",Bitwuzla,0.14511513710021973,unsat,['Bitwuzla'],[0.14511513710021973]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_sub2.short.smt2,"[0.17062563 0.07511457 0.10325897 0. 0. 0.
0. 0. 0.0378198 0. 0.0728988 ]",Bitwuzla,0.13594818115234375,unsat,['Bitwuzla'],[0.13594818115234375]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_full_sub3.short.smt2,"[0.18680868 0.08319756 0.1136939 0. 0. 0.
0. 0. 0.04196576 0. 0.08050847]",Bitwuzla,0.1281728744506836,unsat,['Bitwuzla'],[0.1281728744506836]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_mul_aux2.short.smt2,"[4.38815263 1.35991594 5.18740813 0. 0. 0.
0. 0. 2.90628707 0. 5.3546817 ]",Bitwuzla,0.3896059989929199,unsat,['Bitwuzla'],[0.3896059989929199]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_mul_aux3.short.smt2,"[6.08878256 1.40641822 7.68416596 0. 0. 0.
0. 0. 3.53535354 0. 8.03241826]",Bitwuzla,0.3480348587036133,unsat,['Bitwuzla'],[0.3480348587036133]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_mul_aux4.short.smt2,"[4.54383954 0.99506087 5.6354792 0. 0. 0.
0. 0. 2.50996016 0. 5.85362666]",Bitwuzla,0.33704304695129395,unsat,['Bitwuzla'],[0.33704304695129395]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_aux1.short.smt2,"[1.54121037 1.54694301 1.71020856 0. 0. 0.
0. 0. 1.8358209 0. 1.81118012]",Bitwuzla,0.16932296752929688,unsat,['Bitwuzla'],[0.16932296752929688]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_aux11.short.smt2,"[2.06889691 0.76755529 1.72399621 0. 0. 0.
0. 0. 3.54970224 0. 1.69948934]",Bitwuzla,0.19550704956054688,unsat,['Bitwuzla'],[0.19550704956054688]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_aux12.short.smt2,"[2.26153146 0.90300966 1.93226483 0. 0. 0.
0. 0. 3.70854271 0. 1.91261352]",Bitwuzla,0.138077974319458,unsat,['Bitwuzla'],[0.138077974319458]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_init.short.smt2,"[0.53944158 0.12902693 0.26596816 0. 0. 0.
0. 0. 0.25621118 0. 0.16284551]",Bitwuzla,0.09484982490539551,unsat,['Bitwuzla'],[0.09484982490539551]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_init1.short.smt2,"[0.71322406 0.15941693 0.36484839 0. 0. 0.
0. 0. 0.31984036 0. 0.22481295]",Bitwuzla,0.06233096122741699,unsat,['Bitwuzla'],[0.06233096122741699]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.ec_twin_mul_init2.short.smt2,[1. 1. 1. 0. 0. 0. 0. 0. 1. 0. 1.],Bitwuzla,0.1007530689239502,unsat,['Bitwuzla'],[0.1007530689239502]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.group_red1.short.smt2,"[0.27036161 0.09891834 0.29333647 0. 0. 0.
0. 0. 0.36566332 0. 0.30515565]",Bitwuzla,0.0975179672241211,unsat,['Bitwuzla'],[0.0975179672241211]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div1.short.smt2,"[0.26438188 0.12978245 0.24250733 0. 0. 0.
0. 0. 0.14532872 0. 0.21889701]",Bitwuzla,0.1968700885772705,unsat,['Bitwuzla'],[0.1968700885772705]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div10.short.smt2,"[0.19213902 0.08321571 0.16045381 0. 0. 0.
0. 0. 0.08965136 0. 0.13787234]",Bitwuzla,0.048774003982543945,unsat,['Bitwuzla'],[0.048774003982543945]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div12.short.smt2,"[0.2778022 0.07412796 0.2613769 0. 0. 0.
0. 0. 0.15962441 0. 0.23848816]",Bitwuzla,0.14065098762512207,unsat,['Bitwuzla'],[0.14065098762512207]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mod_div14.short.smt2,"[0.272215 0.1240292 0.24383164 0. 0. 0.
0. 0. 0.17414966 0. 0.22040013]",Bitwuzla,0.19960808753967285,unsat,['Bitwuzla'],[0.19960808753967285]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mul_inner3.short.smt2,"[0.21069182 0.06350912 0.14654323 0. 0. 0.
0. 0. 0.20091324 0. 0.14621849]",Bitwuzla,0.6011910438537598,sat,['Bitwuzla'],[0.6011910438537598]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.mul_inner4.short.smt2,"[0.14652157 0.05083207 0.15683985 0. 0. 0.
0. 0. 0.21407186 0. 0.1644887 ]",Bitwuzla,0.14999008178710938,sat,['Bitwuzla'],[0.14999008178710938]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.signHash3.short.smt2,"[2.20526823 0.69600499 2.21715328 0. 0. 0.
0. 0. 2.60714286 0. 2.27118644]",Bitwuzla,1.8024699687957764,unsat,['Bitwuzla'],[1.8024699687957764]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.signHash4.short.smt2,"[2.21059209 0.42492713 1.73134328 0. 0. 0.
0. 0. 3.89047936 0. 1.67644285]",Bitwuzla,3.6654810905456543,unsat,['Bitwuzla'],[3.6654810905456543]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.signHash5.short.smt2,"[2.12199313 0.43106194 1.67243697 0. 0. 0.
0. 0. 3.53789443 0. 1.61553589]",Bitwuzla,3.3315060138702393,unsat,['Bitwuzla'],[3.3315060138702393]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.sq_inner12.short.smt2,"[0.13404389 0.04282676 0.06303748 0. 0. 0.
0. 0. 0.03161492 0. 0.05785268]",Bitwuzla,0.1468510627746582,sat,['Bitwuzla'],[0.1468510627746582]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.sq_inner13.short.smt2,"[0.04740886 0.0353752 0.04592423 0. 0. 0.
0. 0. 0.03307607 0. 0.04589926]",Bitwuzla,0.06670093536376953,sat,['Bitwuzla'],[0.06670093536376953]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.sq_inner22.short.smt2,"[0.12091455 0.06337829 0.06472628 0. 0. 0.
0. 0. 0.03019213 0. 0.06088786]",Bitwuzla,0.3433821201324463,sat,['Bitwuzla'],[0.3433821201324463]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.sq_inner23.short.smt2,"[0.06554622 0.04550505 0.07467532 0. 0. 0.
0. 0. 0.03152124 0. 0.07613373]",Bitwuzla,0.14131593704223633,sat,['Bitwuzla'],[0.14131593704223633]
./tmp/QF_AUFBV/com.galois.ecc.P384ECC64.verifySignature.short.smt2,"[1.97439353 0.475471 1.49476456 0. 0. 0.
0. 0. 3.1671834 0. 1.40299501]",Bitwuzla,7.125905990600586,unsat,['Bitwuzla'],[7.125905990600586]
./tmp/QF_AUFBV/opStructure_C_16_32_2_2.smt2,"[0.00517837 0.79948313 0.00657174 0. 0. 0.
0. 0. 0. 0. 0. ]",Bitwuzla,60,timeout (60.0 s),['Bitwuzla'],[60]
./tmp/QF_AUFBV/opStructure_MBA_6.smt2,"[2.02663578e-03 4.20336261e+00 2.71618625e-02 0.00000000e+00
0.00000000e+00 0.00000000e+00 0.00000000e+00 0.00000000e+00
0.00000000e+00 0.00000000e+00 0.00000000e+00]",Bitwuzla,30.141774892807007,error,['Bitwuzla'],[30.141774892807007]
./tmp/QF_AUFBV/opStructure_MBA_7.smt2,"[1.80365885e-03 1.44911930e+01 1.85185185e-02 0.00000000e+00
0.00000000e+00 0.00000000e+00 0.00000000e+00 0.00000000e+00
0.00000000e+00 0.00000000e+00 0.00000000e+00]",Bitwuzla,46.51360201835632,error,['Bitwuzla'],[46.51360201835632]
./tmp/QF_AUFBV/opStructure_NPT_1.smt2,"[0.00356994 0.01148702 0.00532954 0. 0. 0.
0. 0. 0. 0. 0. ]",Bitwuzla,60,timeout (60.0 s),['Bitwuzla'],[60]
./tmp/QF_AUFBV/opStructure_NPT_2.smt2,"[0.00379407 0.00933751 0.00585128 0. 0. 0.
0. 0. 0. 0. 0. ]",Bitwuzla,0.5396239757537842,sat,['Bitwuzla'],[0.5396239757537842]
./tmp/QF_AUFBV/opStructure_O_16_24_2_2.smt2,"[0.00368906 0.85854528 0.00568967 0. 0. 0.
0. 0. 0. 0. 0. ]",Bitwuzla,60,timeout (60.0 s),['Bitwuzla'],[60]
./tmp/QF_AUFBV/opStructure_O_16_32_2_2.smt2,"[0.00398992 1.20034477 0.00616483 0. 0. 0.
0. 0. 0. 0. 0. ]",Bitwuzla,60,timeout (60.0 s),['Bitwuzla'],[60]
./tmp/QF_AUFBV/opStructure_O_32_16_2_2.smt2,"[0.00462963 0.83449639 0.00885936 0. 0. 0.
0. 0. 0. 0. 0. ]",Bitwuzla,60,timeout (60.0 s),['Bitwuzla'],[60]
./tmp/QF_AUFBV/opStructure_O_32_32_2_2.smt2,"[0.0045977 2.80746918 0.00874317 0. 0. 0.
0. 0. 0. 0. 0. ]",Bitwuzla,29.474472999572754,error,['Bitwuzla'],[29.474472999572754]
Loading

0 comments on commit f1dc5bd

Please sign in to comment.