From 356eb0b3b1451efd565c2fcd6c75984651779914 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 2 May 2020 18:55:38 -0700 Subject: [PATCH] fix debugging assistance code that is no longer valid when you compute multiple counterexamples --- .../counterexamples/SMTMinimalLabelSetGenerator.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 58f13ae10..4d4dd9629 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1220,10 +1220,6 @@ namespace storm { // try with an increased bound. while (solver.checkWithAssumptions({assumption}) == storm::solver::SmtSolver::CheckResult::Unsat) { STORM_LOG_DEBUG("Constraint system is unsatisfiable with at most " << currentBound << " taken commands; increasing bound."); -#ifndef NDEBUG - STORM_LOG_DEBUG("Sanity check to see whether constraint system is still satisfiable."); - STORM_LOG_ASSERT(solver.check() == storm::solver::SmtSolver::CheckResult::Sat, "Constraint system is not satisfiable anymore."); -#endif solver.add(variableInformation.auxiliaryVariables.back()); variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(solver, variableInformation, ++currentBound)); assumption = !variableInformation.auxiliaryVariables.back(); @@ -1755,6 +1751,10 @@ namespace storm { if (result.size() > 0 && iterations > firstCounterexampleFound + options.maximumExtraIterations) { break; } + if (result.size() == 0) { + STORM_LOG_DEBUG("Sanity check to see whether constraint system is still satisfiable."); + STORM_LOG_ASSERT(solver->check() == storm::solver::SmtSolver::CheckResult::Sat, "Constraint system is not satisfiable anymore."); + } STORM_LOG_DEBUG("Computing minimal command set."); solverClock = std::chrono::high_resolution_clock::now(); boost::optional> smallest = findSmallestCommandSet(*solver, variableInformation, currentBound);