Category | Problems | CHC2SMT-LIB user time | CHC2SMT-LIB system time | Z3 user time | Z3 system time | answer | Fixedpoint engine | ||
01.NLIN | 01.01_ackermann.enc.pl | 50 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
01.NLIN | 01.02_ackermann-faulty.enc.pl | 50 | 0 | 140 | 20 | false | z3-duality | ||
01.NLIN | 01.03_mccarthy91.enc.pl | 20 | 10 | 14870 | 380 | true | z3-duality | ||
01.NLIN | 01.04_ack_drec_iterec.enc.pl | 10 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
01.NLIN | 01.05_ack_drec_mirror.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
01.NLIN | 01.06_ack-eh.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
01.NLIN | 01.07_ack-p.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
01.NLIN | 01.08_B.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
01.NLIN | 01.09_fusc.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
01.NLIN | 01.10_G.enc.pl | 30 | 0 | 0 | 10 | true | z3-duality | ||
01.NLIN | 01.11_hanoi.enc.pl | 20 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
01.NLIN | 01.12_mc91itrec.enc.pl | 40 | 0 | 670 | 20 | true | z3-duality | ||
01.NLIN | 01.13_sudan.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.01_add-horn.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.02_barthe.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.03_barthe2.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.04_bug15.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.05_cube.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.06_digits10.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.07_fib.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.08_loop.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.09_loop2.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.10_loop3.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.11_loop4.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.12_nested-while.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.13_product.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.14_simple-loop.enc.pl | 30 | 0 | 980 | 60 | true | z3-duality | ||
02.MON | 02.15_square.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.16_sum.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.17_upcount.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
02.MON | 02.18_while-if.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.01_add-horn.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.02_fib.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.03_loop.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.04_loop2.enc.pl | 20 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.05_loop3.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.06_loop4.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.07_product.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.08_square.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.09_sum.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.10_upcount.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
03.INJ | 03.11_while-if.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
04.FUN | 04.01_add-horn.enc.pl | 30 | 10 | 70 | 10 | true | z3-duality | ||
04.FUN | 04.02_bug15.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
04.FUN | 04.03_fib.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
04.FUN | 04.04_nested-while.enc.pl | 50 | 0 | 110 | 30 | true | z3-duality | ||
04.FUN | 04.05_simple-loop.enc.pl | 30 | 0 | 990 | 50 | true | z3-duality | ||
04.FUN | 04.06_upcount.enc.pl | 20 | 20 | 120 | 10 | true | z3-duality | ||
04.FUN | 04.07_while-if.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.01_limit2.enc.pl | 40 | 0 | 297030 | 2340 | solver_timeout | z3-duality | ||
05.NINT | 05.02_limit3.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.03_loop1.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.04_loop2.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.05_loop3.enc.pl | 40 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.06_loopunswitch.enc.pl | 50 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.07_nonint1.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.08_nonint1-hard.enc.pl | 30 | 0 | 40 | 10 | true | z3-duality | ||
05.NINT | 05.09_nonint2.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.10_nonint2-hard.enc.pl | 20 | 10 | 60 | 0 | false | z3-duality | ||
05.NINT | 05.11_nonint3.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.12_nonint3-hard.enc.pl | 20 | 0 | 140 | 20 | true | z3-duality | ||
05.NINT | 05.13_strengthred.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.14_sum01.enc.pl | 40 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.15_sumupto1.enc.pl | 40 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.16_sumupto2.enc.pl | 50 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.17_upcount.enc.pl | 50 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
05.NINT | 05.18_whileif.enc.pl | 40 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.01_code-sinking.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.02_condrem.enc.pl | 20 | 10 | 0 | 10 | solver_timeout | z3-duality | ||
06.LOPT | 06.03_countingloop.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.04_ex1.enc.pl | 40 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.05_lf.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.06_licm.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.07_loop-peeling.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.08_loop-reversal.enc.pl | 20 | 10 | 0 | 10 | solver_timeout | z3-duality | ||
06.LOPT | 06.09_loop-tiling09.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.10_loop-unswitching.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.11_pre01.enc.pl | 20 | 10 | 60 | 10 | true | z3-duality | ||
06.LOPT | 06.12_spin13-ex.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.13_strength-reduction.enc.pl | 20 | 10 | 0 | 10 | solver_timeout | z3-duality | ||
06.LOPT | 06.14_sw-pipelining.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.15_lf2.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.16_loop-flattening.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.17_loop-interchange.enc.pl | 30 | 10 | 4560 | 200 | true | z3-duality | ||
06.LOPT | 06.18_loop-skewing.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.19_loop-tiling02.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
06.LOPT | 06.20_loop-unroll01.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.01_barthe.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.02_barthe2.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.03_barthe2-big.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.04_barthe2-big2.enc.pl | 30 | 20 | 0 | 10 | solver_timeout | z3-duality | ||
07.ITE | 07.05_barthe-faulty.enc.pl | 30 | 20 | 24580 | 630 | false | z3-duality | ||
07.ITE | 07.06_bug15.enc.pl | 40 | 0 | 180 | 10 | true | z3-duality | ||
07.ITE | 07.07_digits10.enc.pl | 60 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.08_digits10_inl.enc.pl | 70 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.09_fib.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.10_invarianthoisting.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.11_loop.enc.pl | 20 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.12_loop2.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.13_loop3.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.14_loop4.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.15_loop5.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.16_loop5-faulty.enc.pl | 30 | 10 | 80 | 0 | false | z3-duality | ||
07.ITE | 07.17_nested-while.enc.pl | 40 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.18_nested-while-faulty.enc.pl | 40 | 10 | 140 | 30 | false | z3-duality | ||
07.ITE | 07.19_simple-loop.enc.pl | 20 | 10 | 940 | 80 | true | z3-duality | ||
07.ITE | 07.20_upcount.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.21_while-if.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
07.ITE | 07.22_su_sq.hm.enc.pl | 10 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
08.ARR | 08.01_fib.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
08.ARR | 08.02_findmax.enc.pl | 50 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
08.ARR | 08.03_loopalign.enc.pl | 40 | 10 | 177990 | 5110 | error (*) | z3-duality | ||
08.ARR | 08.04_looppipe.enc.pl | 40 | 10 | 7180 | 270 | true | z3-duality | ||
08.ARR | 08.05_propagate.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
08.ARR | 08.06_gtemaxarray.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.01_add-horn.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.02_add-horn-faulty.enc.pl | 40 | 10 | 230 | 30 | false | z3-duality | ||
09.REC | 09.03_cocome1.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.04_inlining.enc.pl | 40 | 10 | 140 | 10 | true | z3-duality | ||
09.REC | 09.05_inlining-faulty.enc.pl | 40 | 10 | 100 | 0 | false | z3-duality | ||
09.REC | 09.06_limit1.enc.pl | 20 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.07_limit1-faulty.enc.pl | 40 | 0 | 10 | 0 | false | z3-duality | ||
09.REC | 09.08_limit1unrolled.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.09_limit2.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.10_limit2-faulty.enc.pl | 40 | 0 | 2150 | 80 | false | z3-duality | ||
09.REC | 09.11_limit3.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.12_loop_rec.enc.pl | 40 | 0 | 140 | 0 | true | z3-duality | ||
09.REC | 09.13_triangular.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.14_triangular-mod.enc.pl | 50 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
09.REC | 09.15_triangular-mod-faulty.enc.pl | 40 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
10.I-R | 10.01_gcd.enc.pl | 60 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
10.I-R | 10.02_sumprod.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
10.I-R | 10.03_triangular_nontail.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
10.I-R | 10.04_triangular_tail.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.01_array_copy.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.02_array_copy_max.enc.pl | 30 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.03_array_sum.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.04_array_sum_k.enc.pl | 40 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.05_sum_upto.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.06_sum_upto_mult.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.07_sum_upto_mult_MON.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.08_twice_array_sum.enc.pl | 30 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.09_two_arrays_sum.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
11.COMP | 11.10_two_array_sum_diffsize.enc.pl | 60 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.01_bdiv.enc.pl | 40 | 10 | 680 | 40 | true | z3-duality | ||
12.PCOR | 12.02_fast_mult2.enc.pl | 40 | 0 | 120 | 10 | true | z3-duality | ||
12.PCOR | 12.03_fast_mult3.enc.pl | 40 | 10 | 260 | 30 | true | z3-duality | ||
12.PCOR | 12.04_fibonacci.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.05_fusc.enc.pl | 30 | 10 | 120 | 20 | true | z3-duality | ||
12.PCOR | 12.06_gcd.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.07_idiv.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.08_imc91rec.enc.pl | 30 | 0 | 81870 | 780 | true | z3-duality | ||
12.PCOR | 12.09_imult.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.10_remainder.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.11_sumfirst.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.12_lucas.enc.pl | 20 | 10 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.13_padovan.enc.pl | 30 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.14_perrin.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.15_hanoi.enc.pl | 40 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.16_digits10.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.17_digits10-itmd.enc.pl | 50 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.18_digits10-opt.enc.pl | 60 | 0 | 0 | 0 | solver_timeout | z3-duality | ||
12.PCOR | 12.19_digits10-opt100.enc.pl | 20 | 20 | 0 | 0 | solver_timeout | z3-duality | ||
(*) (error "query failed: Formulas should not contain unbound variables") | |||||||||