@@ -270,9 +270,12 @@ data class UtSolver constructor(
270
270
UNSATISFIABLE -> {
271
271
val unsatCore = z3Solver.unsatCore
272
272
273
+ val failedSoftConstraints = unsatCore.filter { it in translatedSoft.keys }
274
+ val failedAssumptions = unsatCore.filter { it in translatedAssumptions.keys }
275
+
273
276
// if we don't have any soft constraints and enabled unsat cores
274
277
// for hard constraints, then calculate it and print the result using the logger
275
- if (translatedSoft .isEmpty() && translatedAssumptions .isEmpty() && UtSettings .enableUnsatCoreCalculationForHardConstraints) {
278
+ if (failedSoftConstraints .isEmpty() && failedAssumptions .isEmpty() && UtSettings .enableUnsatCoreCalculationForHardConstraints) {
276
279
with (context.mkSolver()) {
277
280
check(* z3Solver.assertions)
278
281
val constraintsInUnsatCore = this .unsatCore.toList()
@@ -286,20 +289,16 @@ data class UtSolver constructor(
286
289
// an unsat core for hard constraints
287
290
if (unsatCore.isEmpty()) return UNSAT
288
291
289
- val failedSoftConstraints = unsatCore.filter { it in translatedSoft.keys }
290
-
291
292
if (failedSoftConstraints.isNotEmpty()) {
292
293
failedSoftConstraints.forEach { translatedSoft.remove(it) }
293
294
// remove soft constraints first, only then try to remove assumptions
294
295
continue
295
296
}
296
297
297
- unsatCore
298
- .filter { it in translatedAssumptions.keys }
299
- .forEach {
300
- assumptionsInUnsatCore + = translatedAssumptions.getValue(it)
301
- translatedAssumptions.remove(it)
302
- }
298
+ failedAssumptions.forEach {
299
+ assumptionsInUnsatCore + = translatedAssumptions.getValue(it)
300
+ translatedAssumptions.remove(it)
301
+ }
303
302
}
304
303
else -> {
305
304
logger.debug { " Reason of UNKNOWN: ${z3Solver.reasonUnknown} " }
0 commit comments