User Tools

Site Tools


sv-comp_2015_sequentialized
# TODO: Counterexamples (possibly spurious - to check)
Sequentialized/seq-pthread/cs_stack_true-unreach-call.i

# Too few unwindings (only 2 or not even that) before time out
Sequentialized/seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c

dominated by solver time

  * ESMBC only other tool to solve this
  * SMT2 backend not working due to floatbv?

Passing problem to SMT2 QF_AUFBV using Yices
TODO: floatbv -> int

SMT2 backend complains

Sequentialized/seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c

dominated by solver time

Sequentialized/seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c
Sequentialized/seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c
Sequentialized/seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c
Sequentialized/seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c
Sequentialized/seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c
Sequentialized/seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c
Sequentialized/seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c
Sequentialized/seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c
Sequentialized/seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c
Sequentialized/seq-mthreaded/rekcba_ctm_false-unreach-call.3.c
Sequentialized/seq-mthreaded/rekcba_ctm_true-unreach-call.1.c
Sequentialized/seq-mthreaded/rekcba_ctm_true-unreach-call.2.c
Sequentialized/seq-mthreaded/rekcba_ctm_true-unreach-call.3.c
Sequentialized/seq-mthreaded/rekcba_ctm_true-unreach-call.4.c
Sequentialized/seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c
Sequentialized/seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c
Sequentialized/seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c
Sequentialized/seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c
Sequentialized/seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c
Sequentialized/seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c
Sequentialized/seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c
Sequentialized/seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c
Sequentialized/seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c
Sequentialized/seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c
Sequentialized/seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c
Sequentialized/seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c
Sequentialized/seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c
Sequentialized/seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c
Sequentialized/seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c
Sequentialized/seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c
Sequentialized/seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c
Sequentialized/seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c

# Too few unwindings (only 2) before time out
Sequentialized/systemc/token_ring.11_false-unreach-call_false-termination.cil.c
Sequentialized/systemc/token_ring.12_false-unreach-call_false-termination.cil.c
Sequentialized/systemc/token_ring.13_false-unreach-call_false-termination.cil.c
Sequentialized/systemc/token_ring.14_false-unreach-call_false-termination.cil.c
Sequentialized/systemc/token_ring.15_false-unreach-call_false-termination.cil.c
sv-comp_2015_sequentialized.txt · Last modified: 2015/01/14 16:01 by bjowac