From 12479e2f840846f43405b6b72fe92b2d090d670b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Kol=C3=A1rik?= Date: Wed, 30 Oct 2024 17:02:08 +0100 Subject: [PATCH] Separated regression tests of unsat cores --- .gitignore | 2 +- ci/run_travis_commands.sh | 1 + .../QF_UF/smtcomp.smt2} | 0 .../QF_UF/smtcomp.smt2.expected.err} | 0 .../QF_UF/smtcomp.smt2.expected.out} | 0 .../QF_UF/smtcomp_min.smt2} | 0 .../QF_UF/smtcomp_min.smt2.expected.err} | 0 .../QF_UF/smtcomp_min.smt2.expected.out} | 0 .../generic/overlap.smt2} | 0 .../generic/overlap.smt2.expected.err} | 0 .../generic/overlap.smt2.expected.out} | 0 .../generic/overlap2.smt2} | 0 .../generic/overlap2.smt2.expected.err} | 0 .../generic/overlap2.smt2.expected.out} | 0 .../generic/overlap2_full.smt2} | 0 .../generic/overlap2_full.smt2.expected.err} | 0 .../generic/overlap2_full.smt2.expected.out} | 0 .../generic/overlap2_min.smt2} | 0 .../generic/overlap2_min.smt2.expected.err} | 0 .../generic/overlap2_min.smt2.expected.out} | 0 .../generic/overlap2_min_full.smt2} | 0 .../overlap2_min_full.smt2.expected.err} | 0 .../overlap2_min_full.smt2.expected.out} | 0 .../generic/overlap3.smt2} | 0 .../generic/overlap3.smt2.expected.err} | 0 .../generic/overlap3.smt2.expected.out} | 0 .../generic/overlap3_full.smt2} | 0 .../generic/overlap3_full.smt2.expected.err} | 0 .../generic/overlap3_full.smt2.expected.out} | 0 .../generic/overlap3_min.smt2} | 0 .../generic/overlap3_min.smt2.expected.err} | 0 .../generic/overlap3_min.smt2.expected.out} | 0 .../generic/overlap3_min_full.smt2} | 0 .../overlap3_min_full.smt2.expected.err} | 0 .../overlap3_min_full.smt2.expected.out} | 0 .../generic/overlap4.smt2} | 0 .../generic/overlap4.smt2.expected.err} | 0 .../generic/overlap4.smt2.expected.out} | 0 .../generic/overlap4_full.smt2} | 0 .../generic/overlap4_full.smt2.expected.err} | 0 .../generic/overlap4_full.smt2.expected.out} | 0 .../generic/overlap4_min.smt2} | 0 .../generic/overlap4_min.smt2.expected.err} | 0 .../generic/overlap4_min.smt2.expected.out} | 0 .../generic/overlap4_min_full.smt2} | 0 .../overlap4_min_full.smt2.expected.err} | 0 .../overlap4_min_full.smt2.expected.out} | 0 .../generic/overlap_full.smt2} | 0 .../generic/overlap_full.smt2.expected.err} | 0 .../generic/overlap_full.smt2.expected.out} | 0 .../generic/overlap_min.smt2} | 0 .../generic/overlap_min.smt2.expected.err} | 0 .../generic/overlap_min.smt2.expected.out} | 0 .../generic/overlap_min_full.smt2} | 0 .../overlap_min_full.smt2.expected.err} | 0 .../overlap_min_full.smt2.expected.out} | 0 .../generic/redundant.smt2} | 0 .../generic/redundant.smt2.expected.err} | 0 .../generic/redundant.smt2.expected.out} | 0 .../generic/redundant2.smt2} | 0 .../generic/redundant2.smt2.expected.err} | 0 .../generic/redundant2.smt2.expected.out} | 0 .../generic/redundant2_full.smt2} | 0 .../redundant2_full.smt2.expected.err} | 0 .../redundant2_full.smt2.expected.out} | 0 .../generic/redundant2_min.smt2} | 0 .../generic/redundant2_min.smt2.expected.err} | 0 .../generic/redundant2_min.smt2.expected.out} | 0 .../generic/redundant2_min_full.smt2} | 0 .../redundant2_min_full.smt2.expected.err} | 0 .../redundant2_min_full.smt2.expected.out} | 0 .../generic/redundant3.smt2} | 0 .../generic/redundant3.smt2.expected.err} | 0 .../generic/redundant3.smt2.expected.out} | 0 .../generic/redundant3_full.smt2} | 0 .../redundant3_full.smt2.expected.err} | 0 .../redundant3_full.smt2.expected.out} | 0 .../generic/redundant3_min.smt2} | 0 .../generic/redundant3_min.smt2.expected.err} | 0 .../generic/redundant3_min.smt2.expected.out} | 0 .../generic/redundant3_min_full.smt2} | 0 .../redundant3_min_full.smt2.expected.err} | 0 .../redundant3_min_full.smt2.expected.out} | 0 .../generic/redundant_full.smt2} | 0 .../generic/redundant_full.smt2.expected.err} | 0 .../generic/redundant_full.smt2.expected.out} | 0 .../generic/redundant_min.smt2} | 0 .../generic/redundant_min.smt2.expected.err} | 0 .../generic/redundant_min.smt2.expected.out} | 0 .../generic/redundant_min_full.smt2} | 0 .../redundant_min_full.smt2.expected.err} | 0 .../redundant_min_full.smt2.expected.out} | 0 .../generic/trivial.smt2} | 0 .../generic/trivial.smt2.expected.err} | 0 .../generic/trivial.smt2.expected.out} | 0 .../generic/trivial2.smt2} | 0 .../generic/trivial2.smt2.expected.err} | 0 .../generic/trivial2.smt2.expected.out} | 0 .../generic/trivial2_full.smt2} | 0 .../generic/trivial2_full.smt2.expected.err} | 0 .../generic/trivial2_full.smt2.expected.out} | 0 .../generic/trivial2_min.smt2} | 0 .../generic/trivial2_min.smt2.expected.err} | 0 .../generic/trivial2_min.smt2.expected.out} | 0 .../generic/trivial3.smt2} | 0 .../generic/trivial3.smt2.expected.err} | 0 .../generic/trivial3.smt2.expected.out} | 0 .../generic/trivial3_full.smt2} | 0 .../generic/trivial3_full.smt2.expected.err} | 0 .../generic/trivial3_full.smt2.expected.out} | 0 .../generic/trivial_full.smt2} | 0 .../generic/trivial_full.smt2.expected.err} | 0 .../generic/trivial_full.smt2.expected.out} | 0 .../generic/trivial_min.smt2} | 0 .../generic/trivial_min.smt2.expected.err} | 0 .../generic/trivial_min.smt2.expected.out} | 0 .../generic/trivial_min_full.smt2} | 0 .../trivial_min_full.smt2.expected.err} | 0 .../trivial_min_full.smt2.expected.out} | 0 .../generic/trivial_xor.smt2} | 0 .../generic/trivial_xor.smt2.expected.err} | 0 .../generic/trivial_xor.smt2.expected.out} | 0 .../generic/trivial_xor_full.smt2} | 0 .../trivial_xor_full.smt2.expected.err} | 0 .../trivial_xor_full.smt2.expected.out} | 0 .../generic/trivial_xor_min.smt2} | 0 .../trivial_xor_min.smt2.expected.err} | 0 .../trivial_xor_min.smt2.expected.out} | 0 .../incremental/global.smt2} | 0 .../incremental/global.smt2.expected.err} | 0 .../incremental/global.smt2.expected.out} | 0 .../incremental/scoped.smt2} | 0 .../incremental/scoped.smt2.expected.err} | 0 .../incremental/scoped.smt2.expected.out} | 0 .../unsatcores/run-test-notiming.sh | 72 +++++++++++++++++++ 135 files changed, 74 insertions(+), 1 deletion(-) rename test/regression/{base/QF_UF/smtcomp_unsat_core.smt2 => unsatcores/QF_UF/smtcomp.smt2} (100%) rename test/regression/{base/QF_UF/smtcomp_min_unsat_core.smt2.expected.err => unsatcores/QF_UF/smtcomp.smt2.expected.err} (100%) rename test/regression/{base/QF_UF/smtcomp_unsat_core.smt2.expected.out => unsatcores/QF_UF/smtcomp.smt2.expected.out} (100%) rename test/regression/{base/QF_UF/smtcomp_min_unsat_core.smt2 => unsatcores/QF_UF/smtcomp_min.smt2} (100%) rename test/regression/{base/QF_UF/smtcomp_unsat_core.smt2.expected.err => unsatcores/QF_UF/smtcomp_min.smt2.expected.err} (100%) rename test/regression/{base/QF_UF/smtcomp_min_unsat_core.smt2.expected.out => unsatcores/QF_UF/smtcomp_min.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_unsat_core.smt2 => unsatcores/generic/overlap.smt2} (100%) rename test/regression/{base/generic/overlap_min_unsat_core.smt2.expected.err => unsatcores/generic/overlap.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_unsat_core.smt2.expected.out => unsatcores/generic/overlap.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_unsat_core2.smt2 => unsatcores/generic/overlap2.smt2} (100%) rename test/regression/{base/generic/overlap_min_unsat_core2.smt2.expected.err => unsatcores/generic/overlap2.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_min_unsat_core.smt2.expected.out => unsatcores/generic/overlap2.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_unsat_core2_full.smt2 => unsatcores/generic/overlap2_full.smt2} (100%) rename test/regression/{base/generic/overlap_min_unsat_core2_full.smt2.expected.err => unsatcores/generic/overlap2_full.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_unsat_core2_full.smt2.expected.out => unsatcores/generic/overlap2_full.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_min_unsat_core2.smt2 => unsatcores/generic/overlap2_min.smt2} (100%) rename test/regression/{base/generic/overlap_min_unsat_core3.smt2.expected.err => unsatcores/generic/overlap2_min.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_min_unsat_core2.smt2.expected.out => unsatcores/generic/overlap2_min.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_min_unsat_core2_full.smt2 => unsatcores/generic/overlap2_min_full.smt2} (100%) rename test/regression/{base/generic/overlap_min_unsat_core3_full.smt2.expected.err => unsatcores/generic/overlap2_min_full.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_min_unsat_core2_full.smt2.expected.out => unsatcores/generic/overlap2_min_full.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_unsat_core3.smt2 => unsatcores/generic/overlap3.smt2} (100%) rename test/regression/{base/generic/overlap_min_unsat_core4.smt2.expected.err => unsatcores/generic/overlap3.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_unsat_core3.smt2.expected.out => unsatcores/generic/overlap3.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_unsat_core3_full.smt2 => unsatcores/generic/overlap3_full.smt2} (100%) rename test/regression/{base/generic/overlap_min_unsat_core4_full.smt2.expected.err => unsatcores/generic/overlap3_full.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_unsat_core3_full.smt2.expected.out => unsatcores/generic/overlap3_full.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_min_unsat_core3.smt2 => unsatcores/generic/overlap3_min.smt2} (100%) rename test/regression/{base/generic/overlap_min_unsat_core_full.smt2.expected.err => unsatcores/generic/overlap3_min.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_min_unsat_core3.smt2.expected.out => unsatcores/generic/overlap3_min.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_min_unsat_core3_full.smt2 => unsatcores/generic/overlap3_min_full.smt2} (100%) rename test/regression/{base/generic/overlap_unsat_core.smt2.expected.err => unsatcores/generic/overlap3_min_full.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_min_unsat_core3_full.smt2.expected.out => unsatcores/generic/overlap3_min_full.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_unsat_core4.smt2 => unsatcores/generic/overlap4.smt2} (100%) rename test/regression/{base/generic/overlap_unsat_core2.smt2.expected.err => unsatcores/generic/overlap4.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_unsat_core4.smt2.expected.out => unsatcores/generic/overlap4.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_unsat_core4_full.smt2 => unsatcores/generic/overlap4_full.smt2} (100%) rename test/regression/{base/generic/overlap_unsat_core2_full.smt2.expected.err => unsatcores/generic/overlap4_full.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_unsat_core4_full.smt2.expected.out => unsatcores/generic/overlap4_full.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_min_unsat_core4.smt2 => unsatcores/generic/overlap4_min.smt2} (100%) rename test/regression/{base/generic/overlap_unsat_core3.smt2.expected.err => unsatcores/generic/overlap4_min.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_min_unsat_core4.smt2.expected.out => unsatcores/generic/overlap4_min.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_min_unsat_core4_full.smt2 => unsatcores/generic/overlap4_min_full.smt2} (100%) rename test/regression/{base/generic/overlap_unsat_core3_full.smt2.expected.err => unsatcores/generic/overlap4_min_full.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_min_unsat_core4_full.smt2.expected.out => unsatcores/generic/overlap4_min_full.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_unsat_core_full.smt2 => unsatcores/generic/overlap_full.smt2} (100%) rename test/regression/{base/generic/overlap_unsat_core4.smt2.expected.err => unsatcores/generic/overlap_full.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_unsat_core_full.smt2.expected.out => unsatcores/generic/overlap_full.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_min_unsat_core.smt2 => unsatcores/generic/overlap_min.smt2} (100%) rename test/regression/{base/generic/overlap_unsat_core4_full.smt2.expected.err => unsatcores/generic/overlap_min.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_unsat_core2.smt2.expected.out => unsatcores/generic/overlap_min.smt2.expected.out} (100%) rename test/regression/{base/generic/overlap_min_unsat_core_full.smt2 => unsatcores/generic/overlap_min_full.smt2} (100%) rename test/regression/{base/generic/overlap_unsat_core_full.smt2.expected.err => unsatcores/generic/overlap_min_full.smt2.expected.err} (100%) rename test/regression/{base/generic/overlap_min_unsat_core_full.smt2.expected.out => unsatcores/generic/overlap_min_full.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_unsat_core.smt2 => unsatcores/generic/redundant.smt2} (100%) rename test/regression/{base/generic/redundant_min_unsat_core.smt2.expected.err => unsatcores/generic/redundant.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_min_unsat_core.smt2.expected.out => unsatcores/generic/redundant.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_unsat_core2.smt2 => unsatcores/generic/redundant2.smt2} (100%) rename test/regression/{base/generic/redundant_min_unsat_core2.smt2.expected.err => unsatcores/generic/redundant2.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_min_unsat_core2.smt2.expected.out => unsatcores/generic/redundant2.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_unsat_core2_full.smt2 => unsatcores/generic/redundant2_full.smt2} (100%) rename test/regression/{base/generic/redundant_min_unsat_core2_full.smt2.expected.err => unsatcores/generic/redundant2_full.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_min_unsat_core2_full.smt2.expected.out => unsatcores/generic/redundant2_full.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_min_unsat_core2.smt2 => unsatcores/generic/redundant2_min.smt2} (100%) rename test/regression/{base/generic/redundant_min_unsat_core3.smt2.expected.err => unsatcores/generic/redundant2_min.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_unsat_core2.smt2.expected.out => unsatcores/generic/redundant2_min.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_min_unsat_core2_full.smt2 => unsatcores/generic/redundant2_min_full.smt2} (100%) rename test/regression/{base/generic/redundant_min_unsat_core3_full.smt2.expected.err => unsatcores/generic/redundant2_min_full.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_min_unsat_core3_full.smt2.expected.out => unsatcores/generic/redundant2_min_full.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_unsat_core3.smt2 => unsatcores/generic/redundant3.smt2} (100%) rename test/regression/{base/generic/redundant_min_unsat_core_full.smt2.expected.err => unsatcores/generic/redundant3.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_min_unsat_core3.smt2.expected.out => unsatcores/generic/redundant3.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_unsat_core3_full.smt2 => unsatcores/generic/redundant3_full.smt2} (100%) rename test/regression/{base/generic/redundant_unsat_core.smt2.expected.err => unsatcores/generic/redundant3_full.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_unsat_core2_full.smt2.expected.out => unsatcores/generic/redundant3_full.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_min_unsat_core3.smt2 => unsatcores/generic/redundant3_min.smt2} (100%) rename test/regression/{base/generic/redundant_unsat_core2.smt2.expected.err => unsatcores/generic/redundant3_min.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_unsat_core3.smt2.expected.out => unsatcores/generic/redundant3_min.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_min_unsat_core3_full.smt2 => unsatcores/generic/redundant3_min_full.smt2} (100%) rename test/regression/{base/generic/redundant_unsat_core2_full.smt2.expected.err => unsatcores/generic/redundant3_min_full.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_unsat_core3_full.smt2.expected.out => unsatcores/generic/redundant3_min_full.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_unsat_core_full.smt2 => unsatcores/generic/redundant_full.smt2} (100%) rename test/regression/{base/generic/redundant_unsat_core3.smt2.expected.err => unsatcores/generic/redundant_full.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_min_unsat_core_full.smt2.expected.out => unsatcores/generic/redundant_full.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_min_unsat_core.smt2 => unsatcores/generic/redundant_min.smt2} (100%) rename test/regression/{base/generic/redundant_unsat_core3_full.smt2.expected.err => unsatcores/generic/redundant_min.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_unsat_core.smt2.expected.out => unsatcores/generic/redundant_min.smt2.expected.out} (100%) rename test/regression/{base/generic/redundant_min_unsat_core_full.smt2 => unsatcores/generic/redundant_min_full.smt2} (100%) rename test/regression/{base/generic/redundant_unsat_core_full.smt2.expected.err => unsatcores/generic/redundant_min_full.smt2.expected.err} (100%) rename test/regression/{base/generic/redundant_unsat_core_full.smt2.expected.out => unsatcores/generic/redundant_min_full.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_unsat_core.smt2 => unsatcores/generic/trivial.smt2} (100%) rename test/regression/{base/generic/trivial_min_unsat_core.smt2.expected.err => unsatcores/generic/trivial.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_min_unsat_core.smt2.expected.out => unsatcores/generic/trivial.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_unsat_core2.smt2 => unsatcores/generic/trivial2.smt2} (100%) rename test/regression/{base/generic/trivial_min_unsat_core2.smt2.expected.err => unsatcores/generic/trivial2.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_min_unsat_core2.smt2.expected.out => unsatcores/generic/trivial2.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_unsat_core2_full.smt2 => unsatcores/generic/trivial2_full.smt2} (100%) rename test/regression/{base/generic/trivial_min_unsat_core_full.smt2.expected.err => unsatcores/generic/trivial2_full.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_min_unsat_core_full.smt2.expected.out => unsatcores/generic/trivial2_full.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_min_unsat_core2.smt2 => unsatcores/generic/trivial2_min.smt2} (100%) rename test/regression/{base/generic/trivial_min_xor_unsat_core.smt2.expected.err => unsatcores/generic/trivial2_min.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_unsat_core2.smt2.expected.out => unsatcores/generic/trivial2_min.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_unsat_core3.smt2 => unsatcores/generic/trivial3.smt2} (100%) rename test/regression/{base/generic/trivial_unsat_core.smt2.expected.err => unsatcores/generic/trivial3.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_unsat_core3.smt2.expected.out => unsatcores/generic/trivial3.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_unsat_core3_full.smt2 => unsatcores/generic/trivial3_full.smt2} (100%) rename test/regression/{base/generic/trivial_unsat_core2.smt2.expected.err => unsatcores/generic/trivial3_full.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_unsat_core2_full.smt2.expected.out => unsatcores/generic/trivial3_full.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_unsat_core_full.smt2 => unsatcores/generic/trivial_full.smt2} (100%) rename test/regression/{base/generic/trivial_unsat_core2_full.smt2.expected.err => unsatcores/generic/trivial_full.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_unsat_core3_full.smt2.expected.out => unsatcores/generic/trivial_full.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_min_unsat_core.smt2 => unsatcores/generic/trivial_min.smt2} (100%) rename test/regression/{base/generic/trivial_unsat_core3.smt2.expected.err => unsatcores/generic/trivial_min.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_min_xor_unsat_core.smt2.expected.out => unsatcores/generic/trivial_min.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_min_unsat_core_full.smt2 => unsatcores/generic/trivial_min_full.smt2} (100%) rename test/regression/{base/generic/trivial_unsat_core3_full.smt2.expected.err => unsatcores/generic/trivial_min_full.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_unsat_core_full.smt2.expected.out => unsatcores/generic/trivial_min_full.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_xor_unsat_core.smt2 => unsatcores/generic/trivial_xor.smt2} (100%) rename test/regression/{base/generic/trivial_unsat_core_full.smt2.expected.err => unsatcores/generic/trivial_xor.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_unsat_core.smt2.expected.out => unsatcores/generic/trivial_xor.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_xor_unsat_core_full.smt2 => unsatcores/generic/trivial_xor_full.smt2} (100%) rename test/regression/{base/generic/trivial_xor_unsat_core.smt2.expected.err => unsatcores/generic/trivial_xor_full.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_xor_unsat_core_full.smt2.expected.out => unsatcores/generic/trivial_xor_full.smt2.expected.out} (100%) rename test/regression/{base/generic/trivial_min_xor_unsat_core.smt2 => unsatcores/generic/trivial_xor_min.smt2} (100%) rename test/regression/{base/generic/trivial_xor_unsat_core_full.smt2.expected.err => unsatcores/generic/trivial_xor_min.smt2.expected.err} (100%) rename test/regression/{base/generic/trivial_xor_unsat_core.smt2.expected.out => unsatcores/generic/trivial_xor_min.smt2.expected.out} (100%) rename test/regression/{base/incremental/unsat_core_global.smt2 => unsatcores/incremental/global.smt2} (100%) rename test/regression/{base/incremental/unsat_core_global.smt2.expected.err => unsatcores/incremental/global.smt2.expected.err} (100%) rename test/regression/{base/incremental/unsat_core_global.smt2.expected.out => unsatcores/incremental/global.smt2.expected.out} (100%) rename test/regression/{base/incremental/unsat_core_scoped.smt2 => unsatcores/incremental/scoped.smt2} (100%) rename test/regression/{base/incremental/unsat_core_scoped.smt2.expected.err => unsatcores/incremental/scoped.smt2.expected.err} (100%) rename test/regression/{base/incremental/unsat_core_scoped.smt2.expected.out => unsatcores/incremental/scoped.smt2.expected.out} (100%) create mode 100755 test/regression/unsatcores/run-test-notiming.sh diff --git a/.gitignore b/.gitignore index 5ea0da75d..bce96fd45 100644 --- a/.gitignore +++ b/.gitignore @@ -22,7 +22,7 @@ m4/ltversion.m4 m4/lt~obsolete.m4 opensmt src/bin/.dirstamp -test/regression/base/log-* +test/regression/*/log-* src/PySMT/opensmt.py .ycm_extra_conf.py .ycm_extra_conf.pyc diff --git a/ci/run_travis_commands.sh b/ci/run_travis_commands.sh index 28178c53e..79d62b124 100755 --- a/ci/run_travis_commands.sh +++ b/ci/run_travis_commands.sh @@ -23,6 +23,7 @@ make test make install if [[ ${CMAKE_BUILD_TYPE} == Debug ]]; then cd ../test/regression/base && ./run-test-notiming.sh ../../../build/opensmt + cd ../unsatcores && ./run-test-notiming.sh ../../../build/opensmt cd ../interpolation && ./run-tests.sh ../../../build/opensmt if [[ "${PARALLEL}" == "ON" ]]; then cd ../splitting && ./bin/run-tests.sh ../../../build/opensmt-splitter diff --git a/test/regression/base/QF_UF/smtcomp_unsat_core.smt2 b/test/regression/unsatcores/QF_UF/smtcomp.smt2 similarity index 100% rename from test/regression/base/QF_UF/smtcomp_unsat_core.smt2 rename to test/regression/unsatcores/QF_UF/smtcomp.smt2 diff --git a/test/regression/base/QF_UF/smtcomp_min_unsat_core.smt2.expected.err b/test/regression/unsatcores/QF_UF/smtcomp.smt2.expected.err similarity index 100% rename from test/regression/base/QF_UF/smtcomp_min_unsat_core.smt2.expected.err rename to test/regression/unsatcores/QF_UF/smtcomp.smt2.expected.err diff --git a/test/regression/base/QF_UF/smtcomp_unsat_core.smt2.expected.out b/test/regression/unsatcores/QF_UF/smtcomp.smt2.expected.out similarity index 100% rename from test/regression/base/QF_UF/smtcomp_unsat_core.smt2.expected.out rename to test/regression/unsatcores/QF_UF/smtcomp.smt2.expected.out diff --git a/test/regression/base/QF_UF/smtcomp_min_unsat_core.smt2 b/test/regression/unsatcores/QF_UF/smtcomp_min.smt2 similarity index 100% rename from test/regression/base/QF_UF/smtcomp_min_unsat_core.smt2 rename to test/regression/unsatcores/QF_UF/smtcomp_min.smt2 diff --git a/test/regression/base/QF_UF/smtcomp_unsat_core.smt2.expected.err b/test/regression/unsatcores/QF_UF/smtcomp_min.smt2.expected.err similarity index 100% rename from test/regression/base/QF_UF/smtcomp_unsat_core.smt2.expected.err rename to test/regression/unsatcores/QF_UF/smtcomp_min.smt2.expected.err diff --git a/test/regression/base/QF_UF/smtcomp_min_unsat_core.smt2.expected.out b/test/regression/unsatcores/QF_UF/smtcomp_min.smt2.expected.out similarity index 100% rename from test/regression/base/QF_UF/smtcomp_min_unsat_core.smt2.expected.out rename to test/regression/unsatcores/QF_UF/smtcomp_min.smt2.expected.out diff --git a/test/regression/base/generic/overlap_unsat_core.smt2 b/test/regression/unsatcores/generic/overlap.smt2 similarity index 100% rename from test/regression/base/generic/overlap_unsat_core.smt2 rename to test/regression/unsatcores/generic/overlap.smt2 diff --git a/test/regression/base/generic/overlap_min_unsat_core.smt2.expected.err b/test/regression/unsatcores/generic/overlap.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core.smt2.expected.err rename to test/regression/unsatcores/generic/overlap.smt2.expected.err diff --git a/test/regression/base/generic/overlap_unsat_core.smt2.expected.out b/test/regression/unsatcores/generic/overlap.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_unsat_core.smt2.expected.out rename to test/regression/unsatcores/generic/overlap.smt2.expected.out diff --git a/test/regression/base/generic/overlap_unsat_core2.smt2 b/test/regression/unsatcores/generic/overlap2.smt2 similarity index 100% rename from test/regression/base/generic/overlap_unsat_core2.smt2 rename to test/regression/unsatcores/generic/overlap2.smt2 diff --git a/test/regression/base/generic/overlap_min_unsat_core2.smt2.expected.err b/test/regression/unsatcores/generic/overlap2.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core2.smt2.expected.err rename to test/regression/unsatcores/generic/overlap2.smt2.expected.err diff --git a/test/regression/base/generic/overlap_min_unsat_core.smt2.expected.out b/test/regression/unsatcores/generic/overlap2.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core.smt2.expected.out rename to test/regression/unsatcores/generic/overlap2.smt2.expected.out diff --git a/test/regression/base/generic/overlap_unsat_core2_full.smt2 b/test/regression/unsatcores/generic/overlap2_full.smt2 similarity index 100% rename from test/regression/base/generic/overlap_unsat_core2_full.smt2 rename to test/regression/unsatcores/generic/overlap2_full.smt2 diff --git a/test/regression/base/generic/overlap_min_unsat_core2_full.smt2.expected.err b/test/regression/unsatcores/generic/overlap2_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core2_full.smt2.expected.err rename to test/regression/unsatcores/generic/overlap2_full.smt2.expected.err diff --git a/test/regression/base/generic/overlap_unsat_core2_full.smt2.expected.out b/test/regression/unsatcores/generic/overlap2_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_unsat_core2_full.smt2.expected.out rename to test/regression/unsatcores/generic/overlap2_full.smt2.expected.out diff --git a/test/regression/base/generic/overlap_min_unsat_core2.smt2 b/test/regression/unsatcores/generic/overlap2_min.smt2 similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core2.smt2 rename to test/regression/unsatcores/generic/overlap2_min.smt2 diff --git a/test/regression/base/generic/overlap_min_unsat_core3.smt2.expected.err b/test/regression/unsatcores/generic/overlap2_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core3.smt2.expected.err rename to test/regression/unsatcores/generic/overlap2_min.smt2.expected.err diff --git a/test/regression/base/generic/overlap_min_unsat_core2.smt2.expected.out b/test/regression/unsatcores/generic/overlap2_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core2.smt2.expected.out rename to test/regression/unsatcores/generic/overlap2_min.smt2.expected.out diff --git a/test/regression/base/generic/overlap_min_unsat_core2_full.smt2 b/test/regression/unsatcores/generic/overlap2_min_full.smt2 similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core2_full.smt2 rename to test/regression/unsatcores/generic/overlap2_min_full.smt2 diff --git a/test/regression/base/generic/overlap_min_unsat_core3_full.smt2.expected.err b/test/regression/unsatcores/generic/overlap2_min_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core3_full.smt2.expected.err rename to test/regression/unsatcores/generic/overlap2_min_full.smt2.expected.err diff --git a/test/regression/base/generic/overlap_min_unsat_core2_full.smt2.expected.out b/test/regression/unsatcores/generic/overlap2_min_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core2_full.smt2.expected.out rename to test/regression/unsatcores/generic/overlap2_min_full.smt2.expected.out diff --git a/test/regression/base/generic/overlap_unsat_core3.smt2 b/test/regression/unsatcores/generic/overlap3.smt2 similarity index 100% rename from test/regression/base/generic/overlap_unsat_core3.smt2 rename to test/regression/unsatcores/generic/overlap3.smt2 diff --git a/test/regression/base/generic/overlap_min_unsat_core4.smt2.expected.err b/test/regression/unsatcores/generic/overlap3.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core4.smt2.expected.err rename to test/regression/unsatcores/generic/overlap3.smt2.expected.err diff --git a/test/regression/base/generic/overlap_unsat_core3.smt2.expected.out b/test/regression/unsatcores/generic/overlap3.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_unsat_core3.smt2.expected.out rename to test/regression/unsatcores/generic/overlap3.smt2.expected.out diff --git a/test/regression/base/generic/overlap_unsat_core3_full.smt2 b/test/regression/unsatcores/generic/overlap3_full.smt2 similarity index 100% rename from test/regression/base/generic/overlap_unsat_core3_full.smt2 rename to test/regression/unsatcores/generic/overlap3_full.smt2 diff --git a/test/regression/base/generic/overlap_min_unsat_core4_full.smt2.expected.err b/test/regression/unsatcores/generic/overlap3_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core4_full.smt2.expected.err rename to test/regression/unsatcores/generic/overlap3_full.smt2.expected.err diff --git a/test/regression/base/generic/overlap_unsat_core3_full.smt2.expected.out b/test/regression/unsatcores/generic/overlap3_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_unsat_core3_full.smt2.expected.out rename to test/regression/unsatcores/generic/overlap3_full.smt2.expected.out diff --git a/test/regression/base/generic/overlap_min_unsat_core3.smt2 b/test/regression/unsatcores/generic/overlap3_min.smt2 similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core3.smt2 rename to test/regression/unsatcores/generic/overlap3_min.smt2 diff --git a/test/regression/base/generic/overlap_min_unsat_core_full.smt2.expected.err b/test/regression/unsatcores/generic/overlap3_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core_full.smt2.expected.err rename to test/regression/unsatcores/generic/overlap3_min.smt2.expected.err diff --git a/test/regression/base/generic/overlap_min_unsat_core3.smt2.expected.out b/test/regression/unsatcores/generic/overlap3_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core3.smt2.expected.out rename to test/regression/unsatcores/generic/overlap3_min.smt2.expected.out diff --git a/test/regression/base/generic/overlap_min_unsat_core3_full.smt2 b/test/regression/unsatcores/generic/overlap3_min_full.smt2 similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core3_full.smt2 rename to test/regression/unsatcores/generic/overlap3_min_full.smt2 diff --git a/test/regression/base/generic/overlap_unsat_core.smt2.expected.err b/test/regression/unsatcores/generic/overlap3_min_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_unsat_core.smt2.expected.err rename to test/regression/unsatcores/generic/overlap3_min_full.smt2.expected.err diff --git a/test/regression/base/generic/overlap_min_unsat_core3_full.smt2.expected.out b/test/regression/unsatcores/generic/overlap3_min_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core3_full.smt2.expected.out rename to test/regression/unsatcores/generic/overlap3_min_full.smt2.expected.out diff --git a/test/regression/base/generic/overlap_unsat_core4.smt2 b/test/regression/unsatcores/generic/overlap4.smt2 similarity index 100% rename from test/regression/base/generic/overlap_unsat_core4.smt2 rename to test/regression/unsatcores/generic/overlap4.smt2 diff --git a/test/regression/base/generic/overlap_unsat_core2.smt2.expected.err b/test/regression/unsatcores/generic/overlap4.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_unsat_core2.smt2.expected.err rename to test/regression/unsatcores/generic/overlap4.smt2.expected.err diff --git a/test/regression/base/generic/overlap_unsat_core4.smt2.expected.out b/test/regression/unsatcores/generic/overlap4.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_unsat_core4.smt2.expected.out rename to test/regression/unsatcores/generic/overlap4.smt2.expected.out diff --git a/test/regression/base/generic/overlap_unsat_core4_full.smt2 b/test/regression/unsatcores/generic/overlap4_full.smt2 similarity index 100% rename from test/regression/base/generic/overlap_unsat_core4_full.smt2 rename to test/regression/unsatcores/generic/overlap4_full.smt2 diff --git a/test/regression/base/generic/overlap_unsat_core2_full.smt2.expected.err b/test/regression/unsatcores/generic/overlap4_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_unsat_core2_full.smt2.expected.err rename to test/regression/unsatcores/generic/overlap4_full.smt2.expected.err diff --git a/test/regression/base/generic/overlap_unsat_core4_full.smt2.expected.out b/test/regression/unsatcores/generic/overlap4_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_unsat_core4_full.smt2.expected.out rename to test/regression/unsatcores/generic/overlap4_full.smt2.expected.out diff --git a/test/regression/base/generic/overlap_min_unsat_core4.smt2 b/test/regression/unsatcores/generic/overlap4_min.smt2 similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core4.smt2 rename to test/regression/unsatcores/generic/overlap4_min.smt2 diff --git a/test/regression/base/generic/overlap_unsat_core3.smt2.expected.err b/test/regression/unsatcores/generic/overlap4_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_unsat_core3.smt2.expected.err rename to test/regression/unsatcores/generic/overlap4_min.smt2.expected.err diff --git a/test/regression/base/generic/overlap_min_unsat_core4.smt2.expected.out b/test/regression/unsatcores/generic/overlap4_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core4.smt2.expected.out rename to test/regression/unsatcores/generic/overlap4_min.smt2.expected.out diff --git a/test/regression/base/generic/overlap_min_unsat_core4_full.smt2 b/test/regression/unsatcores/generic/overlap4_min_full.smt2 similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core4_full.smt2 rename to test/regression/unsatcores/generic/overlap4_min_full.smt2 diff --git a/test/regression/base/generic/overlap_unsat_core3_full.smt2.expected.err b/test/regression/unsatcores/generic/overlap4_min_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_unsat_core3_full.smt2.expected.err rename to test/regression/unsatcores/generic/overlap4_min_full.smt2.expected.err diff --git a/test/regression/base/generic/overlap_min_unsat_core4_full.smt2.expected.out b/test/regression/unsatcores/generic/overlap4_min_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core4_full.smt2.expected.out rename to test/regression/unsatcores/generic/overlap4_min_full.smt2.expected.out diff --git a/test/regression/base/generic/overlap_unsat_core_full.smt2 b/test/regression/unsatcores/generic/overlap_full.smt2 similarity index 100% rename from test/regression/base/generic/overlap_unsat_core_full.smt2 rename to test/regression/unsatcores/generic/overlap_full.smt2 diff --git a/test/regression/base/generic/overlap_unsat_core4.smt2.expected.err b/test/regression/unsatcores/generic/overlap_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_unsat_core4.smt2.expected.err rename to test/regression/unsatcores/generic/overlap_full.smt2.expected.err diff --git a/test/regression/base/generic/overlap_unsat_core_full.smt2.expected.out b/test/regression/unsatcores/generic/overlap_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_unsat_core_full.smt2.expected.out rename to test/regression/unsatcores/generic/overlap_full.smt2.expected.out diff --git a/test/regression/base/generic/overlap_min_unsat_core.smt2 b/test/regression/unsatcores/generic/overlap_min.smt2 similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core.smt2 rename to test/regression/unsatcores/generic/overlap_min.smt2 diff --git a/test/regression/base/generic/overlap_unsat_core4_full.smt2.expected.err b/test/regression/unsatcores/generic/overlap_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_unsat_core4_full.smt2.expected.err rename to test/regression/unsatcores/generic/overlap_min.smt2.expected.err diff --git a/test/regression/base/generic/overlap_unsat_core2.smt2.expected.out b/test/regression/unsatcores/generic/overlap_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_unsat_core2.smt2.expected.out rename to test/regression/unsatcores/generic/overlap_min.smt2.expected.out diff --git a/test/regression/base/generic/overlap_min_unsat_core_full.smt2 b/test/regression/unsatcores/generic/overlap_min_full.smt2 similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core_full.smt2 rename to test/regression/unsatcores/generic/overlap_min_full.smt2 diff --git a/test/regression/base/generic/overlap_unsat_core_full.smt2.expected.err b/test/regression/unsatcores/generic/overlap_min_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/overlap_unsat_core_full.smt2.expected.err rename to test/regression/unsatcores/generic/overlap_min_full.smt2.expected.err diff --git a/test/regression/base/generic/overlap_min_unsat_core_full.smt2.expected.out b/test/regression/unsatcores/generic/overlap_min_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/overlap_min_unsat_core_full.smt2.expected.out rename to test/regression/unsatcores/generic/overlap_min_full.smt2.expected.out diff --git a/test/regression/base/generic/redundant_unsat_core.smt2 b/test/regression/unsatcores/generic/redundant.smt2 similarity index 100% rename from test/regression/base/generic/redundant_unsat_core.smt2 rename to test/regression/unsatcores/generic/redundant.smt2 diff --git a/test/regression/base/generic/redundant_min_unsat_core.smt2.expected.err b/test/regression/unsatcores/generic/redundant.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core.smt2.expected.err rename to test/regression/unsatcores/generic/redundant.smt2.expected.err diff --git a/test/regression/base/generic/redundant_min_unsat_core.smt2.expected.out b/test/regression/unsatcores/generic/redundant.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core.smt2.expected.out rename to test/regression/unsatcores/generic/redundant.smt2.expected.out diff --git a/test/regression/base/generic/redundant_unsat_core2.smt2 b/test/regression/unsatcores/generic/redundant2.smt2 similarity index 100% rename from test/regression/base/generic/redundant_unsat_core2.smt2 rename to test/regression/unsatcores/generic/redundant2.smt2 diff --git a/test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.err b/test/regression/unsatcores/generic/redundant2.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.err rename to test/regression/unsatcores/generic/redundant2.smt2.expected.err diff --git a/test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.out b/test/regression/unsatcores/generic/redundant2.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core2.smt2.expected.out rename to test/regression/unsatcores/generic/redundant2.smt2.expected.out diff --git a/test/regression/base/generic/redundant_unsat_core2_full.smt2 b/test/regression/unsatcores/generic/redundant2_full.smt2 similarity index 100% rename from test/regression/base/generic/redundant_unsat_core2_full.smt2 rename to test/regression/unsatcores/generic/redundant2_full.smt2 diff --git a/test/regression/base/generic/redundant_min_unsat_core2_full.smt2.expected.err b/test/regression/unsatcores/generic/redundant2_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core2_full.smt2.expected.err rename to test/regression/unsatcores/generic/redundant2_full.smt2.expected.err diff --git a/test/regression/base/generic/redundant_min_unsat_core2_full.smt2.expected.out b/test/regression/unsatcores/generic/redundant2_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core2_full.smt2.expected.out rename to test/regression/unsatcores/generic/redundant2_full.smt2.expected.out diff --git a/test/regression/base/generic/redundant_min_unsat_core2.smt2 b/test/regression/unsatcores/generic/redundant2_min.smt2 similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core2.smt2 rename to test/regression/unsatcores/generic/redundant2_min.smt2 diff --git a/test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.err b/test/regression/unsatcores/generic/redundant2_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.err rename to test/regression/unsatcores/generic/redundant2_min.smt2.expected.err diff --git a/test/regression/base/generic/redundant_unsat_core2.smt2.expected.out b/test/regression/unsatcores/generic/redundant2_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_unsat_core2.smt2.expected.out rename to test/regression/unsatcores/generic/redundant2_min.smt2.expected.out diff --git a/test/regression/base/generic/redundant_min_unsat_core2_full.smt2 b/test/regression/unsatcores/generic/redundant2_min_full.smt2 similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core2_full.smt2 rename to test/regression/unsatcores/generic/redundant2_min_full.smt2 diff --git a/test/regression/base/generic/redundant_min_unsat_core3_full.smt2.expected.err b/test/regression/unsatcores/generic/redundant2_min_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core3_full.smt2.expected.err rename to test/regression/unsatcores/generic/redundant2_min_full.smt2.expected.err diff --git a/test/regression/base/generic/redundant_min_unsat_core3_full.smt2.expected.out b/test/regression/unsatcores/generic/redundant2_min_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core3_full.smt2.expected.out rename to test/regression/unsatcores/generic/redundant2_min_full.smt2.expected.out diff --git a/test/regression/base/generic/redundant_unsat_core3.smt2 b/test/regression/unsatcores/generic/redundant3.smt2 similarity index 100% rename from test/regression/base/generic/redundant_unsat_core3.smt2 rename to test/regression/unsatcores/generic/redundant3.smt2 diff --git a/test/regression/base/generic/redundant_min_unsat_core_full.smt2.expected.err b/test/regression/unsatcores/generic/redundant3.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core_full.smt2.expected.err rename to test/regression/unsatcores/generic/redundant3.smt2.expected.err diff --git a/test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.out b/test/regression/unsatcores/generic/redundant3.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core3.smt2.expected.out rename to test/regression/unsatcores/generic/redundant3.smt2.expected.out diff --git a/test/regression/base/generic/redundant_unsat_core3_full.smt2 b/test/regression/unsatcores/generic/redundant3_full.smt2 similarity index 100% rename from test/regression/base/generic/redundant_unsat_core3_full.smt2 rename to test/regression/unsatcores/generic/redundant3_full.smt2 diff --git a/test/regression/base/generic/redundant_unsat_core.smt2.expected.err b/test/regression/unsatcores/generic/redundant3_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_unsat_core.smt2.expected.err rename to test/regression/unsatcores/generic/redundant3_full.smt2.expected.err diff --git a/test/regression/base/generic/redundant_unsat_core2_full.smt2.expected.out b/test/regression/unsatcores/generic/redundant3_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_unsat_core2_full.smt2.expected.out rename to test/regression/unsatcores/generic/redundant3_full.smt2.expected.out diff --git a/test/regression/base/generic/redundant_min_unsat_core3.smt2 b/test/regression/unsatcores/generic/redundant3_min.smt2 similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core3.smt2 rename to test/regression/unsatcores/generic/redundant3_min.smt2 diff --git a/test/regression/base/generic/redundant_unsat_core2.smt2.expected.err b/test/regression/unsatcores/generic/redundant3_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_unsat_core2.smt2.expected.err rename to test/regression/unsatcores/generic/redundant3_min.smt2.expected.err diff --git a/test/regression/base/generic/redundant_unsat_core3.smt2.expected.out b/test/regression/unsatcores/generic/redundant3_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_unsat_core3.smt2.expected.out rename to test/regression/unsatcores/generic/redundant3_min.smt2.expected.out diff --git a/test/regression/base/generic/redundant_min_unsat_core3_full.smt2 b/test/regression/unsatcores/generic/redundant3_min_full.smt2 similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core3_full.smt2 rename to test/regression/unsatcores/generic/redundant3_min_full.smt2 diff --git a/test/regression/base/generic/redundant_unsat_core2_full.smt2.expected.err b/test/regression/unsatcores/generic/redundant3_min_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_unsat_core2_full.smt2.expected.err rename to test/regression/unsatcores/generic/redundant3_min_full.smt2.expected.err diff --git a/test/regression/base/generic/redundant_unsat_core3_full.smt2.expected.out b/test/regression/unsatcores/generic/redundant3_min_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_unsat_core3_full.smt2.expected.out rename to test/regression/unsatcores/generic/redundant3_min_full.smt2.expected.out diff --git a/test/regression/base/generic/redundant_unsat_core_full.smt2 b/test/regression/unsatcores/generic/redundant_full.smt2 similarity index 100% rename from test/regression/base/generic/redundant_unsat_core_full.smt2 rename to test/regression/unsatcores/generic/redundant_full.smt2 diff --git a/test/regression/base/generic/redundant_unsat_core3.smt2.expected.err b/test/regression/unsatcores/generic/redundant_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_unsat_core3.smt2.expected.err rename to test/regression/unsatcores/generic/redundant_full.smt2.expected.err diff --git a/test/regression/base/generic/redundant_min_unsat_core_full.smt2.expected.out b/test/regression/unsatcores/generic/redundant_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core_full.smt2.expected.out rename to test/regression/unsatcores/generic/redundant_full.smt2.expected.out diff --git a/test/regression/base/generic/redundant_min_unsat_core.smt2 b/test/regression/unsatcores/generic/redundant_min.smt2 similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core.smt2 rename to test/regression/unsatcores/generic/redundant_min.smt2 diff --git a/test/regression/base/generic/redundant_unsat_core3_full.smt2.expected.err b/test/regression/unsatcores/generic/redundant_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_unsat_core3_full.smt2.expected.err rename to test/regression/unsatcores/generic/redundant_min.smt2.expected.err diff --git a/test/regression/base/generic/redundant_unsat_core.smt2.expected.out b/test/regression/unsatcores/generic/redundant_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_unsat_core.smt2.expected.out rename to test/regression/unsatcores/generic/redundant_min.smt2.expected.out diff --git a/test/regression/base/generic/redundant_min_unsat_core_full.smt2 b/test/regression/unsatcores/generic/redundant_min_full.smt2 similarity index 100% rename from test/regression/base/generic/redundant_min_unsat_core_full.smt2 rename to test/regression/unsatcores/generic/redundant_min_full.smt2 diff --git a/test/regression/base/generic/redundant_unsat_core_full.smt2.expected.err b/test/regression/unsatcores/generic/redundant_min_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/redundant_unsat_core_full.smt2.expected.err rename to test/regression/unsatcores/generic/redundant_min_full.smt2.expected.err diff --git a/test/regression/base/generic/redundant_unsat_core_full.smt2.expected.out b/test/regression/unsatcores/generic/redundant_min_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/redundant_unsat_core_full.smt2.expected.out rename to test/regression/unsatcores/generic/redundant_min_full.smt2.expected.out diff --git a/test/regression/base/generic/trivial_unsat_core.smt2 b/test/regression/unsatcores/generic/trivial.smt2 similarity index 100% rename from test/regression/base/generic/trivial_unsat_core.smt2 rename to test/regression/unsatcores/generic/trivial.smt2 diff --git a/test/regression/base/generic/trivial_min_unsat_core.smt2.expected.err b/test/regression/unsatcores/generic/trivial.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core.smt2.expected.err rename to test/regression/unsatcores/generic/trivial.smt2.expected.err diff --git a/test/regression/base/generic/trivial_min_unsat_core.smt2.expected.out b/test/regression/unsatcores/generic/trivial.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core.smt2.expected.out rename to test/regression/unsatcores/generic/trivial.smt2.expected.out diff --git a/test/regression/base/generic/trivial_unsat_core2.smt2 b/test/regression/unsatcores/generic/trivial2.smt2 similarity index 100% rename from test/regression/base/generic/trivial_unsat_core2.smt2 rename to test/regression/unsatcores/generic/trivial2.smt2 diff --git a/test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.err b/test/regression/unsatcores/generic/trivial2.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.err rename to test/regression/unsatcores/generic/trivial2.smt2.expected.err diff --git a/test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.out b/test/regression/unsatcores/generic/trivial2.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core2.smt2.expected.out rename to test/regression/unsatcores/generic/trivial2.smt2.expected.out diff --git a/test/regression/base/generic/trivial_unsat_core2_full.smt2 b/test/regression/unsatcores/generic/trivial2_full.smt2 similarity index 100% rename from test/regression/base/generic/trivial_unsat_core2_full.smt2 rename to test/regression/unsatcores/generic/trivial2_full.smt2 diff --git a/test/regression/base/generic/trivial_min_unsat_core_full.smt2.expected.err b/test/regression/unsatcores/generic/trivial2_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core_full.smt2.expected.err rename to test/regression/unsatcores/generic/trivial2_full.smt2.expected.err diff --git a/test/regression/base/generic/trivial_min_unsat_core_full.smt2.expected.out b/test/regression/unsatcores/generic/trivial2_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core_full.smt2.expected.out rename to test/regression/unsatcores/generic/trivial2_full.smt2.expected.out diff --git a/test/regression/base/generic/trivial_min_unsat_core2.smt2 b/test/regression/unsatcores/generic/trivial2_min.smt2 similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core2.smt2 rename to test/regression/unsatcores/generic/trivial2_min.smt2 diff --git a/test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.err b/test/regression/unsatcores/generic/trivial2_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.err rename to test/regression/unsatcores/generic/trivial2_min.smt2.expected.err diff --git a/test/regression/base/generic/trivial_unsat_core2.smt2.expected.out b/test/regression/unsatcores/generic/trivial2_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_unsat_core2.smt2.expected.out rename to test/regression/unsatcores/generic/trivial2_min.smt2.expected.out diff --git a/test/regression/base/generic/trivial_unsat_core3.smt2 b/test/regression/unsatcores/generic/trivial3.smt2 similarity index 100% rename from test/regression/base/generic/trivial_unsat_core3.smt2 rename to test/regression/unsatcores/generic/trivial3.smt2 diff --git a/test/regression/base/generic/trivial_unsat_core.smt2.expected.err b/test/regression/unsatcores/generic/trivial3.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_unsat_core.smt2.expected.err rename to test/regression/unsatcores/generic/trivial3.smt2.expected.err diff --git a/test/regression/base/generic/trivial_unsat_core3.smt2.expected.out b/test/regression/unsatcores/generic/trivial3.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_unsat_core3.smt2.expected.out rename to test/regression/unsatcores/generic/trivial3.smt2.expected.out diff --git a/test/regression/base/generic/trivial_unsat_core3_full.smt2 b/test/regression/unsatcores/generic/trivial3_full.smt2 similarity index 100% rename from test/regression/base/generic/trivial_unsat_core3_full.smt2 rename to test/regression/unsatcores/generic/trivial3_full.smt2 diff --git a/test/regression/base/generic/trivial_unsat_core2.smt2.expected.err b/test/regression/unsatcores/generic/trivial3_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_unsat_core2.smt2.expected.err rename to test/regression/unsatcores/generic/trivial3_full.smt2.expected.err diff --git a/test/regression/base/generic/trivial_unsat_core2_full.smt2.expected.out b/test/regression/unsatcores/generic/trivial3_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_unsat_core2_full.smt2.expected.out rename to test/regression/unsatcores/generic/trivial3_full.smt2.expected.out diff --git a/test/regression/base/generic/trivial_unsat_core_full.smt2 b/test/regression/unsatcores/generic/trivial_full.smt2 similarity index 100% rename from test/regression/base/generic/trivial_unsat_core_full.smt2 rename to test/regression/unsatcores/generic/trivial_full.smt2 diff --git a/test/regression/base/generic/trivial_unsat_core2_full.smt2.expected.err b/test/regression/unsatcores/generic/trivial_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_unsat_core2_full.smt2.expected.err rename to test/regression/unsatcores/generic/trivial_full.smt2.expected.err diff --git a/test/regression/base/generic/trivial_unsat_core3_full.smt2.expected.out b/test/regression/unsatcores/generic/trivial_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_unsat_core3_full.smt2.expected.out rename to test/regression/unsatcores/generic/trivial_full.smt2.expected.out diff --git a/test/regression/base/generic/trivial_min_unsat_core.smt2 b/test/regression/unsatcores/generic/trivial_min.smt2 similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core.smt2 rename to test/regression/unsatcores/generic/trivial_min.smt2 diff --git a/test/regression/base/generic/trivial_unsat_core3.smt2.expected.err b/test/regression/unsatcores/generic/trivial_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_unsat_core3.smt2.expected.err rename to test/regression/unsatcores/generic/trivial_min.smt2.expected.err diff --git a/test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.out b/test/regression/unsatcores/generic/trivial_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_min_xor_unsat_core.smt2.expected.out rename to test/regression/unsatcores/generic/trivial_min.smt2.expected.out diff --git a/test/regression/base/generic/trivial_min_unsat_core_full.smt2 b/test/regression/unsatcores/generic/trivial_min_full.smt2 similarity index 100% rename from test/regression/base/generic/trivial_min_unsat_core_full.smt2 rename to test/regression/unsatcores/generic/trivial_min_full.smt2 diff --git a/test/regression/base/generic/trivial_unsat_core3_full.smt2.expected.err b/test/regression/unsatcores/generic/trivial_min_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_unsat_core3_full.smt2.expected.err rename to test/regression/unsatcores/generic/trivial_min_full.smt2.expected.err diff --git a/test/regression/base/generic/trivial_unsat_core_full.smt2.expected.out b/test/regression/unsatcores/generic/trivial_min_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_unsat_core_full.smt2.expected.out rename to test/regression/unsatcores/generic/trivial_min_full.smt2.expected.out diff --git a/test/regression/base/generic/trivial_xor_unsat_core.smt2 b/test/regression/unsatcores/generic/trivial_xor.smt2 similarity index 100% rename from test/regression/base/generic/trivial_xor_unsat_core.smt2 rename to test/regression/unsatcores/generic/trivial_xor.smt2 diff --git a/test/regression/base/generic/trivial_unsat_core_full.smt2.expected.err b/test/regression/unsatcores/generic/trivial_xor.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_unsat_core_full.smt2.expected.err rename to test/regression/unsatcores/generic/trivial_xor.smt2.expected.err diff --git a/test/regression/base/generic/trivial_unsat_core.smt2.expected.out b/test/regression/unsatcores/generic/trivial_xor.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_unsat_core.smt2.expected.out rename to test/regression/unsatcores/generic/trivial_xor.smt2.expected.out diff --git a/test/regression/base/generic/trivial_xor_unsat_core_full.smt2 b/test/regression/unsatcores/generic/trivial_xor_full.smt2 similarity index 100% rename from test/regression/base/generic/trivial_xor_unsat_core_full.smt2 rename to test/regression/unsatcores/generic/trivial_xor_full.smt2 diff --git a/test/regression/base/generic/trivial_xor_unsat_core.smt2.expected.err b/test/regression/unsatcores/generic/trivial_xor_full.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_xor_unsat_core.smt2.expected.err rename to test/regression/unsatcores/generic/trivial_xor_full.smt2.expected.err diff --git a/test/regression/base/generic/trivial_xor_unsat_core_full.smt2.expected.out b/test/regression/unsatcores/generic/trivial_xor_full.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_xor_unsat_core_full.smt2.expected.out rename to test/regression/unsatcores/generic/trivial_xor_full.smt2.expected.out diff --git a/test/regression/base/generic/trivial_min_xor_unsat_core.smt2 b/test/regression/unsatcores/generic/trivial_xor_min.smt2 similarity index 100% rename from test/regression/base/generic/trivial_min_xor_unsat_core.smt2 rename to test/regression/unsatcores/generic/trivial_xor_min.smt2 diff --git a/test/regression/base/generic/trivial_xor_unsat_core_full.smt2.expected.err b/test/regression/unsatcores/generic/trivial_xor_min.smt2.expected.err similarity index 100% rename from test/regression/base/generic/trivial_xor_unsat_core_full.smt2.expected.err rename to test/regression/unsatcores/generic/trivial_xor_min.smt2.expected.err diff --git a/test/regression/base/generic/trivial_xor_unsat_core.smt2.expected.out b/test/regression/unsatcores/generic/trivial_xor_min.smt2.expected.out similarity index 100% rename from test/regression/base/generic/trivial_xor_unsat_core.smt2.expected.out rename to test/regression/unsatcores/generic/trivial_xor_min.smt2.expected.out diff --git a/test/regression/base/incremental/unsat_core_global.smt2 b/test/regression/unsatcores/incremental/global.smt2 similarity index 100% rename from test/regression/base/incremental/unsat_core_global.smt2 rename to test/regression/unsatcores/incremental/global.smt2 diff --git a/test/regression/base/incremental/unsat_core_global.smt2.expected.err b/test/regression/unsatcores/incremental/global.smt2.expected.err similarity index 100% rename from test/regression/base/incremental/unsat_core_global.smt2.expected.err rename to test/regression/unsatcores/incremental/global.smt2.expected.err diff --git a/test/regression/base/incremental/unsat_core_global.smt2.expected.out b/test/regression/unsatcores/incremental/global.smt2.expected.out similarity index 100% rename from test/regression/base/incremental/unsat_core_global.smt2.expected.out rename to test/regression/unsatcores/incremental/global.smt2.expected.out diff --git a/test/regression/base/incremental/unsat_core_scoped.smt2 b/test/regression/unsatcores/incremental/scoped.smt2 similarity index 100% rename from test/regression/base/incremental/unsat_core_scoped.smt2 rename to test/regression/unsatcores/incremental/scoped.smt2 diff --git a/test/regression/base/incremental/unsat_core_scoped.smt2.expected.err b/test/regression/unsatcores/incremental/scoped.smt2.expected.err similarity index 100% rename from test/regression/base/incremental/unsat_core_scoped.smt2.expected.err rename to test/regression/unsatcores/incremental/scoped.smt2.expected.err diff --git a/test/regression/base/incremental/unsat_core_scoped.smt2.expected.out b/test/regression/unsatcores/incremental/scoped.smt2.expected.out similarity index 100% rename from test/regression/base/incremental/unsat_core_scoped.smt2.expected.out rename to test/regression/unsatcores/incremental/scoped.smt2.expected.out diff --git a/test/regression/unsatcores/run-test-notiming.sh b/test/regression/unsatcores/run-test-notiming.sh new file mode 100755 index 000000000..cd1d6bcc7 --- /dev/null +++ b/test/regression/unsatcores/run-test-notiming.sh @@ -0,0 +1,72 @@ +#!/bin/bash +get_abs_filename() { + echo "$(cd "$(dirname "$1")" && pwd)/$(basename "$1")" +} + +usage="Usage: $0 [-h] " + +while [ $# -gt 0 ]; do + case $1 in + -h|--help) + echo "${usage}" + exit 1 + ;; + -*) + echo "Error: invalid option '$1'" + exit 1 + ;; + *) + break + esac + shift; shift +done + +opensmt=$1 + +if [ -z ${opensmt} ]; then + echo "Opensmt binary not specified" + exit 1 +fi + +echo "This is the script for running regression tests for unsatisfiable cores" +echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')" +echo " - host name $(hostname -f)" +echo " - script path: $(get_abs_filename $0)" + +tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S') +mkdir ${tmpfolder} + +export outmod=false +export errmod=false +export rtmod=false +tolerance=1.5 + +for file in $(find . -name '*.smt2' |sort); do + name=$(basename $file) + dir=$(dirname $file) + + sh -c "ulimit -St 60; ${opensmt} $(echo ${options}) $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null + + grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err + diff -q ${tmpfolder}/${name}.out ${dir}/${name}.expected.out + if [ $? != 0 ]; then + echo "stdout differs for benchmark $file"; + outmod=true; + diff ${tmpfolder}/${name}.out ${dir}/${name}.expected.out + fi + diff -q ${tmpfolder}/${name}.err ${dir}/${name}.expected.err + if [ $? != 0 ]; then + echo "stderr differs for benchmark $file"; + errmod=true; + diff ${tmpfolder}/${name}.err ${dir}/${name}.expected.err + fi + +done +echo "Stdout differs: ${outmod}, stderr differs: ${errmod}" + +if [[ ${outmod} == true || ${errmod} == true ]]; then + echo "There were anomalies: check logs in ${tmpfolder}" + exit 1 +else + rm -rf ${tmpfolder} +fi