detailed results (5033 total)

prover file res expected time
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_4clocks.worst_case_skew.induct.smt2 (content) unsat unsat 1.8s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_4clocks.worst_case_skew.base.smt2 (content) unsat unsat 0.013s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_4clocks.main_invar.induct.smt2 (content) unsat unsat 5.2s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_4clocks.main_invar.base.smt2 (content) unsat unsat 0.027s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_3clocks.worst_case_skew.induct.smt2 (content) unsat unsat 0.550s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_3clocks.worst_case_skew.base.smt2 (content) unsat unsat 0.014s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_3clocks.main_invar.induct.smt2 (content) unsat unsat 2s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_3clocks.main_invar.base.smt2 (content) unsat unsat 0.025s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_2clocks.worst_case_skew.induct.smt2 (content) unsat unsat 0.077s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_2clocks.worst_case_skew.base.smt2 (content) unsat unsat 0.013s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_2clocks.main_invar.induct.smt2 (content) unsat unsat 0.812s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_2clocks.main_invar.base.smt2 (content) unsat unsat 0.020s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_10clocks.worst_case_skew.base.smt2 (content) unsat unsat 0.014s
z3 /home/simon/workspace/smtlib/QF_LRA/clock_synchro/clocksynchro_10clocks.main_invar.base.smt2 (content) unsat unsat 0.057s
z3 /home/simon/workspace/smtlib/QF_LRA/check/bignum_lra2.smt2 (content) unsat unsat 0.015s
z3 /home/simon/workspace/smtlib/QF_LRA/TM/p5-driverlogNumeric_s9.smt2 (content) unsat unsat 0.238s
z3 /home/simon/workspace/smtlib/QF_LRA/LassoRanker/Ultimate/OpposedDisjuncts.bpl_Iteration1_Lasso_2-pieceTemplate.smt2 (content) unsat unsat 9.4s
z3 /home/simon/workspace/smtlib/QF_LRA/LassoRanker/Ultimate/NonTerminationDifficult.bpl_Iteration1_Lasso_7-phaseTemplate.smt2 (content) unsat unsat 3s
z3 /home/simon/workspace/smtlib/QF_LRA/LassoRanker/Ultimate/Gulwani.bpl_Iteration1_Lasso_6-phaseTemplate.smt2 (content) unsat unsat 1.6s
z3 /home/simon/workspace/smtlib/QF_LRA/LassoRanker/SV-COMP/LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c_Iteration2_Lasso_4-phaseTemplate.smt2 (content) unsat unsat 7.6s
z3 /home/simon/workspace/smtlib/QF_LRA/LassoRanker/SV-COMP/GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c_Iteration1_Lasso_5-nestedTemplate.smt2 (content) unsat unsat 4.7s
z3 /home/simon/workspace/smtlib/QF_LRA/LassoRanker/CooperatingT2/polyrank4.t2.c_Iteration8_Loop_4-pieceTemplate.smt2 (content) unsat unsat 3.3s
z3 /home/simon/workspace/smtlib/QF_LRA/LassoRanker/CooperatingT2/efegp.t2.c_Iteration1_Lasso_3-pieceTemplate.smt2 (content) unsat unsat 3.8s
z3 /home/simon/workspace/smtlib/QF_LRA/LassoRanker/CooperatingT2/collatz.t2.c_Iteration3_Lasso_7-phaseTemplate.smt2 (content) unsat unsat 8.6s
z3 /home/simon/workspace/smtlib/QF_LRA/2017-Heizmann-UltimateInvariantSynthesis/_sorting_bubblesort_ground.i_4_3_3.bpl_7.smt2 (content) unsat unsat 10s