Unsound unsat cores #857
Description
For all of the following benchmarks from the Unsat Core Track at the SMT-COMP'25, we returned an unsound unsat core:
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/linear-inequality-inv-a-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/benchmark10_conjunctive-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/afnp2014-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/simple_vardep_2-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/cggmp2005-O0.smt2
QF_LIA/calypto/problem-004299.cvc.1.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/benchmark17_conjunctive-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/jm2006_variant-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/nested9-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/benchmark43_conjunctive-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/benchmark05_conjunctive-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/in-de32-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/benchmark14_linear-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/sum03-1-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/in-de31-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/Mono5_1-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/in-de42-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/nested6-O0.smt2
QF_LIA/calypto/problem-002673.cvc.1.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/in-de61-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/apache-get-tag.i.v+lhb-reducer-O0.smt2
QF_LIA/calypto/problem-001542.cvc.1.smt2
QF_LIA/20210219-Dartagnan/ConcurrencySafety-Main/race-1_1-join-O0.smt2
QF_LIA/fft/Sz64_1159.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/gsv2008-O0.smt2
QF_LIA/calypto/problem-004316.cvc.1.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/SpamAssassin-loop-O0.smt2
QF_LIA/fft/Sz32_455.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/benchmark20_conjunctive-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/deep-nested-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/string_concat-noarr-O0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/for_infinite_loop_2-O0.smt2
QF_LIA/fft/Sz128_2823.smt2
QF_LIA/calypto/problem-004350.cvc.1.smt2
QF_LIA/2019-ezsmt/incrementalScheduling/102-incremental_scheduling-18468-0.smt2
QF_LIA/20210219-Dartagnan/ReachSafety-Loops/benchmark32_linear-O0.smt2
QF_UF/2018-Goel-hwbench/QF_UF_peg_solitaire.6.prop1_ab_br_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_exit.5.prop1_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_pgm_protocol.4.prop5_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_counter_v_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_resistance.2.prop2_ab_cti_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_h_b08_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_loyd.2.prop1_ab_br_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_Heap_ab_br_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_exit.4.prop1_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_sokoban.1.prop1_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_exit.2.prop1_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_cambridge.2.prop1_ab_fp_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_h_TreeArb_ab_br_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_firewire_tree.1.prop1_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_needham.4.prop2_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_pipeline_ab_cti_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_loyd.3.prop1_ab_br_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_sw_sym_ex_v_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_itc99_b13_ab_cti_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_needham.1.prop2_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_resistance.1.prop2_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_v_Unidec_ab_fp_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_pj_icu_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_frogs.1.prop1_ab_br_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_hanoi.2.prop1_ab_br_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_sokoban.3.prop1_ab_br_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_h_Vlunc_ab_cti_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_h_b08_ab_cti_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_lann.4.prop1_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_exit.1.prop1_ab_reg_max.smt2
QF_UF/2018-Goel-hwbench/QF_UF_sw_loop_ab_reg_max.smt2
QF_UFLIA/20230314-Jaroslav-Bendik-Certora/44788_1965f0d6d94d5d8054ba_35_QF_UFLIA.smt2
QF_UFLIA/20230314-Jaroslav-Bendik-Certora/63058_aa742630eef64f949de269382c1f9035_25_UFLIA.smt2
QF_UFLIA/20230314-Jaroslav-Bendik-Certora/38347_092cc73601c78e45f4f9_55_QF_UFLIA.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product62_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product54_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product62_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product62_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product53_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.email_spec27_product13_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec1_product61_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product61_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product58_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product54_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.m0_true-unreach-call_drivers-net-slip-ko--108_1a--1b0b0ac.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--usb--serial--mos7840.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product50_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product49_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec4_product57_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product61_true-unreach-call.cil.c.smt2
QF_UFLRA/cpachecker-induction-svcomp14/cpachecker-induction.minepump_spec2_product53_true-unreach-call.cil.c.smt2
All of the benchmarks have been annotated and scrambled, taken from here.
The files above correspond to scrambled files
QF_LIA/scrambled30654.smt2
QF_LIA/scrambled84839.smt2
QF_LIA/scrambled147110.smt2
QF_LIA/scrambled168191.smt2
QF_LIA/scrambled106765.smt2
QF_LIA/scrambled177511.smt2
QF_LIA/scrambled352846.smt2
QF_LIA/scrambled117620.smt2
QF_LIA/scrambled32555.smt2
QF_LIA/scrambled356964.smt2
QF_LIA/scrambled125252.smt2
QF_LIA/scrambled276784.smt2
QF_LIA/scrambled196444.smt2
QF_LIA/scrambled100518.smt2
QF_LIA/scrambled95988.smt2
QF_LIA/scrambled198009.smt2
QF_LIA/scrambled416382.smt2
QF_LIA/scrambled393197.smt2
QF_LIA/scrambled11202.smt2
QF_LIA/scrambled51100.smt2
QF_LIA/scrambled167829.smt2
QF_LIA/scrambled384403.smt2
QF_LIA/scrambled193255.smt2
QF_LIA/scrambled118225.smt2
QF_LIA/scrambled323914.smt2
QF_LIA/scrambled410916.smt2
QF_LIA/scrambled308223.smt2
QF_LIA/scrambled62811.smt2
QF_LIA/scrambled13423.smt2
QF_LIA/scrambled427454.smt2
QF_LIA/scrambled99570.smt2
QF_LIA/scrambled117749.smt2
QF_LIA/scrambled75911.smt2
QF_LIA/scrambled421127.smt2
QF_LIA/scrambled113793.smt2
QF_LIA/scrambled353166.smt2
QF_UF/scrambled41760.smt2
QF_UF/scrambled306424.smt2
QF_UF/scrambled135136.smt2
QF_UF/scrambled312338.smt2
QF_UF/scrambled50806.smt2
QF_UF/scrambled176632.smt2
QF_UF/scrambled331492.smt2
QF_UF/scrambled313951.smt2
QF_UF/scrambled92890.smt2
QF_UF/scrambled423863.smt2
QF_UF/scrambled251652.smt2
QF_UF/scrambled204021.smt2
QF_UF/scrambled309521.smt2
QF_UF/scrambled148197.smt2
QF_UF/scrambled355026.smt2
QF_UF/scrambled352326.smt2
QF_UF/scrambled410364.smt2
QF_UF/scrambled298017.smt2
QF_UF/scrambled283969.smt2
QF_UF/scrambled153768.smt2
QF_UF/scrambled310261.smt2
QF_UF/scrambled209908.smt2
QF_UF/scrambled53206.smt2
QF_UF/scrambled138860.smt2
QF_UF/scrambled361476.smt2
QF_UF/scrambled166487.smt2
QF_UF/scrambled361891.smt2
QF_UF/scrambled206137.smt2
QF_UF/scrambled349773.smt2
QF_UF/scrambled315645.smt2
QF_UF/scrambled303169.smt2
QF_UFLIA/scrambled104170.smt2
QF_UFLIA/scrambled332262.smt2
QF_UFLIA/scrambled62679.smt2
QF_UFLRA/scrambled440414.smt2
QF_UFLRA/scrambled101284.smt2
QF_UFLRA/scrambled268265.smt2
QF_UFLRA/scrambled256071.smt2
QF_UFLRA/scrambled297883.smt2
QF_UFLRA/scrambled401189.smt2
QF_UFLRA/scrambled144397.smt2
QF_UFLRA/scrambled183424.smt2
QF_UFLRA/scrambled327992.smt2
QF_UFLRA/scrambled285794.smt2
QF_UFLRA/scrambled289711.smt2
QF_UFLRA/scrambled286110.smt2
QF_UFLRA/scrambled91127.smt2
QF_UFLRA/scrambled283690.smt2
QF_UFLRA/scrambled221840.smt2
QF_UFLRA/scrambled26950.smt2
QF_UFLRA/scrambled283180.smt2
For example, QF_LIA/calypto/problem-004299.cvc.1.smt2 was scrambled into:
(set-option :print-success false)
(set-option :produce-unsat-cores true)
(set-logic QF_LIA)
(declare-fun x49 () Int)
(declare-fun x60 () Int)
(declare-fun x1 () Bool)
(declare-fun x50 () Bool)
(declare-fun x46 () Int)
(declare-fun x53 () Int)
(declare-fun x68 () Bool)
(declare-fun x40 () Bool)
(declare-fun x63 () Int)
(declare-fun x27 () Int)
(declare-fun x18 () Bool)
(declare-fun x62 () Int)
(declare-fun x9 () Bool)
(declare-fun x35 () Bool)
(declare-fun x29 () Bool)
(declare-fun x25 () Bool)
(declare-fun x36 () Int)
(declare-fun x11 () Bool)
(declare-fun x34 () Bool)
(declare-fun x21 () Bool)
(declare-fun x69 () Bool)
(declare-fun x57 () Bool)
(declare-fun x44 () Bool)
(declare-fun x13 () Int)
(declare-fun x37 () Bool)
(declare-fun x59 () Int)
(declare-fun x12 () Int)
(declare-fun x70 () Bool)
(declare-fun x47 () Int)
(declare-fun x51 () Int)
(declare-fun x26 () Int)
(declare-fun x61 () Bool)
(declare-fun x58 () Int)
(declare-fun x48 () Bool)
(declare-fun x39 () Bool)
(declare-fun x17 () Bool)
(declare-fun x15 () Int)
(declare-fun x56 () Int)
(declare-fun x16 () Bool)
(declare-fun x65 () Bool)
(declare-fun x31 () Int)
(declare-fun x4 () Int)
(declare-fun x43 () Bool)
(declare-fun x66 () Bool)
(declare-fun x30 () Int)
(declare-fun x45 () Bool)
(declare-fun x28 () Bool)
(declare-fun x54 () Bool)
(declare-fun x64 () Int)
(declare-fun x23 () Bool)
(declare-fun x6 () Bool)
(assert (! (>= 7 x64) :named smtcomp1))
(assert (! (>= 7 x15) :named smtcomp2))
(assert (! (<= 0 x49) :named smtcomp3))
(assert (! (>= x64 0) :named smtcomp4))
(assert (! (<= 0 x63) :named smtcomp5))
(assert (! (<= x47 7) :named smtcomp6))
(assert (! (>= 7 x62) :named smtcomp7))
(assert (! (<= x26 1) :named smtcomp8))
(assert (! (>= 7 x51) :named smtcomp9))
(assert (! (<= x12 7) :named smtcomp10))
(assert (! (<= x36 1) :named smtcomp11))
(assert (! (<= x49 7) :named smtcomp12))
(assert (! (>= x4 0) :named smtcomp13))
(assert (! (<= x31 255) :named smtcomp14))
(assert (! (<= 0 x60) :named smtcomp15))
(assert (! (<= (- 2) x26) :named smtcomp16))
(assert (! (<= 0 x12) :named smtcomp17))
(assert (! (<= x27 1) :named smtcomp18))
(assert (! (>= x46 0) :named smtcomp19))
(assert (! (>= x30 0) :named smtcomp20))
(assert (! (>= x31 0) :named smtcomp21))
(assert (! (<= 0 x53) :named smtcomp22))
(assert (! (<= x56 7) :named smtcomp23))
(assert (! (>= x56 0) :named smtcomp24))
(assert (! (>= 7 x13) :named smtcomp25))
(assert (! (>= 7 x46) :named smtcomp26))
(assert (! (<= 0 x59) :named smtcomp27))
(assert (! (<= (- 2) x36) :named smtcomp28))
(assert (! (<= 0 x58) :named smtcomp29))
(assert (! (>= 7 x53) :named smtcomp30))
(assert (! (>= 7 x63) :named smtcomp31))
(assert (! (>= x15 0) :named smtcomp32))
(assert (! (<= (- 2) x27) :named smtcomp33))
(assert (! (<= 0 x47) :named smtcomp34))
(assert (! (<= x60 7) :named smtcomp35))
(assert (! (>= x62 0) :named smtcomp36))
(assert (! (>= 7 x4) :named smtcomp37))
(assert (! (>= 7 x59) :named smtcomp38))
(assert (! (<= 0 x13) :named smtcomp39))
(assert (! (>= x51 0) :named smtcomp40))
(assert (! (<= x30 255) :named smtcomp41))
(assert (! (<= x58 7) :named smtcomp42))
(declare-fun x2 () Int)
(declare-fun x67 () Bool)
(assert (! (let ((x20 (not x39)) (x22 (not x25))) (let ((x41 (not (not x45))) (x52 (not x34)) (x8 (not (ite x22 false (ite (not x66) (or x23 (or x44 x70)) false)))) (x42 (not x6))) (let ((x55 (ite x52 0 (ite x42 x60 x47))) (x5 (not (not x18)))) (let ((x14 (not (not x69))) (x7 (ite x5 x55 (ite x52 0 (ite x42 x47 x62)))) (x24 (ite (not (not x68)) x55 (ite x52 0 (ite x42 x13 x51))))) (let ((x38 (ite x14 x55 (ite x52 0 (ite x42 x58 x60)))) (x19 (ite (not (not x61)) x55 (ite x52 0 (ite x42 x64 x59))))) (let ((x3 (not (not (or (not (ite x41 (ite x8 (ite x22 x43 (ite x20 (not (= (ite (not (not x48)) 0 (+ (ite (and x65 (and x29 x40)) 1 0) (+ (+ (ite (and (> 0 (ite (< x46 4) x46 (- x46 8))) (and x29 x54)) 1 0) (+ (+ (ite (< x27 0) 1 0) (+ (ite (and x54 (< (ite (< x63 4) x63 (- x63 8)) 0)) 1 0) (+ (+ (ite (and (> 0 (ite (> 4 x49) x49 (- x49 8))) (and x1 x54)) 1 0) (ite (and (> 0 x26) x1) 1 0)) (ite (and x50 (and x40 x1)) 1 0)))) (ite (and x9 x40) 1 0))) (ite (and x29 (> 0 x36)) 1 0)))) 0)) x43)) x43) false)) (not (ite x41 (ite x8 (ite x22 x16 (ite x20 x28 x16)) x16) false)))))) (x32 (ite (not (not (or x48 (not x28)))) x30 x31)) (x10 (= 92 (+ (+ (ite (> x24 x53) 128 0) (+ (+ (+ (ite (> x55 x53) 16 0) (+ (ite (< x53 x38) 8 0) (+ (+ (ite (> (ite (not (not x17)) x38 (ite x14 x19 (ite x52 0 (ite x42 x12 x64)))) x53) 1 0) (ite (< x53 x19) 2 0)) (ite (> (ite (not (not x11)) x7 (ite x5 x19 (ite x52 0 (ite x42 x59 x56)))) x53) 4 0)))) (ite (> x7 x53) 32 0)) (ite (> (ite (not (not x35)) x38 (ite x14 x24 (ite x52 0 (ite x42 x4 x13)))) x53) 64 0))) (ite (< x53 (ite (not (not x57)) x7 (ite x5 x24 (ite x52 0 (ite x42 x51 x15))))) 256 0)))) (x33 (ite (not (not (or (not x16) (not x43)))) x37 x21))) (= (- (ite (ite x3 false (ite x41 (ite x8 (ite x22 x21 (ite x20 (and x10 (> 0 (ite (< x31 128) x31 (- x31 256)))) x21)) x21) false)) 1 0) (ite (ite x3 false (ite x41 (ite x8 (ite x22 x33 (ite x20 (and x10 (> 0 (ite (< x32 128) x32 (- x32 256)))) x33)) x33) false)) 1 0)) (+ (* 2 x2) 1)))))))) :named smtcomp43))
(check-sat)
(get-unsat-core)
(exit)
for which we return
unsat
(
smtcomp14
smtcomp21
)
However, taking only these assertions and omitting the rest, the query becomes satisfiable.
I reproduced the same behavior up until commit 40124b6, so the issue seems to be there from the beginning, that is, since #701.