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] <path-to-opensmt>"
+
+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