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) |

check/bignum_lia1.pri | unsat | 0 | check | 40 | 6 | 1 | 666 | 18 | 76 | 2 | 77 |

check/bignum_lia1.pri | unsat | 0 | check | 50 | 6 | 2 | 666 | 18 | 54 | 2 | 12 |

check/bignum_lia1.pri | unsat | 0 | check | 60 | 6 | 3 | 666 | 18 | 56 | 2 | 29 |

check/bignum_lia1.pri | unsat | 0 | check | 70 | 6 | 4 | 666 | 12 | 32 | 2 | 26 |

check/bignum_lia1.pri | unsat | 0 | check | 80 | 6 | 6 | 666 | 1 | 23 | 1 | 100 |

check/int_incompleteness2.pri | unsat | 0 | check | 50 | 4 | 2 | 193 | 10 | 40 | 5 | 15 |

check/int_incompleteness3.pri | unsat | 0 | check | 40 | 4 | 2 | 181 | 1 | 28 | 1 | 114 |

Statistics | |

Number of benchmarks: | 7 |

Number of benchmarks on which iPrincess is faster: | 3 |

Number of benchmarks on which iPrincess is at least 1 order of magnitude faster: | 0 |

Number of benchmarks on which iPrincess yields smaller interpolants: | 2 |

Number of benchmarks on which iPrincess yiels interpolants that are 1 order of magnitude smaller: | 0 |

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 |