SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Best Overall Ranking - Single Query Track

Page generated on 2025-08-11

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 (45.708019) cvc5 (45.708019) cvc5 (11.028006) cvc5 (15.132984) cvc5 (32.772523)

Sequential Performance

Division Solver Contribution
QF_Strings Z3-Noodler-Mocha 4.503171
QF_Strings Z3-Noodler 4.378626
QF_Strings Z3-Noodler-Mocha-base 4.366658
QF_Strings OSTRICH 4.155295
QF_Bitvec Bitwuzla-MachBV 3.895111
QF_Bitvec Bitwuzla 3.876625
QF_Bitvec Yices2 3.871457
QF_Bitvec Bitwuzla-MachBV-base 3.86703
QF_Equality_Bitvec Bitwuzla 3.736878
QF_Equality_Bitvec Yices2 3.692774
QF_Strings cvc5 3.640918
QF_Equality Yices2 3.582177
QF_Equality OpenSMT 3.580302
QF_Equality cvc5 3.578428
QF_Equality_Bitvec Z3-Owl 3.538279
QF_Equality_Bitvec cvc5 3.497113
QF_Bitvec cvc5 3.474071
QF_Equality SMTInterpol 3.43742
QF_Equality_Bitvec Z3-Owl-base 3.380212
QF_Strings Z3-alpha-base 3.350193
QF_Strings Z3-Noodler-base 3.334725
QF_Strings Z3-alpha 3.334043
QF_LinearIntArith OpenSMT 3.102205
QF_FPArith Bitwuzla 3.049823
QF_Bitvec z3siri 3.047568
QF_LinearIntArith Yices2 2.997634
QF_LinearIntArith cvc5 2.988723
QF_NonLinearRealArith Z3-alpha 2.956225
QF_NonLinearRealArith z3siri-base 2.937623
QF_NonLinearRealArith Z3-alpha-base 2.937623
QF_FPArith cvc5 2.933724
FPArith Bitwuzla 2.929808
QF_NonLinearRealArith z3siri 2.847523
QF_Equality_LinearArith SMTInterpol 2.835018
QF_Bitvec Z3-alpha 2.830255
QF_Equality_LinearArith cvc5 2.825566
QF_Bitvec Z3-alpha-base 2.814501
QF_Bitvec z3siri-base 2.813872
QF_LinearIntArith Z3-alpha 2.779898
QF_NonLinearRealArith cvc5 2.772844
QF_Equality_LinearArith OpenSMT 2.772299
QF_Bitvec bv_decide-nokernel 2.762512
FPArith cvc5 2.751887
QF_NonLinearRealArith Yices2 2.73289
QF_NonLinearIntArith Z3-alpha 2.69275
QF_Equality_LinearArith Yices2 2.667285
QF_Bitvec Z3-Owl 2.635574
QF_LinearIntArith Z3-alpha-base 2.63268
QF_Bitvec bv_decide 2.624624
Arith Z3-alpha-base 2.60121
QF_Bitvec Z3-Owl-base 2.566009
Equality_LinearArith cvc5 2.552562
QF_NonLinearIntArith z3siri 2.547756
Bitvec cvc5 2.52806
QF_NonLinearIntArith Z3-alpha-base 2.527296
Arith Z3-alpha 2.521893
QF_NonLinearIntArith z3siri-base 2.512135
QF_LinearRealArith Yices2 2.484686
QF_LinearRealArith OpenSMT 2.478286
QF_NonLinearRealArith SMT-RAT 2.416204
QF_LinearIntArith SMTInterpol 2.388914
QF_LinearRealArith cvc5 2.370754
QF_LinearRealArith Z3-alpha-base 2.364503
QF_Equality_Bitvec SMTInterpol 2.262531
QF_NonLinearIntArith Yices2 2.231268
Arith cvc5 2.216909
Arith YicesQS 2.216909
Bitvec YicesQS 2.189681
QF_LinearRealArith Z3-alpha 2.121223
Bitvec Bitwuzla 1.963529
QF_NonLinearIntArith cvc5 1.963353
QF_LinearRealArith SMTInterpol 1.75944
Equality_NonLinearArith cvc5 1.730677
Arith UltimateEliminator+MathSAT 1.649241
Equality_LinearArith iProver v3.9.3 1.498317
QF_Equality_NonLinearArith Yices2 1.424062
QF_FPArith colibri2 1.401006
Equality_MachineArith cvc5 1.322942
QF_Equality_NonLinearArith cvc5 1.020831
QF_Datatypes cvc5 0.991872
QF_Equality_NonLinearArith SMTInterpol 0.658486
Equality_NonLinearArith iProver v3.9.3 0.61038
QF_FPArith Z3-Owl 0.583862
Equality cvc5 0.546785
QF_FPArith Z3-Owl-base 0.512659
Equality_MachineArith SMTInterpol 0.35976
QF_Datatypes SMTInterpol 0.338675
Equality_NonLinearArith SMTInterpol 0.327472
Bitvec UltimateEliminator+MathSAT 0.314914
QF_Bitvec SMTInterpol 0.299305
Bitvec SMTInterpol 0.220255
Equality iProver v3.9.3 0.208337
Arith iProver v3.9.3 0.146281
QF_NonLinearRealArith SMTInterpol 0.110033
Arith SMTInterpol 0.074297
FPArith UltimateEliminator+MathSAT 0.070698
Equality_MachineArith Bitwuzla 0.043489
Equality Yices2 0.019418
Equality SMTInterpol 0.018703
Equality_NonLinearArith UltimateEliminator+MathSAT 0.014676
Arith SMT-RAT 0.010697
Equality_MachineArith UltimateEliminator+MathSAT 0.00765
Equality_LinearArith UltimateEliminator+MathSAT 0.000944
QF_NonLinearIntArith SMTInterpol 0.000178
Equality UltimateEliminator+MathSAT 0
QF_FPArith COLIBRI -6.40824
Arith Amaya -6.44335
Equality_LinearArith SMTInterpol -8.457622

Parallel Performance

Division Solver Contribution
QF_Strings Z3-Noodler-Mocha 4.503171
QF_Strings Z3-Noodler 4.378626
QF_Strings Z3-Noodler-Mocha-base 4.366658
QF_Strings OSTRICH 4.1591
QF_Bitvec Bitwuzla-MachBV 3.895111
QF_Bitvec Bitwuzla 3.876625
QF_Bitvec Yices2 3.871457
QF_Bitvec Bitwuzla-MachBV-base 3.86703
QF_Equality_Bitvec Bitwuzla 3.736878
QF_Equality_Bitvec Yices2 3.692774
QF_Strings cvc5 3.640918
QF_Equality Yices2 3.582177
QF_Equality OpenSMT 3.580302
QF_Equality cvc5 3.578428
QF_Equality_Bitvec Z3-Owl 3.538279
QF_Equality_Bitvec cvc5 3.497113
QF_Bitvec cvc5 3.474071
QF_Equality SMTInterpol 3.43742
QF_Equality_Bitvec Z3-Owl-base 3.380212
QF_Strings Z3-alpha 3.373692
QF_Strings Z3-alpha-base 3.350193
QF_Strings Z3-Noodler-base 3.334725
QF_LinearIntArith OpenSMT 3.102205
QF_Bitvec Z3-alpha 3.088303
QF_FPArith Bitwuzla 3.049823
QF_Bitvec z3siri 3.047568
QF_LinearIntArith Yices2 2.997634
QF_NonLinearRealArith Z3-alpha 2.989441
QF_LinearIntArith cvc5 2.988723
QF_NonLinearRealArith z3siri-base 2.937623
QF_NonLinearRealArith Z3-alpha-base 2.937623
QF_FPArith cvc5 2.933724
FPArith Bitwuzla 2.929808
QF_LinearIntArith Z3-alpha 2.928916
QF_NonLinearRealArith z3siri 2.847523
QF_Equality_LinearArith SMTInterpol 2.835018
QF_Equality_LinearArith cvc5 2.825566
QF_Bitvec Z3-alpha-base 2.814501
QF_Bitvec z3siri-base 2.813872
QF_NonLinearRealArith cvc5 2.772844
QF_Equality_LinearArith OpenSMT 2.772299
QF_NonLinearIntArith Z3-alpha 2.762918
QF_Bitvec bv_decide-nokernel 2.762512
FPArith cvc5 2.751887
QF_NonLinearRealArith Yices2 2.73289
QF_Equality_LinearArith Yices2 2.667285
Arith Z3-alpha 2.66414
QF_Bitvec Z3-Owl 2.635574
QF_LinearIntArith Z3-alpha-base 2.63268
QF_Bitvec bv_decide 2.624624
Arith Z3-alpha-base 2.60121
QF_Bitvec Z3-Owl-base 2.566009
Equality_LinearArith cvc5 2.552562
QF_NonLinearIntArith z3siri 2.547756
Bitvec cvc5 2.52806
QF_NonLinearIntArith Z3-alpha-base 2.527296
QF_NonLinearIntArith z3siri-base 2.512135
QF_LinearRealArith Yices2 2.484686
QF_LinearRealArith OpenSMT 2.478286
QF_NonLinearRealArith SMT-RAT 2.416204
QF_LinearIntArith SMTInterpol 2.392896
QF_LinearRealArith cvc5 2.370754
QF_LinearRealArith Z3-alpha-base 2.364503
QF_LinearRealArith Z3-alpha 2.35826
QF_Equality_Bitvec SMTInterpol 2.270264
QF_NonLinearIntArith Yices2 2.231268
Arith cvc5 2.216909
Arith YicesQS 2.216909
Bitvec YicesQS 2.189681
Bitvec Bitwuzla 1.963529
QF_NonLinearIntArith cvc5 1.963353
QF_LinearRealArith SMTInterpol 1.775643
Equality_NonLinearArith cvc5 1.730677
Equality_LinearArith iProver v3.9.3 1.655627
Arith UltimateEliminator+MathSAT 1.649241
QF_Equality_NonLinearArith Yices2 1.424062
QF_FPArith colibri2 1.401006
Equality_MachineArith cvc5 1.322942
QF_Equality_NonLinearArith cvc5 1.020831
QF_Datatypes cvc5 0.991872
Equality_NonLinearArith iProver v3.9.3 0.779408
QF_Equality_NonLinearArith SMTInterpol 0.658486
QF_FPArith Z3-Owl 0.583862
Equality cvc5 0.546785
QF_FPArith Z3-Owl-base 0.512659
Equality_MachineArith SMTInterpol 0.35976
QF_Datatypes SMTInterpol 0.342175
Equality_NonLinearArith SMTInterpol 0.327472
Bitvec UltimateEliminator+MathSAT 0.314914
QF_Bitvec SMTInterpol 0.300949
Equality iProver v3.9.3 0.242307
Bitvec SMTInterpol 0.220255
Arith iProver v3.9.3 0.215619
QF_NonLinearRealArith SMTInterpol 0.110033
Arith SMTInterpol 0.074297
FPArith UltimateEliminator+MathSAT 0.070698
Equality_MachineArith Bitwuzla 0.043489
Equality Yices2 0.019418
Equality SMTInterpol 0.01894
Equality_NonLinearArith UltimateEliminator+MathSAT 0.014676
Arith SMT-RAT 0.010697
Equality_MachineArith UltimateEliminator+MathSAT 0.00765
Equality_LinearArith UltimateEliminator+MathSAT 0.000944
QF_NonLinearIntArith SMTInterpol 0.000178
Equality UltimateEliminator+MathSAT 0
QF_FPArith COLIBRI -6.40824
Arith Amaya -6.44335
Equality_LinearArith SMTInterpol -8.457622

SAT Performance

Division Solver Contribution
QF_Strings Z3-Noodler-Mocha 1.889141
QF_Strings Z3-Noodler-Mocha-base 1.888286
QF_Strings Z3-Noodler 1.888286
QF_Strings OSTRICH 1.779117
QF_Equality_Bitvec Bitwuzla 1.599228
QF_Equality_Bitvec Yices2 1.596277
QF_Strings cvc5 1.591024
QF_Equality_Bitvec Z3-Owl 1.5384
QF_Equality_Bitvec Z3-Owl-base 1.518194
QF_Equality_Bitvec cvc5 1.508428
QF_Strings Z3-alpha 1.413881
QF_Strings Z3-alpha-base 1.391775
QF_Strings Z3-Noodler-base 1.379911
QF_NonLinearIntArith Z3-alpha 1.230033
QF_LinearIntArith Z3-alpha 1.177754
QF_LinearIntArith OpenSMT 1.1666
QF_LinearIntArith cvc5 1.126613
QF_LinearIntArith Yices2 1.12593
QF_NonLinearIntArith Z3-alpha-base 1.080035
QF_NonLinearIntArith z3siri 1.076957
QF_NonLinearIntArith z3siri-base 1.072518
QF_NonLinearIntArith Yices2 1.06231
QF_LinearIntArith Z3-alpha-base 1.052031
QF_Equality_NonLinearArith Yices2 0.994213
QF_Equality_LinearArith SMTInterpol 0.992795
QF_NonLinearIntArith cvc5 0.971661
QF_Equality_LinearArith cvc5 0.932167
QF_Equality_LinearArith OpenSMT 0.880465
QF_Equality_Bitvec SMTInterpol 0.861878
QF_Bitvec Bitwuzla 0.855285
QF_Bitvec Bitwuzla-MachBV 0.854591
QF_Bitvec Bitwuzla-MachBV-base 0.854244
QF_Bitvec Yices2 0.852858
QF_Equality_LinearArith Yices2 0.845667
QF_LinearIntArith SMTInterpol 0.82596
QF_Bitvec cvc5 0.807071
QF_Bitvec bv_decide-nokernel 0.781332
QF_NonLinearRealArith Z3-alpha 0.764107
QF_LinearRealArith OpenSMT 0.759386
QF_Bitvec bv_decide 0.753078
QF_LinearRealArith Yices2 0.748802
QF_NonLinearRealArith z3siri-base 0.744241
QF_NonLinearRealArith Z3-alpha-base 0.744241
QF_Bitvec Z3-alpha 0.741728
QF_NonLinearRealArith z3siri 0.723611
QF_LinearRealArith Z3-alpha-base 0.717497
QF_Bitvec Z3-Owl 0.712621
QF_NonLinearRealArith Yices2 0.702263
QF_Bitvec z3siri-base 0.701896
QF_Bitvec Z3-alpha-base 0.701896
QF_LinearRealArith Z3-alpha 0.696998
QF_LinearRealArith cvc5 0.693611
QF_Bitvec z3siri 0.691876
QF_NonLinearRealArith cvc5 0.663463
QF_Equality SMTInterpol 0.644702
QF_Equality cvc5 0.644702
QF_Equality OpenSMT 0.644702
QF_Equality Yices2 0.644702
QF_Bitvec Z3-Owl-base 0.644661
QF_LinearRealArith SMTInterpol 0.640531
QF_Equality_NonLinearArith cvc5 0.616151
QF_NonLinearRealArith SMT-RAT 0.608739
QF_FPArith Bitwuzla 0.455096
QF_FPArith cvc5 0.446085
QF_Equality_NonLinearArith SMTInterpol 0.405067
Arith Z3-alpha 0.401316
Arith Z3-alpha-base 0.39452
Arith YicesQS 0.383767
Arith cvc5 0.322369
FPArith Bitwuzla 0.306126
FPArith cvc5 0.25246
Arith UltimateEliminator+MathSAT 0.231925
QF_FPArith colibri2 0.202265
QF_Datatypes cvc5 0.168897
Bitvec Bitwuzla 0.150138
Bitvec YicesQS 0.14756
Bitvec cvc5 0.141214
QF_FPArith Z3-Owl 0.139625
QF_FPArith Z3-Owl-base 0.12028
Equality_MachineArith cvc5 0.064713
Equality cvc5 0.046903
Equality_NonLinearArith cvc5 0.019417
QF_Datatypes SMTInterpol 0.019041
QF_Bitvec SMTInterpol 0.012495
Equality_LinearArith cvc5 0.011057
Equality iProver v3.9.3 0.010279
FPArith UltimateEliminator+MathSAT 0.010138
Equality_MachineArith Bitwuzla 0.008531
Equality_NonLinearArith UltimateEliminator+MathSAT 0.007214
Equality_LinearArith SMTInterpol 0.00464
Equality_MachineArith UltimateEliminator+MathSAT 0.00434
Bitvec UltimateEliminator+MathSAT 0.002856
Arith SMTInterpol 0.000464
Equality_LinearArith UltimateEliminator+MathSAT 0.000377
Equality_NonLinearArith SMTInterpol 0.000245
Equality Yices2 0.000203
QF_NonLinearRealArith SMTInterpol 0.000175
Equality_MachineArith SMTInterpol 0.000114
Equality SMTInterpol 1.9e-05
Arith SMT-RAT 1.9e-05
Bitvec SMTInterpol 3e-06
QF_NonLinearIntArith SMTInterpol 1e-06
Equality_LinearArith iProver v3.9.3 0
Arith iProver v3.9.3 0
Equality_NonLinearArith iProver v3.9.3 0
Equality UltimateEliminator+MathSAT 0
QF_FPArith COLIBRI -6.40824
Arith Amaya -6.44335

UNSAT Performance

Division Solver Contribution
Equality_LinearArith cvc5 2.227623
Equality_LinearArith iProver v3.9.3 1.655627
Bitvec cvc5 1.474288
Equality_NonLinearArith cvc5 1.383464
FPArith Bitwuzla 1.341849
FPArith cvc5 1.337323
Bitvec YicesQS 1.200387
QF_Equality Yices2 1.187513
QF_Equality OpenSMT 1.186434
QF_Equality cvc5 1.185355
QF_FPArith Bitwuzla 1.148682
QF_Equality SMTInterpol 1.1048
QF_Bitvec Bitwuzla-MachBV 1.100742
QF_FPArith cvc5 1.091849
QF_Bitvec Yices2 1.090142
QF_Bitvec Bitwuzla 1.090142
QF_Bitvec Bitwuzla-MachBV-base 1.086229
Bitvec Bitwuzla 1.027758
Arith Z3-alpha 0.99745
Arith Z3-alpha-base 0.96967
QF_Bitvec cvc5 0.932219
Arith cvc5 0.848524
QF_Bitvec z3siri 0.835283
QF_Bitvec Z3-alpha 0.803032
Equality_MachineArith cvc5 0.802468
Equality_NonLinearArith iProver v3.9.3 0.779408
QF_FPArith COLIBRI 0.757579
Arith YicesQS 0.755925
QF_NonLinearRealArith Z3-alpha 0.730799
QF_NonLinearRealArith z3siri-base 0.724636
QF_NonLinearRealArith Z3-alpha-base 0.724636
QF_NonLinearRealArith cvc5 0.723611
QF_Bitvec Z3-alpha-base 0.705357
QF_Bitvec z3siri-base 0.705042
QF_NonLinearRealArith z3siri 0.700246
QF_NonLinearRealArith Yices2 0.664444
Arith UltimateEliminator+MathSAT 0.644235
QF_Bitvec Z3-Owl-base 0.638352
QF_Bitvec Z3-Owl 0.607271
QF_Bitvec bv_decide-nokernel 0.605519
QF_NonLinearRealArith SMT-RAT 0.599381
QF_Bitvec bv_decide 0.565908
QF_Strings Z3-Noodler-Mocha 0.558917
QF_FPArith colibri2 0.538613
QF_Equality_LinearArith OpenSMT 0.52808
QF_Strings Z3-Noodler 0.516052
QF_Strings Z3-Noodler-Mocha-base 0.511948
QF_Equality_LinearArith cvc5 0.511874
QF_Equality_LinearArith Yices2 0.509198
QF_LinearRealArith Yices2 0.505457
QF_LinearRealArith cvc5 0.499697
QF_Strings OSTRICH 0.497803
QF_LinearRealArith OpenSMT 0.49397
QF_LinearRealArith Z3-alpha 0.491118
QF_LinearRealArith Z3-alpha-base 0.476986
QF_Equality_LinearArith SMTInterpol 0.472464
QF_LinearIntArith OpenSMT 0.464054
QF_LinearIntArith Yices2 0.449261
QF_Equality_Bitvec Bitwuzla 0.446885
QF_LinearIntArith cvc5 0.445385
QF_Equality_Bitvec Yices2 0.433255
QF_Strings Z3-Noodler-base 0.424357
QF_Strings Z3-alpha-base 0.423304
QF_Strings Z3-alpha 0.419508
QF_Strings cvc5 0.4183
QF_Equality_Bitvec cvc5 0.412005
QF_Equality_Bitvec Z3-Owl 0.410508
QF_LinearIntArith SMTInterpol 0.407141
QF_LinearIntArith Z3-alpha 0.392081
QF_Equality_Bitvec Z3-Owl-base 0.367703
QF_LinearIntArith Z3-alpha-base 0.356251
Equality_MachineArith SMTInterpol 0.347059
QF_Datatypes cvc5 0.342175
QF_Equality_Bitvec SMTInterpol 0.334507
QF_NonLinearIntArith z3siri 0.311815
Equality_NonLinearArith SMTInterpol 0.309798
QF_NonLinearIntArith Z3-alpha 0.305958
QF_NonLinearIntArith Z3-alpha-base 0.30305
QF_NonLinearIntArith z3siri-base 0.301782
QF_LinearRealArith SMTInterpol 0.283237
Equality cvc5 0.273401
Bitvec UltimateEliminator+MathSAT 0.257787
Bitvec SMTInterpol 0.21869
Arith iProver v3.9.3 0.215619
QF_NonLinearIntArith Yices2 0.214423
QF_Datatypes SMTInterpol 0.19978
QF_Bitvec SMTInterpol 0.190801
QF_NonLinearIntArith cvc5 0.172614
Equality iProver v3.9.3 0.152775
QF_FPArith Z3-Owl 0.152447
QF_FPArith Z3-Owl-base 0.1363
QF_NonLinearRealArith SMTInterpol 0.101422
Arith Amaya 0.076665
Arith SMTInterpol 0.063015
QF_Equality_NonLinearArith cvc5 0.050809
QF_Equality_NonLinearArith Yices2 0.038509
QF_Equality_NonLinearArith SMTInterpol 0.030633
FPArith UltimateEliminator+MathSAT 0.027292
Equality SMTInterpol 0.017771
Equality Yices2 0.015653
Equality_MachineArith Bitwuzla 0.013497
Arith SMT-RAT 0.009824
Equality_NonLinearArith UltimateEliminator+MathSAT 0.001311
Equality_MachineArith UltimateEliminator+MathSAT 0.000466
QF_NonLinearIntArith SMTInterpol 0.000148
Equality_LinearArith UltimateEliminator+MathSAT 0.000128
Equality UltimateEliminator+MathSAT 0
Equality_LinearArith SMTInterpol -8.457622

24 seconds Performance

Division Solver Contribution
QF_Strings Z3-Noodler-Mocha 4.489188
QF_Strings Z3-Noodler 4.358861
QF_Strings Z3-Noodler-Mocha-base 4.347698
QF_Bitvec Bitwuzla-MachBV 3.588967
QF_Equality Yices2 3.576554
QF_Equality_Bitvec Bitwuzla 3.568208
QF_Equality OpenSMT 3.531731
QF_Bitvec Bitwuzla 3.530933
QF_Equality cvc5 3.518711
QF_Bitvec Bitwuzla-MachBV-base 3.505604
QF_Bitvec Yices2 3.453825
QF_Equality_Bitvec Yices2 3.384506
QF_Equality SMTInterpol 3.373436
QF_Equality_Bitvec Z3-Owl 3.23751
QF_Strings Z3-alpha 3.139316
QF_Strings cvc5 3.092534
QF_Strings Z3-Noodler-base 3.072218
QF_Strings Z3-alpha-base 3.066115
QF_Strings OSTRICH 3.024859
QF_Equality_Bitvec Z3-Owl-base 3.004893
QF_FPArith Bitwuzla 2.737822
QF_LinearIntArith Yices2 2.679902
QF_Equality_Bitvec cvc5 2.654697
QF_NonLinearRealArith Z3-alpha 2.622561
QF_Equality_LinearArith SMTInterpol 2.561301
QF_Bitvec cvc5 2.540237
QF_Equality_LinearArith Yices2 2.513567
QF_NonLinearRealArith Yices2 2.512597
FPArith Bitwuzla 2.483116
FPArith cvc5 2.440172
QF_Equality_LinearArith OpenSMT 2.373058
QF_Equality_LinearArith cvc5 2.373058
Equality_LinearArith cvc5 2.32693
Arith Z3-alpha 2.324045
QF_NonLinearRealArith cvc5 2.277874
QF_LinearIntArith Z3-alpha 2.239078
QF_NonLinearIntArith Z3-alpha 2.235206
Arith Z3-alpha-base 2.210497
Arith YicesQS 2.204094
QF_Bitvec Z3-alpha 2.104016
QF_FPArith cvc5 2.09898
QF_NonLinearRealArith Z3-alpha-base 2.082366
QF_NonLinearRealArith z3siri-base 2.082366
QF_NonLinearIntArith Yices2 2.000445
Bitvec YicesQS 1.977596
QF_NonLinearIntArith Z3-alpha-base 1.954595
QF_NonLinearIntArith z3siri-base 1.932556
QF_LinearIntArith Z3-alpha-base 1.921698
QF_Bitvec z3siri 1.91945
QF_NonLinearRealArith SMT-RAT 1.915574
QF_Bitvec Z3-alpha-base 1.900787
QF_Bitvec z3siri-base 1.897169
QF_NonLinearRealArith z3siri 1.844588
QF_LinearRealArith Yices2 1.802814
Bitvec Bitwuzla 1.749701
QF_Bitvec Z3-Owl 1.71524
QF_LinearRealArith OpenSMT 1.679536
QF_LinearIntArith OpenSMT 1.635966
Arith cvc5 1.583498
Arith UltimateEliminator+MathSAT 1.500558
QF_LinearIntArith cvc5 1.48245
QF_Bitvec Z3-Owl-base 1.472935
QF_Equality_Bitvec SMTInterpol 1.424737
QF_LinearRealArith cvc5 1.412081
QF_NonLinearIntArith z3siri 1.35544
QF_LinearRealArith Z3-alpha-base 1.345303
Bitvec cvc5 1.324195
Equality_NonLinearArith cvc5 1.32201
QF_Bitvec bv_decide-nokernel 1.287087
QF_FPArith colibri2 1.261642
QF_LinearIntArith SMTInterpol 1.184752
QF_LinearRealArith Z3-alpha 1.167808
QF_Bitvec bv_decide 1.140448
Equality_LinearArith iProver v3.9.3 1.111824
QF_Equality_NonLinearArith Yices2 0.891259
Equality_MachineArith cvc5 0.86174
QF_LinearRealArith SMTInterpol 0.831842
QF_NonLinearIntArith cvc5 0.61054
QF_Equality_NonLinearArith cvc5 0.571207
Equality_NonLinearArith iProver v3.9.3 0.37189
Equality_MachineArith SMTInterpol 0.319065
Equality_NonLinearArith SMTInterpol 0.316808
QF_Equality_NonLinearArith SMTInterpol 0.316064
QF_FPArith Z3-Owl 0.295625
Bitvec UltimateEliminator+MathSAT 0.291017
QF_FPArith Z3-Owl-base 0.252326
Bitvec SMTInterpol 0.21869
Equality cvc5 0.187987
QF_Bitvec SMTInterpol 0.135821
QF_Datatypes SMTInterpol 0.123183
Equality iProver v3.9.3 0.11882
QF_NonLinearRealArith SMTInterpol 0.104124
QF_Datatypes cvc5 0.093622
Arith iProver v3.9.3 0.089062
Arith SMTInterpol 0.072546
FPArith UltimateEliminator+MathSAT 0.044172
Equality_MachineArith Bitwuzla 0.032099
Equality_NonLinearArith UltimateEliminator+MathSAT 0.013333
Equality Yices2 0.012972
Arith SMT-RAT 0.010697
Equality SMTInterpol 0.008524
Equality_MachineArith UltimateEliminator+MathSAT 0.007611
Equality_LinearArith UltimateEliminator+MathSAT 0.000944
QF_NonLinearIntArith SMTInterpol 0.000137
Equality UltimateEliminator+MathSAT 0
QF_FPArith COLIBRI -6.40824
Arith Amaya -6.44335
Equality_LinearArith SMTInterpol -8.457622