blah

src/smt/set_defaults.cpp

@@ -1823,8 +1823,12 @@ void SetDefaults::notifyModifyOption(const std::string& x,
 
 void SetDefaults::disableChecking(Options& opts)
 {
+  opts.write_smt().produceUnsatCores = false;
+  opts.write_smt().unsatCoresMode = options::UnsatCoresMode::OFF;
+  opts.write_smt().minimalUnsatCores = false;
   opts.write_smt().checkUnsatCores = false;
   opts.write_smt().produceProofs = false;
+  opts.write_smt().proofMode = options::ProofMode::OFF;
   opts.write_smt().checkProofs = false;
   opts.write_smt().debugCheckModels = false;
   opts.write_smt().checkModels = false;

src/smt/unsat_core_manager.cpp

@@ -240,6 +240,7 @@ std::vector<Node> UnsatCoreManager::reduceUnsatCore(
     // disable all proof options
     SetDefaults::disableChecking(coreChecker->getOptions());
     // add to removed set?
+    Trace("unsat-core") << "Consider removing " << skip << "\nTest with " << core << " + " << adefs << " - " << removed << "\n";
     removed.insert(skip);
     // assert everything to the subsolver
     theory::assertToSubsolver(*coreChecker.get(), core, adefs, removed);
@@ -255,6 +256,7 @@ std::vector<Node> UnsatCoreManager::reduceUnsatCore(
 
     if (r.getStatus() != Result::UNSAT)
     {
+      Trace("unsat-core") << "\tcannot remove\n";
       removed.erase(skip);
       if (r.isUnknown())
       {

src/theory/smt_engine_subsolver.cpp

@@ -183,6 +183,7 @@ void assertToSubsolver(SolverEngine& subsolver,
         continue;
       }
     }
+    Trace("test") << "\t\tassert " << f << "\n";
     subsolver.assertFormula(f);
   }
 }