classify griggio benchmarks

Since they are QF, the SAT answers can be verified with PyMPF. Not sure what to do about UNSAT ones.

[x] add_01_1000_1.smt2
[x] add_01_1000_2.smt2
[x] add_01_1000_3.smt2
[x] add_01_1000_4.smt2
[x] add_01_100_1.smt2
[x] add_01_100_2.smt2
[x] add_01_100_3.smt2
[x] add_01_100_4.smt2
[x] add_01_10_1.smt2
[x] add_01_10_2.smt2
[x] add_01_10_3.smt2
[x] add_01_10_4.smt2
[x] add_01_1_1.smt2
[x] add_01_1_2.smt2
[x] add_01_1_3.smt2
[x] add_01_1_4.smt2
[x] div.c.10.smt2
[x] div.c.20.smt2
[x] div.c.3.smt2
[x] div.c.30.smt2
[x] div.c.40.smt2
[x] div.c.50.smt2
[x] div2.c.10.smt2
[x] div2.c.20.smt2
[x] div2.c.3.smt2
[x] div2.c.30.smt2
[x] div2.c.40.smt2
[x] div2.c.50.smt2
[x] div3.c.10.smt2
[x] div3.c.20.smt2
[x] div3.c.3.smt2
[x] div3.c.30.smt2
[x] div3.c.40.smt2
[x] div3.c.50.smt2
[x] e1.c.smt2
[x] e1_1.c.smt2
[x] e1_2.c.smt2
[x] e2.c.smt2
[x] e2_1.c.smt2
[x] e2_2.c.smt2
[x] e2_3.c.smt2
[x] e2a_1.c.smt2
[x] e2a_2.c.smt2
[x] e2a_3.c.smt2
[x] e3.c.smt2
[x] e3_1.c.smt2
[x] e3_2.c.smt2
[x] f23.smt2
[ ] gaussian.c.125.smt2
[ ] gaussian.c.175.smt2
[x] gaussian.c.25.smt2
[x] gaussian.c.75.smt2
[ ] mul_000003_30000_1.smt2
[ ] mul_03_3000_1.smt2
[x] mul_03_30_1.smt2
[x] mul_03_30_2.smt2
[x] mul_03_30_3.smt2
[x] mul_03_30_4.smt2
[x] mul_03_30_5.smt2
[x] mul_03_30_6.smt2
[x] mul_03_30_7.smt2
[x] mul_03_3_1.smt2
[x] mult1.c.10.smt2
[x] mult1.c.20.smt2
[x] mult1.c.3.smt2
[x] mult1.c.30.smt2
[x] mult1.c.40.smt2
[x] mult1.c.50.smt2
[x] mult2.c.10.smt2
[x] mult2.c.20.smt2
[x] mult2.c.3.smt2
[x] mult2.c.30.smt2
[x] mult2.c.40.smt2
[x] mult2.c.50.smt2
[x] newton.1.1.i.smt2
[ ] newton.1.2.i.smt2
[ ] newton.1.3.i.smt2
[x] newton.2.1.i.smt2
[ ] newton.2.2.i.smt2
[ ] newton.2.3.i.smt2
[ ] newton.3.1.i.smt2
[ ] newton.3.2.i.smt2
[ ] newton.3.3.i.smt2
[x] newton.4.1.i.smt2
[ ] newton.4.2.i.smt2
[ ] newton.4.3.i.smt2
[x] newton.5.1.i.smt2
[ ] newton.5.2.i.smt2
[ ] newton.5.3.i.smt2
[x] newton.6.1.i.smt2
[ ] newton.6.2.i.smt2
[ ] newton.6.3.i.smt2
[x] newton.7.1.i.smt2
[ ] newton.7.2.i.smt2
[ ] newton.7.3.i.smt2
[x] newton.8.1.i.smt2
[ ] newton.8.2.i.smt2
[ ] newton.8.3.i.smt2
[x] pow5.smt2
[x] qurt.c.10.smt2
[x] qurt.c.15.smt2
[x] qurt.c.2.smt2
[ ] qurt.c.20.smt2
[ ] qurt.c.25.smt2
[x] qurt.c.5.smt2
[ ] sin.c.125.smt2
[ ] sin.c.175.smt2
[ ] sin.c.25.smt2
[ ] sin.c.75.smt2
[ ] sin2.c.10.smt2
[ ] sin2.c.125.smt2
[ ] sin2.c.15.smt2
[ ] sin2.c.175.smt2
[x] sin2.c.2.smt2
[ ] sin2.c.20.smt2
[ ] sin2.c.25.smt2
[x] sin2.c.5.smt2
[ ] sin2.c.75.smt2
[x] sine.1.0.i.smt2
[x] sine.2.0.i.smt2
[x] sine.3.0.i.smt2
[x] sine.4.0.i.smt2
[x] sine.5.0.i.smt2
[x] sine.6.0.i.smt2
[x] sine.7.0.i.smt2
[x] sine.8.0.i.smt2
[ ] sqrt.c.10.smt2
[x] sqrt.c.15.smt2
[x] sqrt.c.2.smt2
[x] sqrt.c.20.smt2
[x] sqrt.c.25.smt2
[ ] sqrt.c.5.smt2
[x] square.1.0.i.smt2
[x] square.2.0.i.smt2
[x] square.3.0.i.smt2
[x] square.4.0.i.smt2
[x] square.5.0.i.smt2
[x] square.6.0.i.smt2
[x] square.7.0.i.smt2
[x] square.8.0.i.smt2
[x] square.smt2
[x] square_and_power_inverse.smt2
[x] test_v3_r3_vr10_c1_s14052.smt2
[x] test_v3_r3_vr10_c1_s24300.smt2
[x] test_v3_r3_vr10_c1_s29304.smt2
[x] test_v3_r3_vr1_c1_s10392.smt2
[x] test_v3_r3_vr1_c1_s5578.smt2
[x] test_v3_r3_vr1_c1_s6731.smt2
[x] test_v3_r3_vr5_c1_s16641.smt2
[x] test_v3_r3_vr5_c1_s16867.smt2
[x] test_v3_r3_vr5_c1_s26769.smt2
[x] test_v3_r8_vr10_c1_s18214.smt2
[x] test_v3_r8_vr10_c1_s4660.smt2
[x] test_v3_r8_vr10_c1_s5590.smt2
[x] test_v3_r8_vr1_c1_s20372.smt2
[x] test_v3_r8_vr1_c1_s23752.smt2
[x] test_v3_r8_vr1_c1_s733.smt2
[x] test_v3_r8_vr5_c1_s10746.smt2
[x] test_v3_r8_vr5_c1_s1507.smt2
[x] test_v3_r8_vr5_c1_s8257.smt2
[ ] test_v5_r10_vr10_c1_s15708.smt2
[x] test_v5_r10_vr10_c1_s21502.smt2
[ ] test_v5_r10_vr10_c1_s7608.smt2
[x] test_v5_r10_vr1_c1_s13516.smt2
[x] test_v5_r10_vr1_c1_s19145.smt2
[x] test_v5_r10_vr1_c1_s32538.smt2
[x] test_v5_r10_vr5_c1_s13195.smt2
[x] test_v5_r10_vr5_c1_s13679.smt2
[x] test_v5_r10_vr5_c1_s8690.smt2
[x] test_v5_r15_vr10_c1_s11127.smt2
[ ] test_v5_r15_vr10_c1_s14516.smt2
[ ] test_v5_r15_vr10_c1_s25268.smt2
[x] test_v5_r15_vr1_c1_s26845.smt2
[x] test_v5_r15_vr1_c1_s32559.smt2
[x] test_v5_r15_vr1_c1_s8236.smt2
[x] test_v5_r15_vr5_c1_s23844.smt2
[x] test_v5_r15_vr5_c1_s26657.smt2
[x] test_v5_r15_vr5_c1_s8246.smt2
[x] test_v5_r5_vr10_c1_s5379.smt2
[x] test_v5_r5_vr10_c1_s5996.smt2
[x] test_v5_r5_vr10_c1_s7194.smt2
[x] test_v5_r5_vr1_c1_s14623.smt2
[x] test_v5_r5_vr1_c1_s15604.smt2
[x] test_v5_r5_vr1_c1_s16138.smt2
[x] test_v5_r5_vr5_c1_s24018.smt2
[x] test_v5_r5_vr5_c1_s2800.smt2
[x] test_v5_r5_vr5_c1_s9855.smt2
[x] test_v7_r12_vr10_c1_s15994.smt2
[ ] test_v7_r12_vr10_c1_s18160.smt2
[ ] test_v7_r12_vr10_c1_s30410.smt2
[ ] test_v7_r12_vr1_c1_s10576.smt2
[ ] test_v7_r12_vr1_c1_s22787.smt2
[ ] test_v7_r12_vr1_c1_s703.smt2
[x] test_v7_r12_vr5_c1_s14336.smt2
[x] test_v7_r12_vr5_c1_s29826.smt2
[x] test_v7_r12_vr5_c1_s8938.smt2
[ ] test_v7_r17_vr10_c1_s18654.smt2
[ ] test_v7_r17_vr10_c1_s3680.smt2
[ ] test_v7_r17_vr10_c1_s8773.smt2
[ ] test_v7_r17_vr1_c1_s23882.smt2
[ ] test_v7_r17_vr1_c1_s24331.smt2
[ ] test_v7_r17_vr1_c1_s30331.smt2
[ ] test_v7_r17_vr5_c1_s25451.smt2
[ ] test_v7_r17_vr5_c1_s2807.smt2
[ ] test_v7_r17_vr5_c1_s4772.smt2
[x] test_v7_r7_vr10_c1_s10625.smt2
[x] test_v7_r7_vr10_c1_s24535.smt2
[x] test_v7_r7_vr10_c1_s32506.smt2
[x] test_v7_r7_vr1_c1_s22845.smt2
[ ] test_v7_r7_vr1_c1_s24449.smt2
[x] test_v7_r7_vr1_c1_s4574.smt2
[x] test_v7_r7_vr5_c1_s14675.smt2
[x] test_v7_r7_vr5_c1_s19694.smt2
[x] test_v7_r7_vr5_c1_s3582.smt2

florianschanda / smtlib_schanda

classify griggio benchmarks #5