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.transform.pl

130

20

2640

100

true

z3-duality

   

01.NLIN

01.02_ackermann-faulty.enc.transform.pl

180

10

280

30

false

z3-duality

   

01.NLIN

01.03_mccarthy91.enc.transform.pl

40

20

1490

60

true

z3-duality

   

01.NLIN

01.04_ack_drec_iterec.enc.transform.pl

40

0

720

40

true

z3-duality

   

01.NLIN

01.05_ack_drec_mirror.enc.transform.pl

40

0

350

30

true

z3-duality

   

01.NLIN

01.06_ack-eh.enc.transform.pl

40

0

2770

130

true

z3-duality

   

01.NLIN

01.07_ack-p.enc.transform.pl

20

10

560

10

true

z3-duality

   

01.NLIN

01.08_B.enc.transform.pl

20

0

70

10

true

z3-duality

   

01.NLIN

01.09_fusc.enc.transform.pl

30

20

40

0

true

z3-duality

   

01.NLIN

01.10_G.enc.transform.pl

30

0

500

30

true

z3-duality

   

01.NLIN

01.11_hanoi.enc.transform.pl

30

0

60

10

true

z3-duality

   

01.NLIN

01.12_mc91itrec.enc.transform.pl

40

0

1380

80

true

z3-duality

   

01.NLIN

01.13_sudan.enc.transform.pl

30

20

1670

60

true

z3-duality

   

02.MON

02.01_add-horn.enc.transform.pl

40

0

260

20

true

z3-duality

   

02.MON

02.02_barthe.enc.transform.pl

60

0

0

0

solver_timeout

z3-duality

   

02.MON

02.03_barthe2.enc.transform.pl

40

20

0

0

solver_timeout

z3-duality

   

02.MON

02.04_bug15.enc.transform.pl

30

0

70

0

true

z3-duality

   

02.MON

02.05_cube.enc.transform.pl

120

0

0

0

solver_timeout

z3-duality

   

02.MON

02.06_digits10.enc.transform.pl

40

0

280

30

true

z3-duality

   

02.MON

02.07_fib.enc.transform.pl

40

20

0

0

solver_timeout

z3-duality

   

02.MON

02.08_loop.enc.transform.pl

40

10

150

20

true

z3-duality

   

02.MON

02.09_loop2.enc.transform.pl

30

10

380

40

true

z3-duality

   

02.MON

02.10_loop3.enc.transform.pl

80

20

520

60

true

z3-duality

   

02.MON

02.11_loop4.enc.transform.pl

50

0

340

40

true

z3-duality

   

02.MON

02.12_nested-while.enc.transform.pl

50

0

230

20

true

z3-duality

   

02.MON

02.13_product.enc.transform.pl

50

0

0

0

solver_timeout

z3-duality

   

02.MON

02.14_simple-loop.enc.transform.pl

20

10

320

20

true

z3-duality

   

02.MON

02.15_square.enc.transform.pl

40

0

0

0

solver_timeout

z3-duality

   

02.MON

02.16_sum.enc.transform.pl

20

20

220

20

true

z3-duality

   

02.MON

02.17_upcount.enc.transform.pl

30

20

220

30

true

z3-duality

   

02.MON

02.18_while-if.enc.transform.pl

60

10

390

40

true

z3-duality

   

03.INJ

03.01_add-horn.enc.transform.pl

40

0

80

0

true

z3-duality

   

03.INJ

03.02_fib.enc.transform.pl

50

20

0

0

solver_timeout

z3-duality

   

03.INJ

03.03_loop.enc.transform.pl

40

10

130

30

true

z3-duality

   

03.INJ

03.04_loop2.enc.transform.pl

40

0

130

10

true

z3-duality

   

03.INJ

03.05_loop3.enc.transform.pl

80

20

210

20

true

z3-duality

   

03.INJ

03.06_loop4.enc.transform.pl

50

10

220

20

true

z3-duality

   

03.INJ

03.07_product.enc.transform.pl

50

0

0

0

solver_timeout

z3-duality

   

03.INJ

03.08_square.enc.transform.pl

40

10

0

0

solver_timeout

z3-duality

   

03.INJ

03.09_sum.enc.transform.pl

40

0

150

10

true

z3-duality

   

03.INJ

03.10_upcount.enc.transform.pl

50

0

150

10

true

z3-duality

   

03.INJ

03.11_while-if.enc.transform.pl

50

10

200

20

true

z3-duality

   

04.FUN

04.01_add-horn.enc.transform.pl

40

20

190

30

true

z3-duality

   

04.FUN

04.02_bug15.enc.transform.pl

40

0

70

0

true

z3-duality

   

04.FUN

04.03_fib.enc.transform.pl

30

0

120

0

true

z3-duality

   

04.FUN

04.04_nested-while.enc.transform.pl

230

0

350

50

true

z3-duality

   

04.FUN

04.05_simple-loop.enc.transform.pl

20

0

320

20

true

z3-duality

   

04.FUN

04.06_upcount.enc.transform.pl

30

10

90

10

true

z3-duality

   

04.FUN

04.07_while-if.enc.transform.pl

40

0

210

20

true

z3-duality

   

05.NINT

05.01_limit2.enc.1.2.transform.pl

310

20

740

60

true

z3-duality

   

05.NINT

05.02_limit3.enc.1.2.transform.pl

330

0

450

50

true

z3-duality

   

05.NINT

05.03_loop1.enc.1.2.transform.pl

450

10

1130

50

true

z3-duality

   

05.NINT

05.04_loop2.enc.1.2.transform.pl

430

20

1220

70

true

z3-duality

   

05.NINT

05.05_loop3.enc.1.2.transform.pl

410

10

1190

100

true

z3-duality

   

05.NINT

05.06_loopunswitch.enc.1.2.transform.pl

1560

20

8930

500

true

z3-duality

   

05.NINT

05.07_nonint1.enc.transform.pl

20

20

50

10

true

z3-duality

   

05.NINT

05.08_nonint1-hard.enc.transform.pl

50

0

50

0

true

z3-duality

   

05.NINT

05.09_nonint2.enc.transform.pl

40

10

30

10

false

z3-duality

   

05.NINT

05.10_nonint2-hard.enc.transform.pl

130

20

1240

110

true

z3-duality

   

05.NINT

05.11_nonint3.enc.transform.pl

30

0

80

0

true

z3-duality

   

05.NINT

05.12_nonint3-hard.enc.transform.pl

40

0

80

20

true

z3-duality

   

05.NINT

05.13_strengthred.enc.1.2.transform.pl

90

0

640

80

true

z3-duality

   

05.NINT

05.14_sum01.enc.1.2.transform.pl

490

10

6420

360

true

z3-duality

   

05.NINT

05.15_sumupto1.enc.1.2.transform.pl

1570

30

0

0

solver_timeout

z3-duality

   

05.NINT

05.16_sumupto2.enc.1.2.transform.pl

1810

30

14260

860

true

z3-duality

   

05.NINT

05.17_upcount.enc.1.2.transform.pl

210

10

1070

100

true

z3-duality

   

05.NINT

05.18_whileif.enc.1.2.transform.pl

700

30

1280

90

true

z3-duality

   

06.LOPT

06.01_code-sinking.enc.transform.pl

110

10

710

40

true

z3-duality

   

06.LOPT

06.02_condrem.enc.transform.pl

30

10

60

10

true

z3-duality

   

06.LOPT

06.03_countingloop.enc.transform.pl

40

0

100

20

true

z3-duality

   

06.LOPT

06.04_ex1.enc.transform.pl

60

20

110

0

true

z3-duality

   

06.LOPT

06.05_lf.enc.transform.pl

40

0

140

20

true

z3-duality

   

06.LOPT

06.06_licm.enc.transform.pl

50

0

100

20

true

z3-duality

   

06.LOPT

06.07_loop-peeling.enc.transform.pl

40

0

220

20

true

z3-duality

   

06.LOPT

06.08_loop-reversal.enc.transform.pl

50

0

240

10

true

z3-duality

   

06.LOPT

06.09_loop-tiling02.enc.transform.pl

40

20

380

30

true

z3-duality

   

06.LOPT

06.10_loop-unswitching.enc.transform.pl

60

10

420

40

true

z3-duality

   

06.LOPT

06.11_pre01.enc.transform.pl

30

0

40

0

true

z3-duality

   

06.LOPT

06.12_spin13-ex.enc.transform.pl

50

0

200

20

true

z3-duality

   

06.LOPT

06.13_strength-reduction.enc.transform.pl

30

0

100

0

true

z3-duality

   

06.LOPT

06.14_sw-pipelining.enc.transform.pl

40

10

170

10

true

z3-duality

   

06.LOPT

06.15_lf2.enc.transform.pl

30

10

0

0

solver_timeout

z3-duality

   

06.LOPT

06.16_loop-flattening.enc.transform.pl

40

10

0

0

solver_timeout

z3-duality

   

06.LOPT

06.17_loop-interchange.enc.transform.pl

90

10

0

0

solver_timeout

z3-duality

   

06.LOPT

06.18_loop-skewing.enc.transform.pl

240

10

3280

2080

error (*)

z3-duality

   

06.LOPT

06.19_loop-tiling01.enc.transform.pl

130

0

0

0

solver_timeout

z3-duality

   

06.LOPT

06.20_loop-unroll01.enc.transform.pl

50

10

7270

210

true

z3-duality

   

07.ITE

07.01_barthe.enc.transform.pl

50

0

140

10

true

z3-duality

   

07.ITE

07.02_barthe2.enc.transform.pl

40

0

220

20

true

z3-duality

   

07.ITE

07.03_barthe2-big.enc.transform.pl

60

10

580

40

true

z3-duality

   

07.ITE

07.04_barthe2-big2.enc.transform.pl

80

20

3460

100

true

z3-duality

   

07.ITE

07.05_barthe-faulty.enc.transform.pl

60

0

1110

70

false

z3-duality

   

07.ITE

07.06_bug15.enc.transform.pl

20

20

70

0

true

z3-duality

   

07.ITE

07.07_digits10.enc.transform.pl

360

10

0

0

solver_timeout

z3-duality

   

07.ITE

07.08_digits10_inl.enc.transform.pl

1730

20

6490

430

true

z3-duality

   

07.ITE

07.09_fib.enc.transform.pl

70

0

610

0

true

z3-duality

   

07.ITE

07.10_invarianthoisting.enc.transform.pl

50

0

140

20

true

z3-duality

   

07.ITE

07.11_loop.enc.transform.pl

40

20

170

30

true

z3-duality

   

07.ITE

07.12_loop2.enc.transform.pl

50

0

190

20

true

z3-duality

   

07.ITE

07.13_loop3.enc.transform.pl

30

10

200

10

true

z3-duality

   

07.ITE

07.14_loop4.enc.transform.pl

50

0

0

0

solver_timeout

z3-duality

   

07.ITE

07.15_loop5.enc.transform.pl

40

20

0

0

solver_timeout

z3-duality

   

07.ITE

07.16_loop5-faulty.enc.transform.pl

50

10

80

10

false

z3-duality

   

07.ITE

07.17_nested-while.enc.transform.pl

60

10

150

10

true

z3-duality

   

07.ITE

07.18_nested-while-faulty.enc.transform.pl

60

10

70

10

false

z3-duality

   

07.ITE

07.19_simple-loop.enc.transform.pl

40

10

2040

60

true

z3-duality

   

07.ITE

07.20_upcount.enc.transform.pl

30

0

160

10

true

z3-duality

   

07.ITE

07.21_while-if.enc.transform.pl

60

10

260

20

true

z3-duality

   

07.ITE

07.22_su_sq.hm.enc.transform.pl

30

0

0

0

solver_timeout

z3-duality

   

08.ARR

08.01_fib.enc.transform.pl

50

0

1000

60

true

z3-duality

   

08.ARR

08.02_findmax.enc.transform.pl

40

10

380

20

true

z3-duality

   

08.ARR

08.03_loopalign.enc.transform.pl

50

10

280

20

true

z3-duality

   

08.ARR

08.04_looppipe.enc.transform.pl

70

10

0

0

solver_timeout

z3-duality

   

08.ARR

08.05_propagate.enc.transform.pl

20

0

50

10

true

z3-duality

   

08.ARR

08.06_gtemaxarray.enc.1.transform.pl

60

10

1350

80

true

z3-duality

   

09.REC

09.01_add-horn.enc.transform.pl

50

0

110

0

true

z3-duality

   

09.REC

09.02_add-horn-faulty.enc.transform.pl

50

20

110

20

false

z3-duality

   

09.REC

09.03_cocome1.enc.transform.pl

40

0

70

10

true

z3-duality

   

09.REC

09.04_inlining.enc.transform.pl

100

10

860

50

true

z3-duality

   

09.REC

09.05_inlining-faulty.enc.transform.pl

100

0

200

20

false

z3-duality

   

09.REC

09.06_limit1.enc.transform.pl

50

0

0

0

solver_timeout

z3-duality

   

09.REC

09.07_limit1-faulty.enc.transform.pl

50

10

20

0

false

z3-duality

   

09.REC

09.08_limit1unrolled.enc.transform.pl

50

10

140

0

true

z3-duality

   

09.REC

09.09_limit2.enc.transform.pl

30

10

120

20

true

z3-duality

   

09.REC

09.10_limit2-faulty.enc.transform.pl

50

0

350

20

false

z3-duality

   

09.REC

09.11_limit3.enc.transform.pl

40

10

90

0

true

z3-duality

   

09.REC

09.12_loop_rec.enc.transform.pl

40

10

90

20

true

z3-duality

   

09.REC

09.13_triangular.enc.transform.pl

40

10

70

20

true

z3-duality

   

09.REC

09.14_triangular-mod.enc.transform.pl

160

20

0

0

solver_timeout

z3-duality

   

09.REC

09.15_triangular-mod-faulty.enc.transform.pl

80

10

1820

50

false

z3-duality

   

10.I-R

10.01_gcd.enc.transform.pl

120

20

120

40

true

z3-duality

   

10.I-R

10.02_sumprod.enc.transform.pl

40

10

0

0

solver_timeout

z3-duality

   

10.I-R

10.03_triangular_nontail.enc.transform.pl

40

10

450

20

true

z3-duality

   

10.I-R

10.04_triangular_tail.enc.transform.pl

40

10

350

40

true

z3-duality

   

11.COMP

11.01_array_copy.enc.transform.pl

60

20

400

40

true

z3-duality

   

11.COMP

11.02_array_copy_max.enc.1.transform.pl

120

20

3400

190

true

z3-duality

   

11.COMP

11.03_array_sum.enc.1.transform.pl

50

10

510

30

true

z3-duality

   

11.COMP

11.04_array_sum_k.enc.1.transform.pl

40

20

0

0

solver_timeout

z3-duality

   

11.COMP

11.05_sum_upto.enc.transform.pl

60

10

460

20

true

z3-duality

   

11.COMP

11.06_sum_upto_mult.enc.transform.pl

60

10

0

0

solver_timeout

z3-duality

   

11.COMP

11.07_sum_upto_mult_MON.enc.transform.pl

70

0

0

0

solver_timeout

z3-duality

   

11.COMP

11.08_twice_array_sum.enc.1.transform.pl

50

10

130

20

true

z3-duality

   

11.COMP

11.09_two_arrays_sum.enc.1.transform.pl

60

0

140

0

true

z3-duality

   

11.COMP

11.10_two_array_sum_diffsize.enc.1.transform.pl

360

20

1020

100

true

z3-duality

   

12.PCOR

12.01_bdiv.enc.transform.pl

570

10

4460

300

true

z3-duality

   

12.PCOR

12.02_fast_mult2.enc.transform.pl

60

0

190

20

true

z3-duality

   

12.PCOR

12.03_fast_mult3.enc.transform.pl

150

0

420

40

true

z3-duality

   

12.PCOR

12.04_fibonacci.enc.1.transform.pl

180

0

980

100

true

z3-duality

   

12.PCOR

12.05_fusc.enc.1.transform.pl

170

0

120

20

true

z3-duality

   

12.PCOR

12.06_gcd.enc.transform.pl

100

0

1090

60

true

z3-duality

   

12.PCOR

12.07_idiv.enc.transform.pl

30

10

180

10

true

z3-duality

   

12.PCOR

12.08_imc91rec.enc.transform.pl

90

10

0

0

solver_timeout

z3-duality

   

12.PCOR

12.09_imult.enc.transform.pl

100

10

0

0

solver_timeout

z3-duality

   

12.PCOR

12.10_remainder.enc.transform.pl

40

0

110

10

true

z3-duality

   

12.PCOR

12.11_sumfirst.enc.transform.pl

60

10

350

20

true

z3-duality

   

12.PCOR

12.12_lucas.enc.1.transform.pl

120

20

730

60

true

z3-duality

   

12.PCOR

12.13_padovan.enc.1.transform.pl

280

20

2970

140

true

z3-duality

   

12.PCOR

12.14_perrin.enc.1.transform.pl

120

10

840

40

true

z3-duality

   

12.PCOR

12.15_hanoi.enc.transform.pl

60

0

300

30

true

z3-duality

   

12.PCOR

12.16_digits10.enc.transform.pl

40

20

180

20

true

z3-duality

   

12.PCOR

12.17_digits10-itmd.enc.transform.pl

530

10

1000

90

true

z3-duality

   

12.PCOR

12.18_digits10-opt.enc.transform.pl

510

20

1900

200

true

z3-duality

   

12.PCOR

12.19_digits10-opt100.enc.transform.pl

150

10

630

40

true

z3-duality

   
           

(*) (error "query failed: Overflow encountered when expanding vector")