Fix tests of unsat cores (#6593)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 21 May 2021 21:46:48 +0000 (16:46 -0500)
committerGitHub <noreply@github.com>
Fri, 21 May 2021 21:46:48 +0000 (21:46 +0000)
commit0e9fed387aaf5d0cb1844ab20551fbebfcb8893d
treeeae04bb949859b150c35803f764e8f7a4d47794c
parent8829c2cbb569296c188ef4285c7fe9568148f48a
Fix tests of unsat cores (#6593)

This updates all regressions that pass check-unsat-cores to enable check-unsat-cores. This includes any incremental benchmark, which was disabled in run_regression.py previously.

It adds --no-check-unsat-cores to a few corner benchmarks that were previously disabled based on --incremental.

It also reverts a change to when proofs are disabled: options like sygus-inference should not permit proofs (or unsat cores).
45 files changed:
src/smt/set_defaults.cpp
test/regress/regress0/arith/ackermann.real.smt2
test/regress/regress0/arith/arith-eq.smt2
test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
test/regress/regress0/arith/arith-mixed-types-tighten.smt2
test/regress/regress0/arith/arith-strict-relaxed.smt2
test/regress/regress0/arith/arith-strict.smt2
test/regress/regress0/arith/arith-tighten-1.smt2
test/regress/regress0/arith/arith-tighten-2.smt2
test/regress/regress0/arith/integers/ackermann1.smt2
test/regress/regress0/arith/integers/ackermann2.smt2
test/regress/regress0/arith/integers/ackermann3.smt2
test/regress/regress0/arith/integers/ackermann6.smt2
test/regress/regress0/arrays/bug4957.smt2
test/regress/regress0/bug528a.smt2
test/regress/regress0/bv/ackermann1.smt2
test/regress/regress0/bv/ackermann2.smt2
test/regress/regress0/bv/ackermann4.smt2
test/regress/regress0/bv/ackermann5.smt2
test/regress/regress0/bv/ackermann6.smt2
test/regress/regress0/bv/ackermann7.smt2
test/regress/regress0/bv/ackermann8.smt2
test/regress/regress0/bv/bv-int-collapse1.smt2
test/regress/regress0/bv/bv-int-collapse2.smt2
test/regress/regress0/bv/core/slice-12.smtv1.smt2
test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2
test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
test/regress/regress0/datatypes/empty_tuprec.cvc
test/regress/regress0/quantifiers/mix-match.smt2
test/regress/regress1/bv/bv2nat-ground.smt2
test/regress/regress1/fmf/PUZ001+1.smt2
test/regress/regress1/model-blocker-values.smt2
test/regress/regress1/nl/nl_uf_lalt.smt2
test/regress/regress1/push-pop/quant-fun-proc.smt2
test/regress/regress1/quantifiers/dump-inst-proof.smt2
test/regress/regress1/sygus/issue4009-qep.smt2
test/regress/regress2/bv_to_int_bitwise.smt2
test/regress/regress2/bv_to_int_mask_array_1.smt2
test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p
test/regress/regress3/arith_prp-13-24.smt2
test/regress/regress3/bv_to_int_and_or.smt2
test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
test/regress/regress3/bv_to_int_quant1.smt2
test/regress/regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
test/regress/run_regression.py