Benchmark Properties Interpolation Properties iPrincess Results QE Results
Name Status Difficulty Category L/R Ratio (%) #C #LC Dec. Time (ms) IS Time (ms) IS Time (ms)
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 10 28 1 1816 39 244 10 12
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 20 28 2 1816 97 128 36 23
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 30 28 4 1816 132 114 92 44
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 40 28 6 1816 164 131 256 95
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 50 28 8 1816 110 205 448 195
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 60 28 12 1816 103 90 363 291
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 70 28 14 1816 67 94 351 315
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 80 28 17 1816 36 81 252 304
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_2.msat.pri unsat 0 industrial 90 28 21 1816 50 161 281 387
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 10 38 2 3993 253 643 29 25
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 20 38 4 3993 489 328 99 38
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 30 38 6 3993 614 213 412 135
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 40 38 9 3993 737 185 2171 380
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 50 38 13 3993 561 302 2885 667
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 60 38 16 3993 389 250 3503 1434
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 70 38 22 3993 292 306 1831 1210
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 80 38 25 3993 163 282 867 909
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_3.msat.pri unsat 0 industrial 90 38 30 3993 103 185 1518 842
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 10 48 2 9016 1509 1580 35 15
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 20 48 5 9016 2386 1124 231 38
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 30 48 8 9016 2898 985 1728 240
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 40 48 12 9016 3388 880 16105 2049
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 50 48 16 9016 2741 829 17106 2476
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 60 48 21 9016 1923 767 14387 5268
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 70 48 27 9016 1161 790 12155 5186
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 80 48 32 9016 931 686 8211 11570
CIRC/simplebitadder/SIMPLEBITADDER_COMPOSE_4.msat.pri unsat 0 industrial 90 48 40 9016 621 930 4262 6504
CIRC/multiplier/MULTIPLIER_2.msat.pri unsat 0 industrial 30 18 2 1325 42 190 33 25
CIRC/multiplier/MULTIPLIER_2.msat.pri unsat 0 industrial 40 18 4 1325 21 538 31 39
CIRC/multiplier/MULTIPLIER_2.msat.pri unsat 0 industrial 50 18 6 1325 30 543 41 69
CIRC/multiplier/MULTIPLIER_2.msat.pri unsat 0 industrial 60 18 8 1325 46 205 41 27
CIRC/multiplier/MULTIPLIER_2.msat.pri unsat 0 industrial 70 18 10 1325 57 172 113 84
CIRC/multiplier/MULTIPLIER_2.msat.pri unsat 0 industrial 80 18 11 1325 211 617 125 78
CIRC/multiplier/MULTIPLIER_2.msat.pri unsat 0 industrial 90 18 15 1325 1 30 60 97
CIRC/multiplier/MULTIPLIER_3.msat.pri unsat 0 industrial 20 24 2 2415 57 437 - T/O
Statistics
Number of benchmarks: 35
Number of benchmarks on which iPrincess is faster: 18
Number of benchmarks on which iPrincess is at least 1 order of magnitude faster: 2
Number of benchmarks on which iPrincess yields smaller interpolants: 23
Number of benchmarks on which iPrincess yiels interpolants that are 1 order of magnitude smaller: 4
Legend
L/R Ratio: Ratio of the number of conjuncts on the left and on the right part of the formula
#C: Number of constants in the input formula
#LC: Number of local constants in the input formula (constants occuring in the left part of the formula only)
IS: Size of the generated interpolant (number of operators)
T/O: Timeout
O/M: Out of Memory