Performance and assertion fix in min unsat cores

usi-verification-and-security · Nov 4, 2024 · ecd1474 · ecd1474
1 parent 6503ff8
commit ecd1474
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/src/unsatcores/UnsatCoreBuilder.cc b/src/unsatcores/UnsatCoreBuilder.cc
@@ -92,18 +92,19 @@ void UnsatCoreBuilder::partitionNamedTerms() {
     namedTerms.clear();
     hiddenTerms.clear();
 
+    bool const minCore = config.minimal_unsat_cores();
+    // See the comment in `minimize` for why we exclude hidden terms here
+
     auto const & termNames = solver.getTermNames();
     if (termNames.empty()) {
-        hiddenTerms = std::move(allTerms);
+        if (not minCore) { hiddenTerms = std::move(allTerms); }
         return;
     }
 
-    bool const minCore = config.minimal_unsat_cores();
     for (PTRef term : allTerms) {
         if (termNames.contains(term)) {
             namedTerms.push(term);
         } else if (not minCore) {
-            // See the comment in `minimize` for why we exclude hidden terms
             hiddenTerms.push(term);
         }
     }